CJex / hol-light

HOL Light is an interactive theorem prover / proof checker. Automatically exported from code.google.com/p/hol-light
Other
1 stars 0 forks source link

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

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
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

Original issue reported on code.google.com by ondrej.k...@gmail.com on 16 Nov 2010 at 11:00

GoogleCodeExporter commented 9 years ago
Should be fixed in revision 67.

Original comment by jrh...@gmail.com on 3 Dec 2010 at 3:34

GoogleCodeExporter commented 9 years ago
i just checked out revision 79 and tried make with ocaml 3.12.0 and camlp5 6.00 
and i got a similar error:

<W> Grammar extension: in [str_item], some rule has been masked
<W> Grammar extension: in [expr], some rule has been masked
<W> Grammar extension: in [expr], some rule has been masked
<W> Grammar extension: in [expr], some rule has been masked
<W> Grammar extension: in [expr], some rule has been masked
File "pa_j.ml", line 2672, characters 19-23:
While expanding quotation "ctyp":
Parse error: illegal begin of ctyp_eoi
File "pa_j.ml", line 1, characters 0-1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2

Original comment by joe.pl...@gmail.com on 2 Mar 2011 at 2:26

GoogleCodeExporter commented 9 years ago
Thanks for the report; I'll look into it. Did you build camlp5 yourself,
and if so did you do so in "strict" or "transitional" mode?

Original comment by jrh...@gmail.com on 7 Mar 2011 at 7:14

GoogleCodeExporter commented 9 years ago
Had the exact same problem as ondrej on Mac OS 10.5, with OCaml 3.12 and camlp5 
6.02.3, hol_light revision 90.

Copying pa_j_3.1x_6.02.2.ml over pa_j.ml seems to solve the problem. 
(pa_j_3.1x_6.xx.ml did not)

Original comment by rus...@eecs.qmul.ac.uk on 13 Jun 2011 at 12:16

GoogleCodeExporter commented 9 years ago
Problem in same area.  Had hol light working okay in earlier version, but tried 
to build in newly installed Fedora 15, with OCaml 3.12 and camlp5 6.02.3 both 
strict and transitional, hol light revision 92, 

ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 
pa_j.ml;

gives

File "pa_j.ml", line 153, characters 8-23:
Error: Unbound constructor TyXtr

My understanding is that one is not supposed to access the syntax tree directly 
with the constructors, and it seems that TyXtr is no longer there?

I don't understand how you (comment 4) got around this, since none of the pa_j 
work for me. 

Original comment by calvin.o...@gmail.com on 24 Jun 2011 at 2:55

GoogleCodeExporter commented 9 years ago
[deleted comment]
GoogleCodeExporter commented 9 years ago
[deleted comment]
GoogleCodeExporter commented 9 years ago
[deleted comment]
GoogleCodeExporter commented 9 years ago
[deleted comment]
GoogleCodeExporter commented 9 years ago
I am trying to build rev 106 on Ubuntu 11.10 using ocaml 3.12.0 and camlp5 
6.02.2. No matter which pa_j.ml I try, I always get an error of this form:

felix@VirtualBox:~/hol_light$ 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 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
make: *** [pa_j.cmo] Error 2

Original comment by fe...@fbreuer.de on 17 Oct 2011 at 3:24

GoogleCodeExporter commented 9 years ago
Sorry about the last comment. It is a duplicate of issue 3.

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