Another error in pa_j.ml

GoogleCodeExporter commented 9 years ago

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.

Original issue reported on code.google.com by gyorokpe...@freemail.hu on 2 Apr 2011 at 4:31

GoogleCodeExporter commented 9 years ago

I have the same problem on 
MacOS X 10.6 
Ocaml : 3.12
Camlp5 : 6.02.2

Original comment by denghao8...@gmail.com on 8 May 2011 at 3:05

GoogleCodeExporter commented 9 years ago

I solved it by use ocaml 3.0.9
read the tutorial carefully.

Original comment by denghao8...@gmail.com on 8 May 2011 at 3:13

GoogleCodeExporter commented 9 years ago

I have the same problem on Ubuntu 11.10, which only has ocaml 3.12.0 and camlp5 
6.02.2 in its repositories. 

I realize that I could build historic version of ocaml to work around this 
issue. However, judging by the text on the HOL light homepage, it should be 
possible to build HOL light using ocaml 3.12.0 if camlp5 is installed. So, how 
can I resolve this issue without downgrading ocaml?

Original comment by fe...@fbreuer.de on 17 Oct 2011 at 4:08

GoogleCodeExporter commented 9 years ago

This is a puzzling situation. On two machines at work I'm using the
following combinations, both of which seem to work fine:

* Ocaml 3.12.0 and camlp5 6.02.2 in Windows 7 under Cygwin

* OCaml 3.12.1 (actually 3.12.1+ocamlnatjit2 but I doubt if that makes a
  difference) and camlp5 6.02.3, under Ubuntu Lucid.

Since others seem to be seeing failures with what looks like the same
or a very similar combination, what could account for the difference?

 * Maybe people are not using such a recent revision of HOL Light. I'm
   using versions around r100-r106, and some of the recent changes are
   relevant to building under recent OCaml / camlp5 combinations.

 * In both cases I believe I built camlp5 in "strict" mode (i.e.
   started the camlp5 build with ./configure --strict). If you
   used "transitional" mode, something could be different. I'm
   not sure what you get if you just install the package.

 * I built both OCaml and camlp5 myself, and the binaries are in
   /usr/local/bin/..., which is on my $PATH.

Original comment by jrh...@gmail.com on 17 Oct 2011 at 11:04

GoogleCodeExporter commented 9 years ago

I'd like to add a positive data point: on a Debian wheezy system with Ocaml 
3.12.0 and camlp5 6.02.2, I was getting the error message in the original post.

Recompiling the same Debian package for camlp5 while adding -strict to the 
configure script resolves the error. In other words, the default build for the 
Debian (and I suppose Ubuntu) packages for camlp5 use transitional mode, and 
transitional somehow breaks HOL light.

Original comment by Nikos.Go...@gmail.com on 31 Oct 2011 at 7:39

GoogleCodeExporter commented 9 years ago

I now succeeded building HOL Light on Cygwin under Windows 7.

* I used the Cygwin package of OCaml 3.12.0.
* I built Camlp5 6.02.3 myself using ./configure --strict.
* Then I built the current svn version of HOL Light successfully (using 
pa_j_3.1x_6.02.2.ml).

So I can confirm Nikos observation that Camlp5 has to be built in --strict mode.

Original comment by fe...@fbreuer.de on 15 Dec 2011 at 10:44

GoogleCodeExporter commented 9 years ago

I have been using OCaml 3.11.2 with camlp5 6.02.1 for quite a while because it 
was the only combination I could get built on Fedora 15 with the versions of 
hol that were current when I tried.  

But I tried again now and found I can build the current hol okay with the 
Fedora 15 OCaml 3.12 and camlp5 6.02,3-1 (most current version with the patch) 
built in strict mode.

Original comment by calvin.o...@gmail.com on 19 Dec 2011 at 11:54

CJex / hol-light

Another error in pa_j.ml #3