Ramkumar Ramachandra (Oct 28 2022 at 16:40): Ramkumar Ramachandra (Oct 28 2022 at 16:40):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?
Ramkumar Ramachandra (Oct 28 2022 at 16:41):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.
Ramkumar Ramachandra (Oct 28 2022 at 16:43):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.
Ali Caglayan (Oct 28 2022 at 16:55):I take it you are using dune 3.4?
Ali Caglayan (Oct 28 2022 at 16:56):The coq repo in pre 8.16 was relying on a bug in the Coq support for Dune
Ali Caglayan (Oct 28 2022 at 16:56):The bug is that you were able to put private lib names in the plugins/(libraries) field of the stanza
Ali Caglayan (Oct 28 2022 at 16:57):That was fixed, and the correct name would be coq-core.plugins.ltac.
Ali Caglayan (Oct 28 2022 at 16:57):So either downgrade Dune to 3.3 or rename the plugins in the file.
Ramkumar Ramachandra (Oct 28 2022 at 16:58):Renaming the plugins in the file across revisions isn't an option, but I can downgrade to 3.3. Thanks for the insight!
Ramkumar Ramachandra (Oct 28 2022 at 17:01):Any hints about why I didn't have to dune clean earlier? Am I misremembering?
Ramkumar Ramachandra (Oct 28 2022 at 17:03):Okay, I'm on dune 3.3 now, and I'm getting the same error :/
Ramkumar Ramachandra (Oct 28 2022 at 17:08):Okay, works with 3.2.
Notification Bot (Oct 28 2022 at 18:00):Ramkumar Ramachandra has marked this topic as resolved.
Last updated: Jun 09 2023 at 08:01 UTC