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.
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.
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 ?
Clearly there is a missing invocation to dynlink micromega-lib from micromega-plugin, but I am not sure where this should go.
(Also since we can now have plugins depending on one another, I think that zify should be moved in its own folder)
I think we would need to stop using legacy loading for it
or maybe do a preliminary Declare ML Module "micromega_lib" while we use legacy loading
Weren't we supposed to remove the support for legacy loading in 8.17 though?
don't know
and also, if we use the new syntax for plugin loading, this should work out of the box, shouldn't it?
try and tell us
well, it doesn't and this is my point
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?
Can you do --always-show-command-line
to Dune? (DUNEOPT for the makefile)
you want the precise ocaml call?
Was it not coqc complaining?
coqc, I mean
$ (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?
what do you mean by that?
Declare ML Module micromega_lib:coq-core.plugins.micromega-lib.
Just before the failing Declare
seems to work
so we have to transitively register the ML plugins?
hopefully not
or just add a findlib call somewhere in the code of the coq_micromega plugin?
It shouldn't be like that but this will let you work for now
I'm not sure how the findlib call needs to be tweaked
this compiles stdlib fine but then the test-suite fails with path issues
Also did you want to make micromega_lib internal?
currently you have public_name in the stanza
I have no idea of what I am doing
If you remove public_name it might work without the Delcare line
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
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
yeah we need to ask Emilio and Enrico about this
I'm not very happy about this plugin loading situation
For now transitive deps for plugins should be declared I guess
as hinted above this is not enough
for some reason the stdlib goes through, but then any Require of micromega fails complaining about missing cmxs
Error: Can't find file micromega_lib.cmxs on loadpath.
Is this in the test-suite?
yes
but even outside of it, it also fails
a fresh CoqIDE call that only does Require ZArith.
fails the same way
Did you ./configure
at all?
nope
Do you have config/coq_config.ml around?
If not don't worry
in the dune build folder?
yes I think so
yes there is such a file in _build/default
It shouldhave a list of plugins what are they
I'm trying again with git clean to see what happens
I am suspecting that the plugin list that configure produces isn't up to date (tho i'm not sure)
Even if you don't run configure Dune runs it
But since we don't go adding plugins every Tuesday, I don't think it has been tested well
this doesn't mention any specific cmxs though
it just mentions the paths
Right thats the hint for findlib to look for them
I haven't added any folder so this shouldn't matter.
Then I am at a lost unforutnately
I know how to fix it with the new test-suite setup :)
nope, even after a git clean -xdff this is still broken
but this is not test-suite specific again
and the weird thing is that the file it complains about is definitely in the path
oh wait, no
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
now why I don't understand is why this works for zify, which uses the same organization, but not for this one
(the plot thickens)
https://github.com/coq/coq/blob/master/lib/core_plugins_findlib_compat.ml
There are indeed known dune issues with Coq plugins: https://github.com/ocaml/dune/issues/5998#issuecomment-1273399569.
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