Hi Bill,

| John, here's my bug report for trying to install the latest ocaml &
| camlp5.   `make' failed in hol_light (error message at the end).

Yes, these issues with camlp5 versioning are getting to be painful.
The solution could be as simple as a change to the Makefile, which
doesn't necessarily do the right thing if it hits a version of camlp5
that isn't explicitly tested for. I think the current Makefile will
end up using "pa_j_3.1x_6.xx.ml" in this case. You could try manually
copying one of the more recent versions then doing "make", e.g:

  cp pa_j_3.1x_6.02.2.ml pa_j.ml
  make

or

  cp pa_j_3.1x_6.02.1.ml pa_j.ml
  make

If either of those works, let me know and I'll simply fix the Makefile
accordingly. If not, then I may need yet another pa_j.ml variant.

In any case, I can confirm that the OCaml 3.12.1 and camlp5 6.02.3
combination works, since that's what I use on my main machine at
work. You might also consider using Alex Krauss's script that should
help to install the right versions of everything (see his hol-info
message "HOL Light setup script" on 5th May).

  https://bitbucket.org/akrauss/hol-light-workbench/

John.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to