Stream: Dune devs & users

Topic: Composable builds coqdep

Lasse Blaauwbroek (Dec 06 2020 at 17:48):

So I've finally decided to give this fancy composable builds feature a real try. I've created a symlink from Coq's plugin directory to my plugin. However, all my .v files error out on coqdep: Error: cannot guess a path for Coq libraries; please use -coqlib option. Is this a known limitation or am I doing something wrong?

Lasse Blaauwbroek (Dec 06 2020 at 18:29):

Ah, I finally found this section: https://github.com/ejgallego/coq-plugin-template#composing-with-coq. So apparently I should symlink Coq into my plugin and not the other way around. I'm still not entirely clear on what this means though:

you should call Coq's configure with the a correct install path

What is the correct install path here? _build/install maybe?

Théo Zimmermann (Dec 06 2020 at 21:07):

I can't explain precisely, but this is a known issue that is worked around in the "shims". See https://github.com/coq/coq/blob/master/dev/shim/dune

Emilio Jesús Gallego Arias (Dec 06 2020 at 21:54):

Umm, that's bizarre, it should work, tho I'd recommend having the plugin under something such as user-contribs/my_plugin

Emilio Jesús Gallego Arias (Dec 06 2020 at 21:55):

There is some special code for for plugins in configure [for Coq Makefile]

Emilio Jesús Gallego Arias (Dec 06 2020 at 21:55):

Can I maybe see the plugin you are linking to?

Emilio Jesús Gallego Arias (Dec 06 2020 at 21:55):

Note that if you have a dune-project file in your plugin things won't sadly work

Emilio Jesús Gallego Arias (Dec 06 2020 at 21:56):

Regarding calling Coq's configure witht he correct install path, that is only needed if you plan to run dune install; that limitation should be lifted soon by making the dune build fully relocatable

Emilio Jesús Gallego Arias (Dec 06 2020 at 21:58):

I wouldn't be surprised if this is just a bug in Dune's Coq support as we don't handle composable builds that are inter-scope [no need to worry what this means, just that I need to complete some parts of the code and it took way longer than I expected, creating confusion]

Emilio Jesús Gallego Arias (Dec 07 2020 at 11:57):

@Lasse I've verified that indeed the problem is due to dune not supporting inter-scope for .v files, I've added tactician as a test case, I hope to push the patch fixing this week

Emilio Jesús Gallego Arias (Dec 07 2020 at 11:58):

for now there is no other workaround that moving the coq-tactician package to Coq's dune-project

Emilio Jesús Gallego Arias (Dec 07 2020 at 11:58):

which is very inconvenient

Emilio Jesús Gallego Arias (Dec 07 2020 at 11:58):

however, the OCaml check target does at least work

Emilio Jesús Gallego Arias (Dec 07 2020 at 11:59):

Dune should directly error in your case instead of giving this confusing failure when attempting the v files

Emilio Jesús Gallego Arias (Dec 07 2020 at 11:59):

that's entirely my fault

Lasse Blaauwbroek (Dec 07 2020 at 12:12):

Thanks for looking into it. So to summarize for my understanding: If I want a composable build with coq I

1. Create a symlink from user-contrib to the plugin
2. Remove the dune-project file from the plugin, and add the package to Coq's dune-project
3. Wait for a patch that allows for .v files with dependencies on other plugins with the same module scope (I assume that this is what 'inter-scope' means?)

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:27):

If you 1 & 2 things work [just tested] ; the patch will allow you not to have to move the package from coq-tactician dune-project to the root one.

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:27):

A scope in dune is a part of the build that has its own dune-project

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:27):

so we only support composition for things in the same scope

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:28):

I tested the basic build, other things such a shims etc ... may need adjustement, tho we worked on a patch that will solve also the need for shims

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:28):

you would still missing better plugin install workflow, pending on Coq using findlib

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:29):

Only change I had to do was to add (package coq-tactician) to src/dune for the executable.

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:29):

and remove Ltac1Dummy

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:31):

yeah that's not ideal, but on the other hand tooling seems to work properly, including merlin / etc...

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:31):

and doing dune build -p coq-tactician does only build the required parts for example of the stdlib

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:31):

so that's faster

