Hi,
I ran into several problems installing HOL Light on Ubuntu 12.04. Googling
around, I found similar problems; any new HOL user with Ubuntu will run
into these, I think. It would be great if the configurations and
documentation could reflect this so other users don't hit this.
I checked out the latest sources from SVN. Following the README, I
installed ocaml and camlp5 via "apt-get install".
1. Error with workaround... "apt-get install" puts Ocaml in a
"nonstandard" location.. /usr/lib/ocaml/camlp5. Specifying this with
"export CAMLP5LIB" fixed the problem. (This was tricky to find, because
there were also libs at /usr/local/lib/ocaml/3.12.1, and specifying that
location didn't fix the problem.)
Can the README be updated for this case (or add a "configure" script)?
2. Error with workaround via Google ... The version of campl5, which is
6.02.3. According to a Google search for the error "Error: This expression
has type (string * MLast.ctyp) list", I see this has been a problem for a
while.
Can the README (and the web page) be updated to indicate that HOL
won't work with campl5 versions >= 6.0, and indicate that that's the
default version?
Or even better, can HOL work with campl5 versions >= 6.0 ?
3. Error with workaround via Google... from #2, it was suggested to build
camlp5 from sources. I downloaded campl5-5.15 sources, and according to
the README, ran "./configure --strict", and ran "make". I encountered the
error:
ocamlrun ../boot/camlp5 -nolib -I ../boot ./pa_lispr.cmo pa_extend.cmo
q_MLast.cmo pr_dump.cmo -mode S -o pa_lisp.ppo pa_lisp.ml
Error while loading "./pa_lispr.cmo": interface mismatch on MLast.
Turns out I should have run "./configure --strict", and then "make
world.opt" (and then "sudo make install", of course). Can the README be
changed to reflect this?
4. Running "make clean" and then "make" didn't result in any errors, and
then the other commands worked.
Anyway, with all that, it runs now. Looking forward to trying it out!
Cheers,
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
