Hi there,

I'm installing hol light on a mac. I'm following the instruction on
https://github.com/jrh13/hol-light/blob/master/README. I suppose it would
be pretty straight forward. Here are my actions:

1. I installed the newest version of ocaml (4.05) and camlp5 using brew. No
problem.

2. I cloned the hol-light git to my machine. No problem.

3. I ran "make" in the root folder. It complained at the pa_j.cmo part.
Seems like some files are not found. I manually did some fix to make it
going (without fully understand what I'm doing). Anyway a new pa_j.ml file
was created.

4. I entered the ocaml interface and do #use "hol.ml";;. Boom! There are
like several hundreds of systax errors in almost all ml files. It seems
like nothing is correctly loaded.

I thought maybe it's because the ocaml is too new to recognize the code in
hol-light? So I uninstalled the ocaml and replaced an older version (3.09).
Still not working.

So what did I miss and how can I fix it? Any help would be greatly
appreciated. Thanks!
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to