Lasse Blaauwbroek (Dec 07 2020 at 12:32):

Ah, that actually sounds quite reasonable, especially when you compare it to the hoops I was previously jumping through to compile the plugin with a modified Coq. I'll try it out later today. Thanks!

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:45):

:+1:

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:45):

Note that merlin sometimes goes crazy silently if -rectypes flags on modules don't match

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:45):

let me know if you have any problem

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:45):

but seems to be working fine here

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:47):

So I had to add -rectypes to the flags in src/dune to prevent some erractic behavior

Emilio Jesús Gallego Arias (Dec 07 2020 at 12:47):

yup, all working fine AFAICS

Lasse Blaauwbroek (Dec 17 2020 at 10:17):

Hi @Emilio Jesús Gallego Arias , sorry for coming back to this so late. I got distracted by other things. With your pointers, I can now build my plugin as part of a call to dune build in the Coq repo. However, my experience does not appear to be the same as yours:

• Running dune build -p coq-tactician does not also build Coq. If there is an installed version of Coq available dune selects that one. Otherwise it gives an error. The same is true for dune build -p coqide-server btw. After running make -f Makefile.dune world running dune build -p coq-tactician does indeed work.
• When I make a change in Coq and the plugin, I first need to run make -f Makefile.dune world again before running dune -p coq-tactician again. So I'm currently not really benefiting from a "minimal" Coq build that only builds what my plugin needs.

Am I still doing something wrong?

Lasse Blaauwbroek (Dec 17 2020 at 10:37):

Well, it is even a bit worse, because it seems that make -f Makefile.dune world does not build coq.plugins.funind and coq.plugins.ssreflect, who I depend on. So the only thing that works now is building absolutely everything with dune build.

Emilio Jesús Gallego Arias (Dec 17 2020 at 13:55):

Hi @Lasse , thanks for trying. I'll try answer:

• using -p has indeed that semantics on purpose [build only that package, ignore the rest] For development you don't want to use -p, only for releases as the build is much slower due to inter-module optimiziations being enable for example. To build several packages at once you can do -p coq,coq-tactician and that will work. Behavior of -p is indeed confusing and this is FAQ, or more accurately, an Always Asked Question.
• On what to build, dune is target-based, so for example you can request dune build coq-tactician.install to build all the set of installable files, etc... of your package, that will also build dependencies. dune build @check is the usual dev target, for building combinations of things, as of today, I suggest you look into dev/shim to see how it is done, we will implement a command that does that automatically, so if you issue dune coqtop foo.v it will build all that foo.v needs.
• It is strange that make world doesn't build that plugins, I couldn't reproduce and indeed it should.

Lasse Blaauwbroek (Dec 17 2020 at 17:41):

Okay with dune build coq-tactician.install everything works, and rather quickly so that is great. Thanks!

It is clear that Dune is better than make, but it is also a lot more magic/confusing/complex. First, I don't have to declare the coq-tactician.install target, which makes it difficult to know about (although I suppose I knew it existed because it is needed for Opam). Then, there is an indirection step that translates any target '*' to _build/*. Finally there are also these 'fake' targets like @install, which are also confusing.

But once you've understood it, everything works great!

Regarding the problem with make -f Makefile.dune world: I can consistently reproduce this:

1. Make sure that there is no installed version of Coq available somewhere
2. dune clean
3. make -f Makefile.dune world
4. dune build -p coq-tactician
   This leads to the following error:

File "user-contrib/coq-tactician/src/dune", line 34, characters 3-21:
34 |    coq.plugins.funind
        ^^^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.funind" not found.
Hint: try:
  dune external-lib-deps --missing -p coq-tactician @install
File "user-contrib/coq-tactician/src/dune", line 48, characters 3-24:
48 |    coq.plugins.ssreflect
        ^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.ssreflect" not found.
Hint: try:
  dune external-lib-deps --missing -p coq-tactician @install

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:48):

Indeed, there are many implicit targets in dune, see some documentation at https://dune.readthedocs.io/en/stable/usage.html?highlight=targets#interpretation-of-targets and https://dune.readthedocs.io/en/stable/usage.html?highlight=targets#built-in-aliases , but I'm sure the docs can be improved.

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:48):

