Stream: Dune devs & users

Topic: Building reflective tactics using dune

Karl Palmskog (May 31 2020 at 17:10):

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?

Karl Palmskog (May 31 2020 at 17:13):

e.g., I change file A.v, which is used in extraction to a.ml, and 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 B.v

Rudi Grinberg (May 31 2020 at 22:58):

That should work, yes. As far as dune is concerned, there's no difference between extracted or hand written sources by the way.

Emilio Jesús Gallego Arias (Jun 01 2020 at 14:42):

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.

Karl Palmskog (Jun 01 2020 at 15:01):

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.

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:28):

Umm, not sure what you mean, but that's bizarre; care to post more details?

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:28):

in particular the public / non-public status should not matter a lot

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:29):

what is the (libraries ...) field of the extracted code stanza?

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:29):

indeed note the limitations of Coq's dynamic linker

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:29):

[I should say Coq's non-linker]

Karl Palmskog (Jun 01 2020 at 15:37):

OK, so the extracted file is called run.ml and 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.

Karl Palmskog (Jun 01 2020 at 15:39):

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.

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:53):

Yes, you need to depend on run in your project, and load it manually

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:54):

Coq's linker cannot understand the dependency on run

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:54):

so you'll have to load it manually

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:54):

this is possible tho

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:54):

just use as many Declare ML as you have deps

Karl Palmskog (Jun 01 2020 at 15:56):

OK, so this is a known limitation? I just insert Declare ML Module "run" into the .v file?

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:58):

Yes

Karl Palmskog (Jun 01 2020 at 15:59):

and the .mlpack file can be completely empty?

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:59):

see https://github.com/coq/coq/issues/7698

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:59):

yes, that's another known issue

Emilio Jesús Gallego Arias (Jun 01 2020 at 15:59):

and it has its own issue too

Rudi Grinberg (Jun 01 2020 at 20:13):

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.

Emilio Jesús Gallego Arias (Jun 01 2020 at 23:08):

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

Emilio Jesús Gallego Arias (Jun 01 2020 at 23:08):

Actually plugins for Coq are a kind of success story; it is one of the few cases where they do make sense

Emilio Jesús Gallego Arias (Jun 01 2020 at 23:09):

But I agree than in general I think they are overused, I much prefer to incorporate functionality on the core system

Karl Palmskog (Jun 02 2020 at 01:53):

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

Emilio Jesús Gallego Arias (Jun 02 2020 at 11:35):

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: Apr 19 2024 at 00:02 UTC