Error in pa_j.ml with OCaml 3.12.0 and camlp5 6.02.2-2

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Install OCaml 3.12.0 on Mac OS X 10.5.8 from prebuilt binaries
2. Download camlp5-6.02.2, apply two patches, and build.
3. Check out most recent verson of HOL Light with svn, and do make.

What is the expected output? What do you see instead?

I get this error message from make:

File "pa_j.ml", line 195, characters 6-21:
Error: The constructor PaLab expects 2 argument(s),
       but is applied here to 3 argument(s)
make: *** [pa_j.cmo] Error 2

What version of the product are you using? On what operating system?

Revision 83 on Mac OS 10.5.8.

Please provide any additional information below.

Can you tell me a combination of a version of HOL Light and a version of camlp5 
that work together?  I had other problems when I tried building the 10 Jan 2010 
snapshot you have on the HOL Light home page.

Original issue reported on code.google.com by kvanh...@ksvanhorn.com on 19 Mar 2011 at 3:19

[GoogleCodeExporter]

BTW, I built camlp5 in strict mode.

Original comment by kvanh...@ksvanhorn.com on 19 Mar 2011 at 3:20

[GoogleCodeExporter]

I believe this should be fixed in revision 86. Let me know if not.
Sorry it took a while to get to this.

Original comment by jrh...@gmail.com on 2 Apr 2011 at 3:38

[GoogleCodeExporter]

This issue appears again with camlp5-6.02.3 (Mac OS X 10.5.8, OCaml 3.12.1, 
HOL-Light svn-r101)

I modified the Makefile as follows to force pa_j_3.1x_6.02.2.ml to be used 
instead of pa_j_3.1x_6.xx.ml and 'make' succeeded.

$ diff Makefile.bak Makefile
59c59
<              else if test ${CAMLP5_VERSION} = "6.02.2" ; \
---
>              else if test ${CAMLP5_VERSION} > "6.02.1" ; \

Original comment by jdgleeso...@gmail.com on 10 Aug 2011 at 6:49

[GoogleCodeExporter]

The > operator there does not behave the way you might expect. In particular 
note that test "6.02.0" > "6.02.1" and even test "6.00.0" > "6.02.1" both 
succeed. I don't know if the test program can do a lexicographic comparison on 
strings, but at least this should work for now:

else if test ${CAMLP5_VERSION} = "6.02.2" -o ${CAMLP5_VERSION} = "6.02.3" ; \

Original comment by ramana.k...@gmail.com on 17 Sep 2011 at 2:20

[GoogleCodeExporter]

Thanks, adopted this change in revision 104.

Original comment by jrh...@gmail.com on 10 Oct 2011 at 1:55

[GoogleCodeExporter]

Still have the same problem in the current svn version of HOL-Light. Solved by 
using camlp5-6.02.0 (camlp5 types were changed after this version, thus 
yielding the above bug).

Original comment by vincent....@gmail.com on 31 Jan 2012 at 9:42

[GoogleCodeExporter]

This needs to be fixed again for camlp5 6.05 (in which case we want 
pa_j_3.1x_6.02.2ml).

Original comment by ramana.k...@gmail.com on 20 Mar 2012 at 11:22

[GoogleCodeExporter]

I ran into same problem with latest version.  Modified make file so that it 
just copied pa_j_3.1x_6.02.2ml -- did this with camlp5-6.05 and the makefile 
succeed and hol_light builds, etc.

Original comment by shlomoba...@gmail.com on 3 May 2012 at 5:57

[GoogleCodeExporter]

I have encountered the reported problem with:
* Ubuntu 12.04 on 64-bit Intel core i7 vPro
* OCaml 3.12.1
* camlp5 6.06 (configured strictly)
* HOL Light rev. 146 (via svn)

I edited the HOL lines 59 & 60 of Makefile to read:

else if test ${CAMLP5_VERSION} = "6.06" -o ${CAMLP5_VERSION} = "6.02.2" -o 
${CAMLP5_VERSION} = "6.06" ; \
then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \

This fixes the reported error, but yields a new one:

File "pa_j.ml", line 247, characters 4-4723:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(ExSpw (_, _)|ExRpl (_, _, _)|ExPar (_, _, _)|ExJdf (_, _, _))
File "pa_j.ml", line 514, characters 4-1928:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
StDef (_, _)

Original comment by c.ro...@espero.org.uk on 8 Jun 2012 at 1:23

[GoogleCodeExporter]

Here is a suggested solution that should solve problems encountered by myself 
and others when using new versions of ocamlp5:

--- Makefile    (revision 146)
+++ Makefile    (working copy)
@@ -56,10 +56,7 @@
         then cp pa_j_${OCAML_VERSION}.ml pa_j.ml ; \
         else if test ${CAMLP5_VERSION} = "6.02.1" ; \
              then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
-             else if test ${CAMLP5_VERSION} = "6.02.2" -o ${CAMLP5_VERSION} = 
"6.02.3" -o ${CAMLP5_VERSION} = "6.05" ; \
-                  then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
-                  else cp pa_j_3.1x_${CAMLP5_BINARY_VERSION}.xx.ml pa_j.ml; \
-                  fi \
+             else cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
              fi \
         fi

Original comment by cris.per...@gmail.com on 13 Jul 2012 at 6:52

[GoogleCodeExporter]

I see this error when building hol_light revision 146, using ocamlc 3.12.1 and 
camlp5 6.06.

Original comment by therealj...@gmail.com on 22 Aug 2012 at 9:24