The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

The error message says that Pcoq.Gram is somewhat wrong. I could
verify empirically that doing "open Pcoq" first then "GEXTEND Gram
..." makes camlp5 happy.

The Camlp5 manual (
http://camlp5.gforge.inria.fr/doc/pdf/camlp5-6.00.pdf ) says (page 61)
that the module name after GEXTEND can be a "qualid" (I assume a
qualified module name), but the sources of camlp5 6.14
(meta/pa_extend.ml, line 1052) would seem confirm that just an uppercase
identifier (not a long path) is expected.

I don't understand why this would work with some other configuration.
On my machine, camlp4 (rather than camlp5) accepts the version using
"EXTEND Pcoq.Gram" (so it support reading full module paths here), but
complains than "GEXTEND" is deprecated syntax, which seems to rule out
the hypothesis that your system OCaml setup is using camlp4 instead
(unless your camlp4 was debian-patched to preserve Coq compatibility
or what not).

On Fri, Oct 2, 2015 at 2:03 PM, Beta Ziliani 
<beta AT mpi-sws.org>
 wrote:
> I should add that the minimal example is precisely the code that I wrote:
>
> GEXTEND Pcoq.Gram
> GLOBAL: myproof_instr;
>   myproof_instr :
>     [[ c=Pcoq.Constr.operconstr ; "." -> MyInstr.my_constr c ]];
> END
>
>
> With Ocaml installed in /usr/bin it fails complaining about myproof_instr
> not being defined, while in .opam's Ocaml it fails at the preprocessor
> level.
>
> Thanks,
> Beta
>
>
> On Thu, Oct 1, 2015 at 5:16 PM, Beta Ziliani 
> <beta AT mpi-sws.org>
>  wrote:
>>
>> Hi list,
>>
>> I have the following issue that is driving me nuts. I have two Ubuntu
>> boxes with practically the same setup. I have a plugin for Coq 8.5 beta 2.
>> However, I can compile it in one machine but not on the other. In the
>> machine where it works, I have OCaml installed in the system (as in
>> /usr/bin), while on the other is in .opam.  The error in the second machine
>> is:
>>
>> File "src/myfile.ml4", line 92, characters 13-14:
>> Parse error: [global] or [entry] expected after uppercase identifier (in
>>   [gextend_body])
>> File "src/myfile.ml4", line 1:
>> Error: Error while running external preprocessor
>>
>> That line is:
>> GEXTEND Pcoq.Gram
>> GLOBAL: myproof_instr;
>>   myproof_instr :
>>     [[ c=Pcoq.Constr.operconstr ; "." -> MyInstr.my_constr c ]];
>> END
>>
>>
>> When compiling Coq, the ./configure -local script outputs the text below,
>> where XXX is replaced by specific locations for OCaml: /usr/bin (or lib) 
>> for
>> one machine, and .opam in the other.
>>
>> Any ideas?
>>
>> Thanks!
>> Beta
>>
>> ---
>> You have GNU Make 3.81. Good!
>> You have OCaml 4.02.3. Good!
>> You have Camlp5 6.14. Good!
>> You have native-code compilation. Good!
>> No such directory '/home/beta/.opam/4.02.3/lib/ocaml/lablgtk2' (in OCaml
>> library).
>> LablGtk2 not found:
>> => no CoqIde will be built.
>>
>>   Architecture                : Linux
>>   Coq VM bytecode link flags  : -dllib -lcoqrun -dllpath
>> /home/beta/coq/coq8.5b2/coq-8.5beta2/kernel/byterun
>>   Other bytecode link flags   :
>>   OS dependent libraries      : -cclib -lunix
>>   OCaml version               : 4.02.3
>>   OCaml binaries in           : XXX
>>   OCaml library in            : XXX
>>   Camlp5 version              : 6.14
>>   Camlp5 binaries in          : /home/beta/.opam/4.02.3/bin
>>   Camlp5 library in           : /home/beta/.opam/4.02.3/lib/camlp5
>>   Native dynamic link support : true
>>   CoqIde                      : no
>>   Documentation               : None
>>   Web browser                 : firefox -remote "OpenURL(%s,new-tab)" ||
>> firefox %s &
>>   Coq web site                : http://coq.inria.fr/
>>
>