Pierre-Marie Pédrot (Oct 19 2022 at 21:14): 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.
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
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?
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)
Ali Caglayan (Oct 19 2022 at 21:16):Do the other shims work?
Pierre-Marie Pédrot (Oct 19 2022 at 21:17):no, anything that requires the prelude dies
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)
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):Can you reproduce after git clean -fxd ?
Pierre-Marie Pédrot (Oct 19 2022 at 21:18):yes
Pierre-Marie Pédrot (Oct 19 2022 at 21:18):even -xffd
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):what commands are you running?
Pierre-Marie Pédrot (Oct 19 2022 at 21:18):make states is the shortest one
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):Coq commit?
Pierre-Marie Pédrot (Oct 19 2022 at 21:18):but dune build -- dev/shim/coqtop-prelude dies as well
Pierre-Marie Pédrot (Oct 19 2022 at 21:18):tag V8.17+alpha
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:18):COQ_USE_DUNE envar?
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:19):that that in 8.16 make will not pick Makefile.dune
Pierre-Marie Pédrot (Oct 19 2022 at 21:19):this is set
Ali Caglayan (Oct 19 2022 at 21:19):Can you cat theories/dune?
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
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))
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))
I don't think I use the dune cache, at least I never remember having activated it
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):Yes, the problem is that newer dunes require public names in the deps
Pierre-Marie Pédrot (Oct 19 2022 at 21:21):@Ali Caglayan this is the file that is stored in the repo afaict
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):This is change in dune which was not properly tracked
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):so either you use older dune, or patch Coq
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:21):the change was introduced in the inter-composition PR
Pierre-Marie Pédrot (Oct 19 2022 at 21:21):great
Pierre-Marie Pédrot (Oct 19 2022 at 21:22):tell me about reproducible artifacts
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):if you use the Dune version in CI thing will work
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):what do you want to know about reproducible artifacts?
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):You wanna use docker for dev?
Pierre-Marie Pédrot (Oct 19 2022 at 21:22):please no
Ali Caglayan (Oct 19 2022 at 21:22):Why not just patch the dune file like I said?
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):Then I'm not sure what you mean
Pierre-Marie Pédrot (Oct 19 2022 at 21:22):this is not great for bisecting
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:22):that's a bug in Dune tho
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):use older dune
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):but yes it is a pita
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):Dune should not have made that change
Ali Caglayan (Oct 19 2022 at 21:23):To be clear, it was a bug and I fixed it but ptotato potatoe.
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):yes you are right actually
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:23):it was a bug they live in different packages
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:24):it was not a bug before the package split
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:24):the package split is in 8.16 tho?
Pierre-Marie Pédrot (Oct 19 2022 at 21:24):what breaks if I downgrade dune?
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:24):We discussed this indeed, whether Dune lang versioning should preserve bugs is interesting
Ali Caglayan (Oct 19 2022 at 21:25):We have still not split the package
Emilio Jesús Gallego Arias (Oct 19 2022 at 21:25):@Pierre-Marie Pédrot ntohing
Pierre-Marie Pédrot (Oct 19 2022 at 21:25):ok I had the impression we were depending on bleeding edge features
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.
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
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-corevs thestdlibliving incoq-stdlib
At least on opam, there are a myriad of bugs to be found when you install only coq-core.
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
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: Apr 19 2024 at 19:02 UTC