Stream: Dune devs & users

Topic: Problem with alt-ergo on quite a few architectures


view this post on Zulip Julien Puydt (Jul 04 2022 at 07:05):

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?

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 10:22):

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

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 10:25):

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)

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 10:27):

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

view this post on Zulip Julien Puydt (Jul 04 2022 at 14:22):

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.

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:37):

I meant that as the patch for upstream

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:38):

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.

view this post on Zulip Julien Puydt (Jul 04 2022 at 14:39):

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.

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:41):

Yes I agree, so there’s a misunderstanding.

view this post on Zulip Julien Puydt (Jul 04 2022 at 14:44):

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.

view this post on Zulip Julien Puydt (Jul 04 2022 at 14:47):

Ah, there's coq itself

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:47):

@Julien Puydt https://github.com/ejgallego/coq-plugin-template/blob/v8.16/src/dune is a concrete template

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:47):

as you see, no install section is needed

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:48):

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

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:50):

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.

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:50):

then it's up to dune to figure out the filename to use (depending on native vs bytecode) etc.

view this post on Zulip Julien Puydt (Jul 04 2022 at 14:51):

I think I see how to make alt-ergo plugins install correctly, but I'll need to dig how alt-ergo loads its plugins.

view this post on Zulip Paolo Giarrusso (Jul 04 2022 at 14:52):

I see — you said "plugins" not "Coq plugins"

view this post on Zulip Julien Puydt (Jul 04 2022 at 15:00):

Yes, I'm interested in alt-ergo plugins ; I only mentioned coq because I saw it's using dune for plugins.

view this post on Zulip Julien Puydt (Jul 04 2022 at 16:43):

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: Feb 04 2023 at 02:03 UTC