pa_j.ml: parse error after upgrade to ocaml 3.12 and camlp5 6.02

kx@linux:~/tmp/hol_light_svn> make
if test `ocamlc -version | cut -c3` = "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 1689, characters 37-56:
While expanding quotation "class_expr":
Parse error: ']' or [expr] expected after '[' (in [expr])
File "pa_j.ml", line 1, characters 0-1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2

What steps will reproduce the problem?
1. Install the Windows version of OCaml
2. Download Camlp5 and apply all 3 patches, "configure", "make" and "make 
install"
3. Download the HOL Light source and try to "make" it

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

File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
       but is here used with type ('a * MLast.ctyp) list Ploc.vala
make: *** [pa_j.cmo] Error 2


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

Windows 7 Professional
OCaml: 3.11.0, MinGW port
Camlp5: 6.02.2-3
HOL Light: revision 86
MSys to run patch, make etc.

Please provide any additional information below.

Documentation of new_type's FAILURE CONDITIONS contains a grammar error (or a 
grammar mistake): "Fails if HOL is there is already a type operator..."

Here's a patch to the print_to_string function that accesses the current line 
length using a call to get_margin before printing the argument to a string. I 
also recoded the print_to_string function in terms of ocaml buffers, instead of 
a string reference.

The patchfile can be applied using the command

patch -p0 < patchfile

Exception: Failure "new_definition: term not closed: V, Fn".
Error in included file /home/blanqui/src/hol-light/Logic/canon.ml

real	1m4,107s

What steps will reproduce the problem?
1. Install camlp5-6.12 (released 2014-09-19)
2. Checkout the source of hol-light (revision 199)
3. Run `make`

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

The compilation fails, because the wrong file was copied to `pa_j.ml`.

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

hol-light r199 on linux x86_64 with ocaml 4.01.0 and camlp5 6.12

Please provide any additional information below.

utop # t1;;
- : term = `\x. s x`
utop # x1, type_of x1;;
- : term * hol_type = (`x`, `:A->bool`)
utop # let s1 = frees t1 |> hd;;
val s1 : term = `s`
utop # instantiate (term_match [] s1 x1) t1;;
- : term = `\x. x x`

utop # t2;;
- : term = `\x. s + x`
utop # x2, type_of x2;;
- : term * hol_type = (`x`, `:num`)
utop # let s2 = frees t2 |> hd;;
val s2 : term = `s`
utop # instantiate (term_match [] s2 x2) t2;;
- : term = `\x'. x + x'`

I installed OCaml 4.00.0 and camlp5 using GODI a while back. Today, I checked 
out the hol-light sources, but when I tried building them I got the following 
error:

File "pa_j.ml", line 13, characters 0-10:
Error: Unbound module Pcaml
make: *** [pa_j.cmo] Error 2

After a bit of searching, I found that ocamlc treats the `-I +foo` argument as 
`-I /usr/lib/ocaml/foo`:
http://stackoverflow.com/questions/3848897/unbound-modules-in-ocaml

As it turns out, GODI installs camlp5 in a non-standard location. On this 
machine (Ubuntu 12.04.1 x86), `which camlp5` returns:
/opt/godi/bin/camlp5

So, I tweaked the Makefile a bit to make it more robust (see the attached 
diff). camlp4 and camlp5 both support the "-where" option, so I've used that 
within backticks along with the -I option when invoking ocamlc. This makes it 
so camlp4/camlp5 will be included properly no matter where it's installed on 
the system.

Cheers,
Jack

^

Chapter 11 (Page 74, file 'tutorial_220.pdf'); is "far from a a simple", should 
be "far from a simple".

Reference manual of REWRITE_CONV points to undocumented SUBST_CONV.

What steps will reproduce the problem?
1. Install the Windows version of OCaml
2. Download Camlp5 and apply all 3 patches, "configure", "make" and "make 
install"
3. Download the HOL Light source and try to "make" it

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

File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
       but is here used with type ('a * MLast.ctyp) list Ploc.vala
make: *** [pa_j.cmo] Error 2


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

Windows 7 Professional
OCaml: 3.11.0, MinGW port
Camlp5: 6.02.2-3
HOL Light: revision 86
MSys to run patch, make etc.

Please provide any additional information below.

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

In few places in the documentation "i.e." is followed by extra comma (,).

Attached patch makes the punctuation consistent with "e.g." and other uses 
"i.e.".

The attached patch documents failure conditions of 'is_hidden'.

What steps will reproduce the problem?
1. svn checkout
2. make
3.

What is the expected output? What do you see instead?
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)


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

Please provide any additional information below.
This patch seems to solve the problem

Index: Makefile
===================================================================
--- Makefile    (revision 146)
+++ Makefile    (working copy)
@@ -56,7 +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" ; \
+             else if test ${CAMLP5_VERSION} = "6.02.2" -o ${CAMLP5_VERSION} = 
"6.02.3" -o ${CAMLP5_VERSION} = "6.05" -o ${CAMLP5_VERSION} = "6.06" ; \
                   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 \

