I have just tried to install HOL Light, but seem to be encountering a version
of the problem documented in this thread.
I would be grateful for any advice - particularly if it had newbie-granularity.
I have camlp4 installed as well as camlp5 now, but don't see any signs of their
interference. Do I have any reason to have both, or should I uninstall camlp4?
Thank you in advance,
Colin Rowat
University of Birmingham
System: Ubuntu 12.04 running on an 64-bit Intel CORE i7 vPro
Used Synaptic to install camlp4 (v.3.12.1), camlp5, ocaml (v.3.12.1)
Used SVN to checkout HOL Light (rev 146)
Found a "Error 2" in Make that seemed to interfere with HOL Light's parsing
Found this thread, so used Synaptic to uninstall camlp5
Downloaded camlp5-6.06 to Desktop and then:
$ make clean
$ ./configure --strict
$ make world.opt
$ sudo make install
>From hol_light directory:
$ make clean
$ make
with this last command yielding:
<begins>
\
if test `ocamlc -version | cut -c3` = "0" ; \
then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut
-c1-6` = "6.02.1" ; \
then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' |
cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' |
cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' |
cut -c1-6` = "6.05" ; \
then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-c1`.xx.ml pa_j.ml; \
fi \
fi \
fi
if test `ocamlc -version | cut -c3` = "0" ; \
then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I
+camlp4 pa_j.ml; \
else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo
q_MLast.cmo" -I +camlp5 pa_j.ml; \
fi
File "pa_j.ml", line 195, characters 6-21:
Error: The constructor PaLab expects 2 argument(s),
but is applied here to 3 argument(s)
make: *** [pa_j.cmo] Error 2
<ends>
The relevant line of pa_j.ml reads:
<begins>
| PaLab loc x1 x2 ->
<ends>
------------------------------------------------------------------------------
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
