search

CJex / hol-light

HOL Light is an interactive theorem prover / proof checker. Automatically exported from code.google.com/p/hol-light
Other
1 stars 0 forks source link

Problem building HOL light with OCaml 4 #9

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?
1. svn checkout http://hol-light.googlecode.com/svn/trunk/ hol-light-read-only
2. make
3.

What is the expected output? What do you see instead?
I get the error message:
File "pa_j.ml", line 1918, characters 35-43:
While expanding quotation "str_item":
Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in
  [str_item])
File "pa_j.ml", line 1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2

What version of the product are you using? On what operating system?
OCaml 4.00.1
Linux Fedora 18

Please provide any additional information below.
I am trying to build HOL Light with OCaml 4, but the build bombs out with the 
above error message.

Original issue reported on code.google.com by nroger1...@gmail.com on 27 Oct 2013 at 7:39

GoogleCodeExporter commented 9 years ago 
This should have been fixed by the changes in r176; please let me know if not.

Original comment by jrh...@gmail.com on 9 Mar 2014 at 4:53