Pierre-Marie Pédrot (Oct 16 2022 at 11:35): Pierre-Marie Pédrot (Oct 16 2022 at 11:35):In a neverending effort of reducing the general footprint of the Coq system (la fin de l'abondance, as they said), I was concerned by the fact that the csdpcert binary in the docker image was quite big (32Mio). After looking at the code, I realized that it links against the whole Ltac plugin, which brings in a lot of unrelated code. IIUC, csdpcert only needs access to the kernel term representation, or maybe a bit more, but definitely not the whole tactic library and much less the Ltac plugin.
Pierre-Marie Pédrot (Oct 16 2022 at 11:36):So I am trying to split the micromega plugin in two parts, a minimal library and the stuff that actually hooks into the plugins. But my dune level is not up to the task. I've tried to cargo-cult the dune file of the micromega plugin, which already does some internal splitting, but I am facing dynlink errors.
Pierre-Marie Pédrot (Oct 16 2022 at 11:36):Basically, I now have something like
(library
(name micromega_plugin)
(public_name coq-core.plugins.micromega)
; be careful not to link the executable to the plugin!
(modules g_micromega)
(flags :standard -open Micromega_lib)
(synopsis "Coq's micromega plugin")
(libraries coq-core.plugins.ltac coq-core.plugins.micromega-lib))
(library
(name micromega_lib)
(public_name coq-core.plugins.micromega-lib)
; be careful not to link the executable to the plugin!
(modules (:standard \ csdpcert g_micromega g_zify zify))
(synopsis "Base library of the Coq micromega plugin")
(libraries coq-core.plugins.ltac))
but the Require ML module fails with errors that look like
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/pm/sources/coq/_build/default/plugins/micromega/micromega_plugin.cmxs: undefined symbol: camlMicromega_lib__Coq_micromega\")")
So, my question is the following: are we supposed to be able to have split libraries used by plugins like this ?
Pierre-Marie Pédrot (Oct 16 2022 at 11:39):Clearly there is a missing invocation to dynlink micromega-lib from micromega-plugin, but I am not sure where this should go.
Pierre-Marie Pédrot (Oct 16 2022 at 11:40):(Also since we can now have plugins depending on one another, I think that zify should be moved in its own folder)
Gaëtan Gilbert (Oct 16 2022 at 11:43):I think we would need to stop using legacy loading for it
Gaëtan Gilbert (Oct 16 2022 at 11:44):or maybe do a preliminary Declare ML Module "micromega_lib" while we use legacy loading
Pierre-Marie Pédrot (Oct 16 2022 at 11:44):Weren't we supposed to remove the support for legacy loading in 8.17 though?
Gaëtan Gilbert (Oct 16 2022 at 11:45):don't know
Pierre-Marie Pédrot (Oct 16 2022 at 11:45):and also, if we use the new syntax for plugin loading, this should work out of the box, shouldn't it?
Gaëtan Gilbert (Oct 16 2022 at 11:45):try and tell us
Pierre-Marie Pédrot (Oct 16 2022 at 11:46):well, it doesn't and this is my point
Pierre-Marie Pédrot (Oct 16 2022 at 11:46):the files that are not compiling are using
Declare ML Module "micromega_plugin:coq-core.plugins.micromega".
should I write a META file by hand or something?
Ali Caglayan (Oct 16 2022 at 11:50):Can you do --always-show-command-line to Dune? (DUNEOPT for the makefile)
Pierre-Marie Pédrot (Oct 16 2022 at 11:50):you want the precise ocaml call?
Ali Caglayan (Oct 16 2022 at 11:51):Was it not coqc complaining?
Pierre-Marie Pédrot (Oct 16 2022 at 11:51):coqc, I mean
Pierre-Marie Pédrot (Oct 16 2022 at 11:52):$ (cd _build/default/theories/micromega && ../../../install/default/bin/coqc -boot -R ../. Coq -I ../../plugins/derive -I ../../plugins/micromega -I ../../plugins/nsatz -I ../../plugins/ssr -I ../../plugins/ltac -I ../../plugins/ssrmatching -I ../../plugins/btauto -I ../../plugins/rtauto -I ../../plugins/cc -I ../../plugins/extraction -I ../../plugins/ltac2 -I ../../plugins/ring -I ../../plugins/firstorder -I ../../plugins/syntax -I ../../plugins/funind -w +default -q -w -deprecated-native-compiler-option -native-compiler off Lia.v)
What if you also declare the library module?
Pierre-Marie Pédrot (Oct 16 2022 at 11:54):what do you mean by that?
Ali Caglayan (Oct 16 2022 at 11:54):Declare ML Module micromega_lib:coq-core.plugins.micromega-lib.
Ali Caglayan (Oct 16 2022 at 11:54):Just before the failing Declare
Pierre-Marie Pédrot (Oct 16 2022 at 11:55):seems to work
Pierre-Marie Pédrot (Oct 16 2022 at 11:55):so we have to transitively register the ML plugins?
Ali Caglayan (Oct 16 2022 at 11:56):hopefully not
Pierre-Marie Pédrot (Oct 16 2022 at 11:56):or just add a findlib call somewhere in the code of the coq_micromega plugin?
Ali Caglayan (Oct 16 2022 at 11:56):It shouldn't be like that but this will let you work for now
Ali Caglayan (Oct 16 2022 at 11:56):I'm not sure how the findlib call needs to be tweaked
Pierre-Marie Pédrot (Oct 16 2022 at 11:57):this compiles stdlib fine but then the test-suite fails with path issues
Ali Caglayan (Oct 16 2022 at 11:57):Also did you want to make micromega_lib internal?
Ali Caglayan (Oct 16 2022 at 11:57):currently you have public_name in the stanza
Pierre-Marie Pédrot (Oct 16 2022 at 11:57):I have no idea of what I am doing
Ali Caglayan (Oct 16 2022 at 11:58):If you remove public_name it might work without the Delcare line
Ali Caglayan (Oct 16 2022 at 11:58):The issue is that you've made the internal lib public so the other plugin tries to link against it, and findlib in coqc doesn't know where that is
Pierre-Marie Pédrot (Oct 16 2022 at 11:58):well tried but no:
Error: Library "micromega_lib" is private, it cannot be a dependency of a
public library. You need to give "micromega_lib" a public name.
oh shit
Ali Caglayan (Oct 16 2022 at 11:59):yeah we need to ask Emilio and Enrico about this
Ali Caglayan (Oct 16 2022 at 11:59):I'm not very happy about this plugin loading situation
Ali Caglayan (Oct 16 2022 at 11:59):For now transitive deps for plugins should be declared I guess
Pierre-Marie Pédrot (Oct 16 2022 at 12:00):as hinted above this is not enough
Pierre-Marie Pédrot (Oct 16 2022 at 12:01):for some reason the stdlib goes through, but then any Require of micromega fails complaining about missing cmxs
Pierre-Marie Pédrot (Oct 16 2022 at 12:02):Error: Can't find file micromega_lib.cmxs on loadpath.
Is this in the test-suite?
Pierre-Marie Pédrot (Oct 16 2022 at 12:02):yes
Pierre-Marie Pédrot (Oct 16 2022 at 12:03):but even outside of it, it also fails
Pierre-Marie Pédrot (Oct 16 2022 at 12:03):a fresh CoqIDE call that only does Require ZArith. fails the same way
Ali Caglayan (Oct 16 2022 at 12:03):Did you ./configure at all?
Pierre-Marie Pédrot (Oct 16 2022 at 12:03):nope
Ali Caglayan (Oct 16 2022 at 12:05):Do you have config/coq_config.ml around?
Ali Caglayan (Oct 16 2022 at 12:06):If not don't worry
Pierre-Marie Pédrot (Oct 16 2022 at 12:06):in the dune build folder?
Ali Caglayan (Oct 16 2022 at 12:06):yes I think so
Pierre-Marie Pédrot (Oct 16 2022 at 12:07):yes there is such a file in _build/default
Ali Caglayan (Oct 16 2022 at 12:07):It shouldhave a list of plugins what are they
Pierre-Marie Pédrot (Oct 16 2022 at 12:07):I'm trying again with git clean to see what happens
Ali Caglayan (Oct 16 2022 at 12:08):I am suspecting that the plugin list that configure produces isn't up to date (tho i'm not sure)
Ali Caglayan (Oct 16 2022 at 12:09):Even if you don't run configure Dune runs it
Ali Caglayan (Oct 16 2022 at 12:09):But since we don't go adding plugins every Tuesday, I don't think it has been tested well
Pierre-Marie Pédrot (Oct 16 2022 at 12:09):this doesn't mention any specific cmxs though
Pierre-Marie Pédrot (Oct 16 2022 at 12:09):it just mentions the paths
Ali Caglayan (Oct 16 2022 at 12:09):Right thats the hint for findlib to look for them
Pierre-Marie Pédrot (Oct 16 2022 at 12:10):I haven't added any folder so this shouldn't matter.
Ali Caglayan (Oct 16 2022 at 12:10):Then I am at a lost unforutnately
Ali Caglayan (Oct 16 2022 at 12:10):I know how to fix it with the new test-suite setup :)
Pierre-Marie Pédrot (Oct 16 2022 at 12:10):nope, even after a git clean -xdff this is still broken
Pierre-Marie Pédrot (Oct 16 2022 at 12:10):but this is not test-suite specific again
Pierre-Marie Pédrot (Oct 16 2022 at 12:11):and the weird thing is that the file it complains about is definitely in the path
Pierre-Marie Pédrot (Oct 16 2022 at 12:12):oh wait, no
Pierre-Marie Pédrot (Oct 16 2022 at 12:15):so it puts the cmxs in a separate _build/install/default/lib/coq-core/plugins/micromega-lib folder, which is why it doesn't find it
Pierre-Marie Pédrot (Oct 16 2022 at 12:15):now why I don't understand is why this works for zify, which uses the same organization, but not for this one
Pierre-Marie Pédrot (Oct 16 2022 at 12:15):(the plot thickens)
Gaëtan Gilbert (Oct 16 2022 at 12:32): Gaëtan Gilbert (Oct 16 2022 at 12:33):https://github.com/coq/coq/blob/master/lib/core_plugins_findlib_compat.ml
Paolo Giarrusso (Oct 16 2022 at 14:30):There are indeed known dune issues with Coq plugins: https://github.com/ocaml/dune/issues/5998#issuecomment-1273399569.
Emilio Jesús Gallego Arias (Oct 17 2022 at 10:58):It should be possible to port gen_rules to use the new loading method, tho https://github.com/coq/coq/issues/16571 is likely to be an issue
Last updated: Jun 05 2023 at 09:01 UTC