Stream: Coq devs & plugin devs

Topic: dune build woes


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Oct 28 2022 at 16:55):

I take it you are using dune 3.4?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Oct 28 2022 at 16:57):

That was fixed, and the correct name would be coq-core.plugins.ltac.

view this post on Zulip Ali Caglayan (Oct 28 2022 at 16:57):

So either downgrade Dune to 3.3 or rename the plugins in the file.

view this post on Zulip 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!

view this post on Zulip Ramkumar Ramachandra (Oct 28 2022 at 17:01):

Any hints about why I didn't have to dune clean earlier? Am I misremembering?


Last updated: Feb 06 2023 at 19:03 UTC