I reported this issue to alt-ergo upstream, but they didn't react, so I would like to tackle it myself. I'm pretty sure it's a case of native vs bytecode issue, and while dune isn't the culprit, that's probably where something needs to be done differently.
Indeed, if you check this dune file, you see:
(files
(ABWhy3Plugin.cma as plugins/AB-Why3-plugin.cma)
(ABWhy3Plugin.cmxs as plugins/AB-Why3-plugin.cmxs)
)
where ABWhy3Plugin.cmxs is used unconditionally -- that fails on non-native if I'm not mistaken.
What can be done to get around it?
idea: Delete that install stanza, and find out how to use public_name/package in the library stanza to get dune to install the library the right way: https://dune.readthedocs.io/en/stable/dune-files.html#library-1
At least, that seems the dune spirit, but step 2 is not obvious, and I'm not sure if clients would still build without patches (so this might not work)
I checked the history, and this install stanza doesn't seem to have had much evolution https://github.com/OCamlPro/alt-ergo/commit/ec395a6741643f347dee1dacb166238502b4b178#diff-cf8e32539ebe85175307f2d2c9b603ff6610e1e819c82a98d9f8f7212d764aa7
Well, I modified the Debian package : when there's no ocamlc.opt, I apply a patch to remove the two faulty lines. But I would still like a better patch for upstream.
I meant that as the patch for upstream
According to the docs I linked, dune allows to get libraries installed without writing any install sections: you just give a declarative description of your library that is sufficient for dune to figure what to install.
My patch doesn't fly : I use the fact that I have a Makefile-like file to decide whether to apply it or not... that's not suitable for the dune-base upstream build system.
Yes I agree, so there’s a misunderstanding.
Do you know of a project using dune correctly to build plugins? I could use a working example to understand the situation and propose a nicer patch to alt-ergo upstream.
Ah, there's coq itself
@Julien Puydt https://github.com/ejgallego/coq-plugin-template/blob/v8.16/src/dune is a concrete template
as you see, no install
section is needed
then https://github.com/ejgallego/coq-plugin-template/blob/v8.16/theories/MyPlugin.v shows how to load that in Coq — note this changed for Coq 8.16
in particular, https://github.com/ejgallego/coq-plugin-template/blob/c0cc512a43e170d8843d7d7fb2310def8e2c3b66/src/dune#L7-L9 is the critical part: once you declare public_name
, dune
will install the library appropriately.
then it's up to dune to figure out the filename to use (depending on native vs bytecode) etc.
I think I see how to make alt-ergo plugins install correctly, but I'll need to dig how alt-ergo loads its plugins.
I see — you said "plugins" not "Coq plugins"
Yes, I'm interested in alt-ergo plugins ; I only mentioned coq because I saw it's using dune for plugins.
Hmmm... I get subdirectories of the plugins/ directory -- but that's not what they're trying to load. They want to point to the right file and load it using DynLink, like it is explained here.
Last updated: Oct 13 2024 at 01:02 UTC