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