I am trying to build Coq 8.16.0+ε and I'm getting a very weird error.
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?
(any non-trivial invocation of the make targets gives this, and I can't build via dune build either)
Do the other shims work?
no, anything that requires the prelude dies
(this is on V8.17+alpha tag, but the same issue arises around these commits)
Can you reproduce after git clean -fxd
?
yes
even -xffd
what commands are you running?
make states
is the shortest one
Coq commit?
but dune build -- dev/shim/coqtop-prelude
dies as well
tag V8.17+alpha
COQ_USE_DUNE envar?
that that in 8.16 make
will not pick Makefile.dune
this is set
Can you cat theories/dune?
we're talking 8.17 here so IIRC we're already using dune by default anyways
(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
Yes, the problem is that newer dunes require public names in the deps
@Ali Caglayan this is the file that is stored in the repo afaict
This is change in dune which was not properly tracked
so either you use older dune, or patch Coq
the change was introduced in the inter-composition PR
great
tell me about reproducible artifacts
if you use the Dune version in CI thing will work
what do you want to know about reproducible artifacts?
You wanna use docker for dev?
please no
Why not just patch the dune file like I said?
Then I'm not sure what you mean
this is not great for bisecting
that's a bug in Dune tho
use older dune
but yes it is a pita
Dune should not have made that change
To be clear, it was a bug and I fixed it but ptotato potatoe.
yes you are right actually
it was a bug they live in different packages
it was not a bug before the package split
the package split is in 8.16 tho?
what breaks if I downgrade dune?
We discussed this indeed, whether Dune lang versioning should preserve bugs is interesting
We have still not split the package
@Pierre-Marie Pédrot ntohing
ok I had the impression we were depending on bleeding edge features
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.
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
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 thestdlib
living incoq-stdlib
At least on opam, there are a myriad of bugs to be found when you install only coq-core.
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
@Pierre-Marie Pédrot our lower bound is 2.9 for now, see dune-project
for the version required
Last updated: Oct 13 2024 at 01:02 UTC