I'm getting a Dynlink failure when building quickchick with coq.dev on my machine, whereas quickchick CI is green. Any ideas where I could look? It seems to not find coq-core.printing
(which would be where undefined symbol in the dynlink error is defined); I have tried making that dependency explicit in the plugin's libraries
field or the coq.theory
's plugins
field but it doesn't help. Somehow using (coq 0.8)
in my dune config fixes it, but it requires me to list transitive dependencies so I'd rather avoid that if possible.
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/sam/.opam/coq-dev/lib/coq/../coq-core/../coq-quickchick/plugin/quickchick_plugin.cmxs: undefined symbol: camlPrinter.safe_gen_2436\")")
how did you install coq?
with opam, in its own switch, I've just done an opam upgrade
to get the latest commit, and I'm trying to dune build
in the quickchick repository.
I guess you didn't forget to eval opam env?
What's the dune version?
I haven't forgotten! Dune 3.14.2
maybe there's a bug in the dependency inference? does anything change if you add an explicit coq-core.vernac
to https://github.com/QuickChick/QuickChick/blob/master/plugin/dune#L6 ?
no change.
IDK then
btw maybe this would be better targetted at the dune stream rather than coq devs stream
Indeed that's a bit bizarre due to that library being already linked into Coq, IIANM. Dune doesn't do a lot of special things.
I agree that should be better handled in the dune stream.
What's the diff on the build log _build/log
when you bump to 0.8 Dune lang? Can you post the line that fails from your dune log?
Feel free to move it. Here are the two relevant commands from the logs with a bit of manual prettyfying. The failing one, vs the good one. The only difference seems to be the extra -Q
libraries in the good one.
$ (cd _build/default && /home/sam/.opam/coq-dev/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand
-I /home/sam/.opam/coq-dev/lib/coq-core/boot
-I /home/sam/.opam/coq-dev/lib/coq-core/clib
-I /home/sam/.opam/coq-dev/lib/coq-core/config
-I /home/sam/.opam/coq-dev/lib/coq-core/engine
-I /home/sam/.opam/coq-dev/lib/coq-core/gramlib
-I /home/sam/.opam/coq-dev/lib/coq-core/interp
-I /home/sam/.opam/coq-dev/lib/coq-core/kernel
-I /home/sam/.opam/coq-dev/lib/coq-core/lib
-I /home/sam/.opam/coq-dev/lib/coq-core/library
-I /home/sam/.opam/coq-dev/lib/coq-core/parsing
-I /home/sam/.opam/coq-dev/lib/coq-core/perf
-I /home/sam/.opam/coq-dev/lib/coq-core/plugins/extraction
-I /home/sam/.opam/coq-dev/lib/coq-core/plugins/ltac
-I /home/sam/.opam/coq-dev/lib/coq-core/pretyping
-I /home/sam/.opam/coq-dev/lib/coq-core/printing
-I /home/sam/.opam/coq-dev/lib/coq-core/proofs
-I /home/sam/.opam/coq-dev/lib/coq-core/tactics
-I /home/sam/.opam/coq-dev/lib/coq-core/vernac
-I /home/sam/.opam/coq-dev/lib/coq-core/vm
-I /home/sam/.opam/coq-dev/lib/findlib
-I /home/sam/.opam/coq-dev/lib/zarith
-I /home/sam/.opam/coq-dev/lib64/dynlink
-I /home/sam/.opam/coq-dev/lib64/str
-I /home/sam/.opam/coq-dev/lib64/threads
-I /home/sam/.opam/coq-dev/lib64/unix
-I plugin
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/btauto
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/cc
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/derive
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/extraction
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/firstorder
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/funind
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ltac
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ltac2
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ltac2_ltac1
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/micromega
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/micromega_core
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/nsatz
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/number_string_notation
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ring
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/rtauto
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ssreflect
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ssrmatching
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tauto
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p0
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p1
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p2
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p3
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/zify
-R /home/sam/.opam/coq-dev/lib/coq/theories Coq
-R src QuickChick
src/QuickChick.v)
$ (cd _build/default && /home/sam/.opam/coq-dev/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot
-I /home/sam/.opam/coq-dev/lib/coq-core/boot
-I /home/sam/.opam/coq-dev/lib/coq-core/clib
-I /home/sam/.opam/coq-dev/lib/coq-core/config
-I /home/sam/.opam/coq-dev/lib/coq-core/engine
-I /home/sam/.opam/coq-dev/lib/coq-core/gramlib
-I /home/sam/.opam/coq-dev/lib/coq-core/interp
-I /home/sam/.opam/coq-dev/lib/coq-core/kernel
-I /home/sam/.opam/coq-dev/lib/coq-core/lib
-I /home/sam/.opam/coq-dev/lib/coq-core/library
-I /home/sam/.opam/coq-dev/lib/coq-core/parsing
-I /home/sam/.opam/coq-dev/lib/coq-core/perf
-I /home/sam/.opam/coq-dev/lib/coq-core/plugins/extraction
-I /home/sam/.opam/coq-dev/lib/coq-core/plugins/ltac
-I /home/sam/.opam/coq-dev/lib/coq-core/pretyping
-I /home/sam/.opam/coq-dev/lib/coq-core/printing
-I /home/sam/.opam/coq-dev/lib/coq-core/proofs
-I /home/sam/.opam/coq-dev/lib/coq-core/tactics
-I /home/sam/.opam/coq-dev/lib/coq-core/vernac
-I /home/sam/.opam/coq-dev/lib/coq-core/vm
-I /home/sam/.opam/coq-dev/lib/findlib
-I /home/sam/.opam/coq-dev/lib/zarith
-I /home/sam/.opam/coq-dev/lib64/dynlink
-I /home/sam/.opam/coq-dev/lib64/str
-I /home/sam/.opam/coq-dev/lib64/threads
-I /home/sam/.opam/coq-dev/lib64/unix
-I plugin
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/btauto
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/cc
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/derive
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/extraction
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/firstorder
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/funind
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ltac
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ltac2
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ltac2_ltac1
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/micromega
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/micromega_core
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/nsatz
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/number_string_notation
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ring
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/rtauto
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ssreflect
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/ssrmatching
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tauto
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p0
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p1
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p2
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/tutorial/p3
-I /home/sam/.opam/coq-dev/lib/coq/../coq-core/plugins/zify
-I /home/sam/.opam/coq-dev/lib/coq/user-contrib/SimpleIO
-I /home/sam/.opam/coq-dev/lib/coq/user-contrib/elpi
-I /home/sam/.opam/coq-dev/lib/coq/user-contrib/elpi/apps
-R /home/sam/.opam/coq-dev/lib/coq/theories Coq
-Q /home/sam/.opam/coq-dev/lib/coq/user-contrib/mathcomp mathcomp
-Q /home/sam/.opam/coq-dev/lib/coq/user-contrib/SimpleIO SimpleIO
-Q /home/sam/.opam/coq-dev/lib/coq/user-contrib/ExtLib ExtLib
-Q /home/sam/.opam/coq-dev/lib/coq/user-contrib/elpi elpi
-Q /home/sam/.opam/coq-dev/lib/coq/user-contrib/HB HB
-Q /home/sam/.opam/coq-dev/lib/coq/user-contrib/Ltac2 Ltac2
-R src QuickChick
src/QuickChick.v)
Last updated: Oct 13 2024 at 01:02 UTC