Problem building HOL light with OCaml 4

[GoogleCodeExporter]

trafficstars

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 [email protected] on 27 Oct 2013 at 7:39

[GoogleCodeExporter]

This should have been fixed by the changes in r176; please let me know if not.

Original comment by [email protected] on 9 Mar 2014 at 4:53

[girving]

I'm hitting what I believe is the same problem, with ocaml 4.04 and camlp5 6.17:

(master) beltrami:hol-light% camlp5 -v
Camlp5 version 6.17 (ocaml 4.04.0)

The full output of make is

(master) beltrami:hol-light% make
\
        if test `ocamlc -version | cut -c1-3` = "3.0"  ; \
        then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
        else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.1" ; \
             then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
             else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.03" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.04" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.05" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.06" ; \
                  then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
                  else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.06" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.07" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.08" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.09" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.10" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.11" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.12" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.13" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.14" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.15" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.16" ; \
                       then cp pa_j_3.1x_6.11.ml pa_j.ml; \
                       else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1`.xx.ml pa_j.ml; \
                       fi \
                  fi \
             fi \
        fi
if test `ocamlc -version | cut -c1-3` = "3.0" ; \
                   then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I `camlp4 -where` pa_j.ml ; \
                   else if test `ocamlc -version | cut -c1-3` = "3.1" -o `ocamlc -version | cut -c1-4` = "4.00" -o `ocamlc -version | cut -c1-4` = "4.01"  -o `ocamlc -version | cut -c1-4` = "4.02" -o `ocamlc -version | cut -c1-4` = "4.03" ; \
                        then  ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \
                        else ocamlc -safe-string -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I `camlp5 -where` pa_j.ml ; \
                        fi \
                   fi
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: Error while running external preprocessor
Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' > /tmp/ocamlpp75a063

make: *** [pa_j.cmo] Error 2

[AlaeddineDaghar]

You have 3 options:

1. The easiest way is to use this setup from this link, it will download the right versions automatically: https://bitbucket.org/akrauss/hol-light-workbench

2. Download only the versions mentioned in the make file results (they are old versions but are working fine, no need for the latest versions - nothing new).

3. Tweak the code to recognize your version (it is not guaranteed to work ! I have camlp5 6.16 with ocaml 4.03 running on a mac laptop)

[girving]

Actually Rob Arthan provided me with a patch that fixes the problem. It's attached, but a bit of work would have to be done before it could be safely integrated.

patch-for-pa_j-ml.txt