Suppose a project extracts its own code to generate a plugin, which is then used in other project Coq files. Is this possible to do in dune at all with the current Coq support? Can the interdependencies across Coq and OCaml be represented properly to do intra-project composable builds?
e.g., I change file
A.v, which is used in extraction to
a.ml is in turn used in the plugin used by
B.v. So dune will know it has to recompile
a.ml if I want to use
That should work, yes. As far as dune is concerned, there's no difference between extracted or hand written sources by the way.
Yup, as Rudi notes that should work; biggest pain tho is that Coq's plugin loader is not aware of deps yet, so setting up your
Declare ML may be a bit tricky.
managed to do it, but only when the extracted file is not a standalone library (with a public name). In case it is, there is dynamic linking error when a
Require loads the plugin.
Umm, not sure what you mean, but that's bizarre; care to post more details?
in particular the public / non-public status should not matter a lot
what is the
(libraries ...) field of the extracted code stanza?
indeed note the limitations of Coq's dynamic linker
[I should say Coq's non-linker]
OK, so the extracted file is called
Extract.v lives in a directory
src. Here is what the
src/dune looks like that works:
(library (name staltac_plugin) (public_name coq-stalmarck.plugin) (flags :standard -rectypes -w -3-27-32) (libraries coq.plugins.ltac)) (coq.pp (modules staltac)) (coq.extraction (prelude Extract) (extracted_modules run) (theories Stalmarck))
and here is the refactored version that doesn't work (plugin compiles but can't be loaded):
(library (name staltac_plugin) (public_name coq-stalmarck.plugin) (flags :standard -rectypes -w -3-27-32) (modules :standard \ run) (libraries coq.plugins.ltac coq-stalmarck.run)) (coq.pp (modules staltac)) (coq.extraction (prelude Extract) (extracted_modules run) (theories Stalmarck)) (library (name run) (public_name coq-stalmarck.run) (modules run))
The reason why I want
run to have a public name is that I want to reuse it elsewhere in the project.
The error message I get is as follows:
error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/home/palmskog/src/coq-community/stalmarck/_build/default/src/staltac_plugin.cmxs: undefined symbol: camlRun\")")
and indeed whether I have
public_name or not doesn't matter, but if I don't make it public there isn't much point.
Yes, you need to depend on run in your project, and load it manually
Coq's linker cannot understand the dependency on run
so you'll have to load it manually
this is possible tho
just use as many
Declare ML as you have deps
OK, so this is a known limitation? I just insert
Declare ML Module "run" into the
.mlpack file can be completely empty?
yes, that's another known issue
and it has its own issue too
I wonder if it's at all possible to avoid dynlink mess. For example, one could specify the list of plugins in a stanza and have dune create a coq executable with all the plugins statically linked. I'm sure there's subtleties that I'm not appreciating here, but in all of my experiences with OCaml, plugins were never worth the effort.
You could do that, but unfortunately plugins tends to change too much of the behavior as to have them always loaded, so we are stuck with them for a while, even some of them may not be compatible
Actually plugins for Coq are a kind of success story; it is one of the few cases where they do make sense
But I agree than in general I think they are overused, I much prefer to incorporate functionality on the core system
ah, everything works well now, except that every build gets this warning:
coqdep theories/StalTac.v.d *** Warning: in file StalTac.v, declared ML module stal has not been found!
I guess once the Coq issue gets resolved this will go away
Actually that seems due to a missing
.mlpack file somewhere; this stuff is annoying but until we don't patch
coqdep in a slightly incompatible fashion we cannot improve I'm afraid
Last updated: Jun 03 2023 at 18:01 UTC