Thank you very much, Jeremy! It worked! Doing the same thing to hol.ml gets
past the second error.
Very gratefully,
Anthony
On Fri, Sep 17, 2010 at 7:51 PM, Jeremy Bem <jere...@gmail.com> wrote:
> 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 <
> anthony.pul...@gmail.com> 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
>> hol-info@lists.sourceforge.net
>> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
