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
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