Its presence here https://github.com/jbem/dead-souls suggests that the project 
is abandoned. The link on the hol-light home page (and google code page) is 
broken.

 File "pa_j.ml", line 571, characters 6-18:
Error: The constructor StTyp expects 3 argument(s),
       but is applied here to 2 argument(s)

There are three semicolons instead of two in the documentation of SPECL (typo). 
Patch attached.

$ make
$ ocaml
# #use "hol.ml";;
val hol_version : string = "2.20++"
val hol_dir : string ref = {contents = "/home/asr/src/hol-light"}
val temp_path : string ref = {contents = "/tmp"}
Cannot find file camlp5o.cma.
- : unit = ()
Exception: Symtable.Error _.

$ ocaml -I `camlp5 -where` camlp5o.cma

$ ocaml

$ ocaml --version
The OCaml toplevel, version 4.03.0

$ camlp5 -v
Camlp5 version 6.16 (ocaml 4.03.0)

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.

This causes user pretty-printers to print directly to the console, instead of 
the correct destination known to the formatter (e.g., a target string in 
string_of_term).

I attach a patchfile that fixes this that can be applied using the command 

patch -p0 < patchfile

Note: it changes the type of user pretty-printers by adding the formatter as an 
argument, so existing user pretty-printers will need to be updated.

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.

Documentation for GEN_REWRITE_TAC seems to be copied from HOL4, but in HOL 
Light this tactic takes only two arguments, not three. Patch attached.

Patch attached.

[jt273@lancing 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" ; \
                       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
cp: cannot stat ‘pa_j_3.1x_9.xx.ml’: No such file or directory
Makefile:58: recipe for target 'pa_j.ml' failed
make: *** [pa_j.ml] Error 1

#use "hol.ml";;
# module OrdInt = struct type t = int let compare = (-) end;;
Toplevel input:
# module OrdInt = struct type t = int let compare = (-) end;;
         ^^^^^^
Parse error: 'type' or 'rec' expected after 'module' (in [str_item])

The attached patch fixes a minor issue in two help descriptions.

As in the summary.

What steps will reproduce the problem?
1. load ocaml and hol.ml as usual
2. loadt "Library/analysis.ml";;
3. loadt "Multivariate/vectors.ml";;

What is the expected output? What do you see instead?
Expecting exit with no problems.  Instead, it exits with the final lines:

val DOT_RMUL : thm = |- !c x y. x dot c % y = c * (x dot y)
Warning: inventing type variables
Exception: Failure "GEN_TAC".
Error in included file 
/home/ivan/Dropbox/ReadSterling/hol_light/Multivariate/vectors.ml
val it : unit = ()


What version of the product are you using? On what operating system?
2.20++ , Linux Mint


Please provide any additional information below.

It appears that the "--" defined in analysis.ml conflicts somehow with the "--" 
defined in realax.ml , or I may be completely off.

Several code examples in documentation contain extra space after "#" char. 
Patch attached.

There are some minor issues with set_goal package documentation, e.g. missing 
cross-references and extra space. Patch attached.

What steps will reproduce the problem?

Execute these commands:
# needs "Examples/prog.ml";;
# install_parser ("correct",parse_program_assertion);;
# g `correct
     T
       var x;
       x := 1
       end
     x > 0`;;
# e VC_TAC;;

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

VC_TAC should generate verification conditions `1 > 0`, but it leaves the goal 
unmodified.

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

HOL Light from SVN, revision 200; ocaml 4.01.0, Linux

Please provide any additional information below.

VC_TAC works as expected if I introduce a dummy variable:

# g `correct T var x, dummy; x := 1 end x > 0`;;

`correct
         T
          var m,n;
        do  [invariant 0<=m ; measure m]
              (if 0<n then n:=0;
               m:= PRE m)
              while 0<m
      end
     n=0`;;

`m' = m /\ n' = n /\ ~(0 < n)
 ==> 0 <= PRE m /\ MEASURE (\(m,n). m) (PRE m,n) (m',n')`

`m' = m /\ n' = n /\ 0 < n
 ==> 0 <= PRE m /\ MEASURE (\(m,n). m) (PRE m,0) (m',n')`

`~(0 < m) /\ 0 <= m ==> n = 0`

`WF (MEASURE (\(m,n). m))`

`correct ((\(m,n). T) AND (\s. X = (\(m,n). m) s))
 (IF (\(m,n). 0 < n) (Assign (\(m,n). m,0)) Seq Assign (\(m,n). PRE m,n))
 ((\(m,n). 0 <= m) AND (\s. (\(m,n). m) s < X))`

`~(0 < m) /\ 0 <= m ==> n = 0`