Stream: Coq devs & plugin devs

Topic: Troubleshooting Dynlink failure


view this post on Zulip Li-yao (Apr 03 2024 at 11:00):

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\")")

view this post on Zulip Gaëtan Gilbert (Apr 03 2024 at 11:08):

how did you install coq?

view this post on Zulip Li-yao (Apr 03 2024 at 11:16):

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.

view this post on Zulip Gaëtan Gilbert (Apr 03 2024 at 11:21):

I guess you didn't forget to eval opam env?
What's the dune version?

view this post on Zulip Li-yao (Apr 03 2024 at 11:22):

I haven't forgotten! Dune 3.14.2

view this post on Zulip Gaëtan Gilbert (Apr 03 2024 at 11:32):

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 ?

view this post on Zulip Li-yao (Apr 03 2024 at 11:50):

no change.

view this post on Zulip Gaëtan Gilbert (Apr 03 2024 at 11:58):

IDK then
btw maybe this would be better targetted at the dune stream rather than coq devs stream

view this post on Zulip Emilio Jesús Gallego Arias (Apr 03 2024 at 14:16):

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?

view this post on Zulip Li-yao (Apr 03 2024 at 19:48):

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