Stream: Coq devs & plugin devs

Topic: Dune strikes back


view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:14):

I am trying to build Coq 8.16.0+ε and I'm getting a very weird error.

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:14):

File "theories/dune", line 11, characters 3-14:
11 |    ltac_plugin
        ^^^^^^^^^^^
Error: Library "ltac_plugin" not found.
-> required by theory Coq in theories
-> required by _build/default/theories/Init/Prelude.vo
-> required by _build/default/dev/shim/coqtop-prelude

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:14):

I don't remember having had this kind of problems before at the time where this was the master branch, did something change in dune?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:15):

(any non-trivial invocation of the make targets gives this, and I can't build via dune build either)

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:16):

Do the other shims work?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:17):

no, anything that requires the prelude dies

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:17):

(this is on V8.17+alpha tag, but the same issue arises around these commits)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):

Can you reproduce after git clean -fxd ?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:18):

yes

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:18):

even -xffd

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):

what commands are you running?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:18):

make states is the shortest one

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):

Coq commit?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:18):

but dune build -- dev/shim/coqtop-prelude dies as well

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:18):

tag V8.17+alpha

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):

COQ_USE_DUNE envar?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:19):

that that in 8.16 make will not pick Makefile.dune

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:19):

this is set

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:19):

Can you cat theories/dune?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:19):

we're talking 8.17 here so IIRC we're already using dune by default anyways

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:19):

(coq.theory
 (name Coq)
 (package coq-stdlib)
 (synopsis "Coq's Standard Library")
 (flags -q -w -deprecated-native-compiler-option)
 ; (mode native)
 (boot)
 ; (per_file
 ;  (Init/*.v -> -boot))
 (libraries
   ltac_plugin
   tauto_plugin

   cc_plugin
   firstorder_plugin

   number_string_notation_plugin

   btauto_plugin
   rtauto_plugin

   ring_plugin
   nsatz_plugin

   zify_plugin
   micromega_plugin

   funind_plugin

   ssreflect_plugin
   derive_plugin))

(include_subdirs qualified)

(documentation
 (package coq-stdlib))

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:20):

Thats a bit sus, shouldn't these be

(libraries
   coq-core.plugins.ltac
   coq-core.plugins.tauto

   coq-core.plugins.cc
   coq-core.plugins.firstorder

   coq-core.plugins.number_string_notation

   coq-core.plugins.btauto
   coq-core.plugins.rtauto

   coq-core.plugins.ring
   coq-core.plugins.nsatz

   coq-core.plugins.zify
   coq-core.plugins.micromega

   coq-core.plugins.funind

   coq-core.plugins.ssreflect
   coq-core.plugins.derive))

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:20):

I don't think I use the dune cache, at least I never remember having activated it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):

Yes, the problem is that newer dunes require public names in the deps

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:21):

@Ali Caglayan this is the file that is stored in the repo afaict

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):

This is change in dune which was not properly tracked

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):

so either you use older dune, or patch Coq

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):

the change was introduced in the inter-composition PR

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:21):

great

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:22):

tell me about reproducible artifacts

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):

if you use the Dune version in CI thing will work

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):

what do you want to know about reproducible artifacts?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):

You wanna use docker for dev?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:22):

please no

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:22):

Why not just patch the dune file like I said?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):

Then I'm not sure what you mean

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:22):

this is not great for bisecting

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):

that's a bug in Dune tho

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):

use older dune

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):

but yes it is a pita

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):

Dune should not have made that change

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:23):

To be clear, it was a bug and I fixed it but ptotato potatoe.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):

yes you are right actually

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):

it was a bug they live in different packages

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:24):

it was not a bug before the package split

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:24):

the package split is in 8.16 tho?

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:24):

what breaks if I downgrade dune?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:24):

We discussed this indeed, whether Dune lang versioning should preserve bugs is interesting

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:25):

We have still not split the package

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:25):

@Pierre-Marie Pédrot ntohing

view this post on Zulip Pierre-Marie Pédrot (Oct 19 2022 at 21:25):

ok I had the impression we were depending on bleeding edge features

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:25):

Pierre-Marie Pédrot said:

what breaks if I downgrade dune?

I think you can get away with git stash and git stash pop with my patch while bisecting.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:25):

Ali Caglayan said:

We have still not split the package

what do you mean, the problem Pierre-Marie sees is actually due to plugins living in coq-core vs the stdlib living in coq-stdlib

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:26):

Emilio Jesús Gallego Arias said:

Ali Caglayan said:

We have still not split the package

what do you mean, the problem Pierre-Marie sees is actually due to plugins living in coq-core vs the stdlib living in coq-stdlib

At least on opam, there are a myriad of bugs to be found when you install only coq-core.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:26):

That's the problem @Pierre-Marie Pédrot , the file in your checkout uses the plugins private name, Ali is correct that is a bug the moment we put the plugins in a separate package

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:26):

@Pierre-Marie Pédrot our lower bound is 2.9 for now, see dune-project for the version required


Last updated: Feb 01 2023 at 16:03 UTC