I have some code that depends on a plugin (https://github.com/coq-community/coq-performance-tests/pull/9). This code builds fine on my local machine (WSL OCaml 4.06.1+fp installed via opam + Coq 8.8.2 built from sources), but on the CI and on my VM running Ubuntu 16.04, with Coq 8.8.2 + OCaml 4.02.3 installed from the
libcoq-8.8.2-ocaml-dev packages on
ppa:jgross-h/many-coq-versions I get a syntax error on https://github.com/coq-community/coq-performance-tests/blob/b63467d49c2e669335d9e14c260f6eb3750454cb/PerformanceExperiments/Reify/OCaml.v#L9-L12 (that
[ is not valid after a constr) which suggests to me that the syntax extension from the plugin (https://github.com/coq-community/coq-performance-tests/blob/ocaml-reify/PerformanceExperiments/Reify/reify_plugin.ml4.v88 loaded at https://github.com/coq-community/coq-performance-tests/blob/b63467d49c2e669335d9e14c260f6eb3750454cb/PerformanceExperiments/Reify/OCamlReify.v#L3 via https://github.com/coq-community/coq-performance-tests/blob/ocaml-reify/PerformanceExperiments/Reify/reify.mlpack) is not being loaded. I saw @Beta Ziliani 's message about porting this code to 8.12 and getting similar issues, but that seems to have been about the
DECLARE PLUGIN which seems to be fine in this code (and in any case this behavior seems to depend on either the version of OCaml or something weirder like what machine I built Coq on). I'm going to see if I can reproduce the issue with OCaml 4.02.3 on my local machine, but any help here would be greatly appreciated.
I'm wondering if maybe it's an issue with camlp5 versions... is there a way to get readable preprocessed output?
/home/jgross/.opam/4.06.1+fp/bin/camlp5o -I /home/jgross/.opam/4.06.1+fp/lib/ocaml -I "/home/jgross/.local64/coq/coq-8.8.2/lib/coq//grammar" pa_extend.cmo q_MLast.cmo pa_macro.cmo grammar.cma -loc loc -impl PerformanceExperiments/Reify/reify_plugin.ml4 is giving me something that's mostly binary...
IIRC if you load the pa_o.cmo file it should output the human readable syntax.
Or maybe the pr_o.cmo instead, I don't remember the details.
I think I've tracked down the issue, at least most of the way:
coqdep emits incorrect output for .mlpack files when the .ml4 files required are generated
Yeash, and apparently the only reason my code works fine on master is because when you do
-include foo_bar.mlg.d foo.mlpack.d, GNU make will try to remake
foo_bar.mlg.d before it tries to make
foo.mlpack.d, whereas this is for whatever reason not the case if you replace
Oh, I guess it's actually due to
GENMLFILES:=$(MLGFILES:.mlg=.ml) $(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES)
Reported as https://github.com/coq/coq/issues/13690
The support of ml4 files has been discontinued, hasn't it?
Yes. But in fact the same issue persists with generated .ml files
Suppose you have a file
foo.v which depends on a plugin in
bar.mlpack which uses code in
bar.ml extracted from
bar.v which depends on a plugin in
baz.mlpack which uses code in
baz.ml extracted from
baz.v... I think there is not currently a way to get
make to work with this setup without hardcoding the dependency chain in the
Makefile.coq.local (or similar) file
Last updated: Jun 10 2023 at 06:31 UTC