The Makefile of HOL Light just needs a tiny update; it hasn't heard of OCaml
3.12.
Change the entry for pa_j.cmo to the following:
pa_j.cmo: pa_j.ml; if test "`ocamlc -version | cut -c1-4` >= 3.10" ; \
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
Hope that helps,
-Jeremy
On Fri, Sep 17, 2010 at 6:42 PM, Anthony V. Pulido <[email protected]
> wrote:
> 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
>
------------------------------------------------------------------------------
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
