Hi. I'm attempting to bisect the coq source tree for a bug, and I noticed that dune build coq-core.install coq-stdlib.install
fails on some revisions with
File "theories/dune", line 11, characters 3-14:
11 | ltac_plugin
^^^^^^^^^^^
Error: Library "ltac_plugin" not found.
Any insights into what's going on?
Another annoyance that didn't seem to be there before: I have to dune clean
before every build, otherwise the stdlib is compiled with the wrong version of coq.
I recall running git bisect
on ~8.14 smoothly with a simple dune build; dune exec -- coqc -q bug.v
. That doesn't seem to do the trick anymore.
I take it you are using dune 3.4?
The coq repo in pre 8.16 was relying on a bug in the Coq support for Dune
The bug is that you were able to put private lib names in the plugins/(libraries) field of the stanza
That was fixed, and the correct name would be coq-core.plugins.ltac
.
So either downgrade Dune to 3.3 or rename the plugins in the file.
Renaming the plugins in the file across revisions isn't an option, but I can downgrade to 3.3. Thanks for the insight!
Any hints about why I didn't have to dune clean
earlier? Am I misremembering?
Okay, I'm on dune 3.3 now, and I'm getting the same error :/
Okay, works with 3.2.
Ramkumar Ramachandra has marked this topic as resolved.
Last updated: Sep 25 2023 at 14:01 UTC