The "fake" targets you mention are aliases, and there are many, most of them are already documented in the doc

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:49):

dune build -p coq-tactician is expected to fail, if you look at the doc for -p , it explicitly tells dune to ignore the local coq packages, then it will try to locate them using ocamlfind, which it fails as a compatible Coq is not installed. To build both packages in release mode you need to use -p coq,coq-tactician

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:50):

see https://dune.readthedocs.io/en/stable/opam.html#invocation-from-opam

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:50):

in particular, the --only-packages pkg

Lasse Blaauwbroek (Dec 17 2020 at 17:50):

I see, now it makes sense to me

Lasse Blaauwbroek (Dec 17 2020 at 17:52):

The aliases I've not yet completely mastered. I'm now trying to add some tests to my package but I'm not entirely sure how to integrate this with @runtest. I'm now looking at https://github.com/lukaszcz/coqhammer/blob/coq8.12/tests/plugin/dune Is that the proper way to do it?

Lasse Blaauwbroek (Dec 17 2020 at 17:53):

Regarding the docs: I find the docs for Opam to be much easier to understand and search. I suspect that this may be because it is a single-page document.

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:57):

runtest is just an alias, aliases are "additive", so you can add more targets to an alias

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:58):

you can also have an alias and sub-alias

Emilio Jesús Gallego Arias (Dec 17 2020 at 17:58):

for tests

Lasse Blaauwbroek (Dec 17 2020 at 17:59):

Ah okay, I think I understand. Thanks

Emilio Jesús Gallego Arias (Dec 17 2020 at 18:00):

there is nothing special other than dune runtest is a shorthand for dune build @runtest

Lasse Blaauwbroek (Dec 18 2020 at 05:21):

For my tests directory I now have the following dune file. Is this a good way of specifying tests, and if not can you tell me what is?

(coq.theory
 (name TacticianTests)
 (flags -q)
 (theories Tactician))
(alias
 (name runtest)
 (deps DummyTest.vo DummyTest2.vo))

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:04):

That should work, you can maybe use a *.vo glob, but indeed we should improve this setup.

Rudi Grinberg (Dec 18 2020 at 15:42):

Lasse said:

Regarding the docs: I find the docs for Opam to be much easier to understand and search. I suspect that this may be because it is a single-page document.

It is also because dune's feature set is far wider than opam's.

Rudi Grinberg (Dec 18 2020 at 15:43):

Lasse said:

For my tests directory I now have the following dune file. Is this a good way of specifying tests, and if not can you tell me what is?

(coq.theory
 (name TacticianTests)
 (flags -q)
 (theories Tactician))
(alias
 (name runtest)
 (deps DummyTest.vo DummyTest2.vo))

Where's your test action though? The test action is the command that dune should run to execute the tests.

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:43):

In this case the test is compiling the .v files

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:43):

if compilation passes, the tests are OK

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:44):

it is natural in Coq to write the tests in the .v files in form of theorems, etc...

Rudi Grinberg (Dec 18 2020 at 15:44):

I see. But then the tests are included as part of the library?

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:47):

They are in a different (coq.theory ...) but you need to declare it as otherwise coq_rules wont setup the rules for .v -> .vo

Rudi Grinberg (Dec 18 2020 at 15:51):

I see. But then it's possible to depend on such a "test" theory. I wonder if a coq.test stanza would make sense here.

Emilio Jesús Gallego Arias (Dec 18 2020 at 16:03):

Indeed, tho it could make sense for tests to depend on other tests? Anyways I'd like to introduce an alias for all the .vo of a theory, that would be useful for many things.

Regarding testing in Coq I guess we need more feedback, on one hand testing workflows in Coq are fairly primitive due to lack of tooling, most fancy things are already covered by dune with output tests or cram. On the other hand, many important developments don't have any tests at all, as that's the whole point of Coq, you prove everything is correct :)

Rudi Grinberg (Dec 18 2020 at 16:47):

Indeed, tho it could make sense for tests to depend on other tests?

That would already be possible. As .v files in a stanza can depend on each other. Or do you mean to depend on another test theory?

Anyways I'd like to introduce an alias for all the .vo of a theory, that would be useful for many things.

