build fails with "cp: cannot stat `pa_j_3.1x_7.xx.ml': No such file or directory"

[GoogleCodeExporter]

I checked out from the subversion repository (r146) and executed make in the 
root directory and got the error message above returned. A quick look at the 
directory showed that it is really not there:

[user@hostname hol-light-read-only]$ ls -1 pa_j*
pa_j_3.07.ml
pa_j_3.08.ml
pa_j_3.09.ml
pa_j_3.1x_5.xx.ml
pa_j_3.1x_6.02.1.ml
pa_j_3.1x_6.02.2.ml
pa_j_3.1x_6.xx.ml

as far as i could see, these files are not automatically generated - is it 
possible that they are only missing in the repository or am I doing something 
wrong? Thanks in advance, Martin

Original issue reported on code.google.com by [email protected] on 29 Aug 2012 at 2:12

[GoogleCodeExporter]

The system used is Fedora 17/x64 with ocaml-3.12.1-12.fc17.x86_64 and 
ocaml-camlp5-6.02.3-2.fc17.x86_64 installed.

Original comment by [email protected] on 29 Aug 2012 at 2:16

[GoogleCodeExporter]

I made an update over the long weekend to try to fix these build
problems with recent OCaml and camlp5 combinations. Can you do an
"svn update" and see if it's fixed?

Original comment by [email protected] on 5 Sep 2012 at 10:27

[GoogleCodeExporter]

Thanks for your help - svn update lead to the same error. Reading the new 
install instructions i found out, that Fedora provides the camlp5 binary 
compiled in transitional mode and only in the devel package. After installing 
that, I got the following error:

[user@hostname hol-light-read-only]$ 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 cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1`.xx.ml pa_j.ml; \
                  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 pa_j.ml; \
                   else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml; \
                   fi
File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
       but an expression was expected of type
         ('a * MLast.ctyp) list Ploc.vala


I will now try to build camlp5 in strict mode from source and report back if 
this was causing the error.

greetings, Martin

Original comment by [email protected] on 6 Sep 2012 at 9:02

[GoogleCodeExporter]

The output with camlp5 in strict mode is unfortunately the same.

Original comment by [email protected] on 6 Sep 2012 at 9:14

[GoogleCodeExporter]

Hmm, that is a bit surprising since I thought that was an OCaml / camlp5
combination I've used successfully.

Can you try "make clean" first in the HOL Light directory before "make",
in case the earlier version was left? If that doesn't work, can you
double-check the versions and let me know? My own output is below:

$ ocamlc -version
4.00.0
$ camlp5 -v
Camlp5 version 6.06 (ocaml 4.00.0)
$ camlp5 -pmode
strict

Original comment by [email protected] on 6 Sep 2012 at 9:38

[jamesturner246]

This may solve your problem. You need to install package ocaml-camlp5-devel to get the camlp5 command in Fedora systems. After this, the Makefile should build successfully. I hope this helps.

All the best, James.