Jason Gross (Dec 29 2020 at 20:19): Jason Gross (Dec 29 2020 at 20:19):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 coq-8.8.2 + 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.
Jason Gross (Dec 29 2020 at 20:45):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...
Pierre-Marie Pédrot (Dec 29 2020 at 20:49):IIRC if you load the pa_o.cmo file it should output the human readable syntax.
Pierre-Marie Pédrot (Dec 29 2020 at 20:50):Or maybe the pr_o.cmo instead, I don't remember the details.
Jason Gross (Dec 29 2020 at 21:04):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
Jason Gross (Dec 29 2020 at 21:46):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 .mlg with .ml4
Jason Gross (Dec 29 2020 at 21:47):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
Pierre-Marie Pédrot (Dec 29 2020 at 22:01):The support of ml4 files has been discontinued, hasn't it?
Jason Gross (Dec 29 2020 at 22:03):Yes. But in fact the same issue persists with generated .ml files
Jason Gross (Dec 29 2020 at 22:05):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: Oct 13 2024 at 01:02 UTC