Stream: Dune devs & users

Topic: Composable builds coqdep


view this post on Zulip Lasse (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?

view this post on Zulip Lasse (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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2020 at 21:55):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2020 at 21:55):

Can I maybe see the plugin you are linking to?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 11:58):

which is very inconvenient

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 11:58):

however, the OCaml check target does at least work

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 11:59):

that's entirely my fault

view this post on Zulip Lasse (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?)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:27):

so we only support composition for things in the same scope

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:28):

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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:29):

and remove Ltac1Dummy

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:31):

so that's faster

view this post on Zulip Lasse (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!

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:45):

:+1:

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:45):

let me know if you have any problem

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:45):

but seems to be working fine here

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 07 2020 at 12:47):

yup, all working fine AFAICS

view this post on Zulip Lasse (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:

Am I still doing something wrong?

view this post on Zulip Lasse (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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 17 2020 at 13:55):

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

view this post on Zulip Lasse (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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 17 2020 at 17:50):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 17 2020 at 17:50):

in particular, the --only-packages pkg

view this post on Zulip Lasse (Dec 17 2020 at 17:50):

I see, now it makes sense to me

view this post on Zulip Lasse (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?

view this post on Zulip Lasse (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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 17 2020 at 17:58):

you can also have an alias and sub-alias

view this post on Zulip Emilio Jesús Gallego Arias (Dec 17 2020 at 17:58):

for tests

view this post on Zulip Lasse (Dec 17 2020 at 17:59):

Ah okay, I think I understand. Thanks

view this post on Zulip 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

view this post on Zulip Lasse (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))

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:43):

In this case the test is compiling the .v files

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:43):

if compilation passes, the tests are OK

view this post on Zulip 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...

view this post on Zulip Rudi Grinberg (Dec 18 2020 at 15:44):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Lasse (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...

view this post on Zulip Lasse (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 :-)

view this post on Zulip Rudi Grinberg (Dec 18 2020 at 18:13):

The 2nd form has been removed in 2.0.

view this post on Zulip Lasse (Dec 18 2020 at 18:14):

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

view this post on Zulip 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.

view this post on Zulip Lasse (Dec 18 2020 at 18:16):

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

view this post on Zulip Lasse (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.

view this post on Zulip Lasse (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... :-)

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip 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: Oct 16 2021 at 09:07 UTC