Sounds good. Do you expect building .vo files to be a part of @check?

Emilio Jesús Gallego Arias (Dec 18 2020 at 16:56):

Do you expect building .vo files to be a part of @check?

Only when we have support for the quick mode for vos/vok

Emilio Jesús Gallego Arias (Dec 18 2020 at 16:57):

And maybe as a different alias, it is a very common use case to hack Coq + N plugins, in this case it is nice that @check only deals with the ml part

Rudi Grinberg (Dec 18 2020 at 17:01):

On the other hand, many important developments don't have any tests at all, as that's the whole point of Coq, you prove everything is correct :)

Indeed :) Though it seems like people still make an effort to separate examples, benchmarks, and other non critical stuff from the main theory. For build speed I presume.

Rudi Grinberg (Dec 18 2020 at 17:02):

Only when we have support for the quick mode for vos/vok

Is that planned for 1.0?

Emilio Jesús Gallego Arias (Dec 18 2020 at 17:04):

hough it seems like people still make an effort to separate examples, benchmarks, and other non critical stuff from the main theory. For build speed I presume.

I'd say more as not to expose these bits to users of the particular theory.

Is that planned for 1.0?

Not critical IMHO but would be nice to have, however the way rules for these targets work is a bit contrived, so I'm unsure how easy it will be to add support

Lasse Blaauwbroek (Dec 18 2020 at 17:41):

Rudi Grinberg said:

It is also because dune's feature set is far wider than opam's.

Yes, perhaps you are right. Let me give you a particular thing in Dune that confuses the hell out of me though: Dune has a top-level syntax of the form

(rule ... (alias ...) (action ...))

But then, there is also some syntax of the form

(alias ... (action ...))

How are these two related? I'm guessing that the last is a shorthand of the first? I cannot find that information readily in the docs. They seem to be used interchangeably in the docs. For example, https://dune.readthedocs.io/en/stable/dune-files.html#alias defines the syntax of an alias, but the example given in that section is for rule...

Lasse Blaauwbroek (Dec 18 2020 at 17:44):

Emilio Jesús Gallego Arias said:

That should work, you can maybe use a *.vo glob, but indeed we should improve this setup.

Okay thanks, then I'll keep it this way until better support is available :-)

Rudi Grinberg (Dec 18 2020 at 18:13):

The 2nd form has been removed in 2.0.

Lasse Blaauwbroek (Dec 18 2020 at 18:14):

Ah, okay. It is still listed under 'optional fields' in the link I gave though

Rudi Grinberg (Dec 18 2020 at 18:15):

Indeed. But it also mentions:

Note that this is removed in the 2.0 version of the dune language. Users should port their code to use the rule stanza with the alias field instead.

Lasse Blaauwbroek (Dec 18 2020 at 18:16):

Ah I see, I didn't read that far :-P

Lasse Blaauwbroek (Dec 18 2020 at 18:19):

Still, the fact that one can have a top-level alias but also nest it inside a rule, in such a way that they have different syntax/semantics is a bit confusing.

Lasse Blaauwbroek (Dec 18 2020 at 18:21):

Mhm, I suppose that the alias inside a rule just specifies the name of the alias, so that may be okay. Perhaps I'm just bad at reading... :-)

Paolo Giarrusso (Dec 18 2020 at 19:11):

@Emilio Jesús Gallego Arias

On the other hand, many important developments don't have any tests at all, as that's the whole point of Coq, you prove everything is correct :)

even in Coq, both tactics and notations tend to need tests. I'm sure there are developments where the lack of tests is unwarranted (but I won't speculate how many).

Paolo Giarrusso (Dec 18 2020 at 19:12):

and +1 for support/examples for tests, including "golden master" ones (compare output with saved output). That can need a bit more flexibility than usual in dune — you might need to customize the comparison, adjust the tests for different coq versions...

Paolo Giarrusso (Dec 18 2020 at 19:13):

(I've needed all features of https://gitlab.mpi-sws.org/iris/iris/-/blob/master/Makefile.coq.local, but that doesn't have docs — only examples in https://gitlab.mpi-sws.org/iris/iris/-/tree/master/tests)

Last updated: Apr 19 2024 at 19:02 UTC