Stream: Coq devs & plugin devs

Topic: Plugin depending on an internal library


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:37):

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

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:38):

So, my question is the following: are we supposed to be able to have split libraries used by plugins like this ?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Oct 16 2022 at 11:43):

I think we would need to stop using legacy loading for it

view this post on Zulip Gaëtan Gilbert (Oct 16 2022 at 11:44):

or maybe do a preliminary Declare ML Module "micromega_lib" while we use legacy loading

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Oct 16 2022 at 11:45):

don't know

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Oct 16 2022 at 11:45):

try and tell us

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:46):

well, it doesn't and this is my point

view this post on Zulip 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".

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:47):

should I write a META file by hand or something?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:50):

Can you do --always-show-command-line to Dune? (DUNEOPT for the makefile)

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:50):

you want the precise ocaml call?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:51):

Was it not coqc complaining?

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:51):

coqc, I mean

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:53):

What if you also declare the library module?

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:54):

what do you mean by that?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:54):

Declare ML Module micromega_lib:coq-core.plugins.micromega-lib.

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:54):

Just before the failing Declare

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:55):

seems to work

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:55):

so we have to transitively register the ML plugins?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:56):

hopefully not

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:56):

It shouldn't be like that but this will let you work for now

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:56):

I'm not sure how the findlib call needs to be tweaked

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:57):

this compiles stdlib fine but then the test-suite fails with path issues

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:57):

Also did you want to make micromega_lib internal?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:57):

currently you have public_name in the stanza

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 11:57):

I have no idea of what I am doing

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:58):

If you remove public_name it might work without the Delcare line

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:59):

oh shit

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:59):

yeah we need to ask Emilio and Enrico about this

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:59):

I'm not very happy about this plugin loading situation

view this post on Zulip Ali Caglayan (Oct 16 2022 at 11:59):

For now transitive deps for plugins should be declared I guess

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:00):

as hinted above this is not enough

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:02):

Error: Can't find file micromega_lib.cmxs on loadpath.

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:02):

Is this in the test-suite?

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:02):

yes

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:03):

but even outside of it, it also fails

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:03):

a fresh CoqIDE call that only does Require ZArith. fails the same way

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:03):

Did you ./configure at all?

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:03):

nope

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:05):

Do you have config/coq_config.ml around?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:06):

If not don't worry

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:06):

in the dune build folder?

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:06):

yes I think so

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:07):

yes there is such a file in _build/default

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:07):

It shouldhave a list of plugins what are they

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:07):

I'm trying again with git clean to see what happens

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:09):

Even if you don't run configure Dune runs it

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:09):

this doesn't mention any specific cmxs though

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:09):

it just mentions the paths

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:09):

Right thats the hint for findlib to look for them

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:10):

I haven't added any folder so this shouldn't matter.

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:10):

Then I am at a lost unforutnately

view this post on Zulip Ali Caglayan (Oct 16 2022 at 12:10):

I know how to fix it with the new test-suite setup :)

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:10):

nope, even after a git clean -xdff this is still broken

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:10):

but this is not test-suite specific again

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:12):

oh wait, no

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Oct 16 2022 at 12:15):

(the plot thickens)

view this post on Zulip Gaëtan Gilbert (Oct 16 2022 at 12:32):

https://github.com/coq/coq/blob/ff0a95f5762938c6ec3754aaf0c129d43db068dd/tools/dune_rule_gen/coq_rules.ml#L38

view this post on Zulip Gaëtan Gilbert (Oct 16 2022 at 12:33):

https://github.com/coq/coq/blob/master/lib/core_plugins_findlib_compat.ml

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 20:03 UTC