Hello,
I've been unsuccessful in installing HOL Light on my Mac. I have both
OCaml 3.12.0 and camlp5 5.15 installed, and I'm installing from the HL
snapshot of 10 January 2010 from the HOL Light page, but when I type
'make' in the hol_light directory, I receive the message:
if test `ocamlc -version | cut -c1-4` = "3.10" -o `ocamlc -version |
cut -c1-4` = "3.11" ; \
then ocamlc -c -pp "camlp5r pa_lexer.cmo
pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml; \
else ocamlc -c -pp "camlp4r pa_extend.cmo
q_MLast.cmo" -I +camlp4 pa_j.ml; \
fi
File "pa_j.ml", line 104, characters 10-13:
Parse error: "::" or "]" expected after [sem_expr_for_list] (in [expr])
File "pa_j.ml", line 1, characters 0-1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2
Thinking that it might have worked despite the error, I typed #use
"hol.ml";; while in OCaml. I obtain
val hol_version : string = "2.20++"
val hol_dir : string ref = {contents = "/Users/Anthony/Documents/hol_light"}
val temp_path : string ref = {contents = "/tmp"}
Exception: Symtable.Error _.
Would anyone be able to help?
Many thanks in advance,
Anthony Pulido
------------------------------------------------------------------------------
Start uncovering the many advantages of virtual appliances
and start using them to simplify application deployment and
accelerate your shift to cloud computing.
http://p.sf.net/sfu/novell-sfdev2dev
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
