The Coq mailing list

[Matej Košík <matej.kosik AT inria.fr>]

Hi,

(I failed to find a suitable bug category in our bugzilla for this, so I am 
posting here)

If I do

        grammar/vernacextend.mlp

and then

        VERBOSE=1 make coqide

This is what happens:

        make --warn-undefined-variable --no-builtin-rules -f Makefile.build 
coqide
        make[1]: Entering directory 'SOME_DIR'
        "/home/me/.opam/4.02.3/bin/ocamlfind" ocamlc -rectypes -bin-annot -g  
-I "/home/me/.opam/4.02.3/lib/camlp5" -I grammar -c -pp 
'"/home/me/.opam/4.02.3/bin/camlp5o" -I
"/home/me/.opam/4.02.3/lib/camlp5"  pa_extend.cmo q_MLast.cmo pa_macro.cmo 
-DOCAML402 -loc loc -impl' -impl grammar/vernacextend.mlp
        "/home/me/.opam/4.02.3/bin/ocamlfind" ocamlc -rectypes -bin-annot -g  
-I "/home/me/.opam/4.02.3/lib/camlp5" -I grammar -pp 
'"/home/me/.opam/4.02.3/bin/camlp5o" -I "/home/me/.opam/4.02.3/lib/camlp5"
grammar/gramCompat.cmo grammar/q_util.cmo grammar/argextend.cmo 
grammar/tacextend.cmo grammar/vernacextend.cmo -impl' -impl grammar/test.mlp 
-o grammar/test
        "/home/me/.opam/4.02.3/bin/ocamlfind" ocamlc -rectypes -bin-annot -g  
-I "/home/me/.opam/4.02.3/lib/camlp5" -I grammar grammar/gramCompat.cmo 
grammar/q_util.cmo grammar/argextend.cmo
grammar/tacextend.cmo grammar/vernacextend.cmo -linkall -a -o 
grammar/grammar.cma
        make[1]: Nothing to be done for 'coqide'.
        make[1]: Leaving directory 'SOME_DIR'

I do not think this is enough.
I guess it would make sense to regenerate all "*.ml" files that were 
generated from "*.ml4" using (macros defined in) grammar/grammar.cma, 
wouldn't it?
It seems as if there were a missing dependency.
(e.g. "plugins/extraction/g_extraction.ml" should depend also on 
"grammar/grammar.cma").
-- 
Matej Košík