✔ Dune, _CoqProject and tests · Dune devs & users

Stream: Dune devs & users

Topic: ✔ Dune, _CoqProject and tests

Jerome Hugues (Sep 07 2021 at 20:46):

Hi,

I am not sure this is the right forum, feel free to tell me where to look for help here. Thanks!

I recently converted my Coq project to Dune, with interesting benefits in terms of compilation time, and ease of maintenance. Yet Dune support for Coq seems to be still a work in progress.

I am looking for guidance on two topics

I still need _CoqProject for VSCoq, I wonder if this file can be generated by dune. I would assume one needs to build a list with the right order of .v files. Apparently dune computes this list, but I could not find any info on dune documentation to generate back a _CoqProject file.
I have a couple of .v files that are basically tests, i.e. a collection of lemma foo x = bar that checks that foo x returns the right value. Those are usually proved through a mere trivial. I would like to instruct dune to consider those files only when I run tests (i.e. dune build @install @runtest). I could imagine grouping those .v files in a dedicated tests directory. But I miss the next step for dune to consider those only when I run a dune build. Do I need to write a dedicated backend? Did someone already try this?

Thanks

Paolo Giarrusso (Sep 07 2021 at 21:49):

(This should move into the Dune devs & users stream, but a mod can do it)
I can't help with the latter, but for the former. You needn't list .v files in _CoqProject, but you do want the Coq options, both for flags and for -Q/-R. For instance:

-arg -w -arg -ssr-search-moved
-Q _build/default/theories your.logical.prefix

We indeed still write those _CoqProject files by hand.

Jerome Hugues (Sep 07 2021 at 22:37):

Paolo Giarrusso said:

(This should move into the Dune devs & users stream, but a mod can do it)
I can't help with the latter, but for the former. You needn't list .v files in _CoqProject, but you do want the Coq options, both for flags and for -Q/-R. For instance:
-arg -w -arg -ssr-search-moved
-Q _build/default/theories your.logical.prefix
We indeed still write those _CoqProject files by hand.

Thanks, that did it. I wonder where -ssr-search-moved is documented though. I could not find anything except for a bug report.

I subscribed to the Dune stream. I am not sure I can move the post. Sorry about that.

Notification Bot (Sep 08 2021 at 01:26):

Jerome Hugues has marked this topic as resolved.

Notification Bot (Sep 08 2021 at 07:21):

This topic was moved here from #Coq users > ✔ Dune, _CoqProject and tests by Théo Zimmermann

Théo Zimmermann (Sep 08 2021 at 07:23):

@Jerome Hugues That first line was just an example in case you want to disable a Coq warning. You probably don't need it. The important line is the -Q one.

Emilio Jesús Gallego Arias (Sep 08 2021 at 07:41):

Hi @Jerome Hugues , the reason we didn't provide Coq project generation is that actually, in many cases, it is not possible to produce a reasonable _CoqProject from a dune definition, I think. Tho, I'd be happy to merge support for a partial solution into dune if someone wants to do it.

There are two potential solutions to missing _CoqProject that work a bit better:

use the merlin protocol, which allows UIs to query for the flags of a particular file. This should be very easy to do for Coq in the Dune side [as it is already implemented], also, editors use it so both VsCode and Emacs could reuse the library code
have Proof General call the upcoming dune coqtop file.v which will open a toplevel with the right settings

Emilio Jesús Gallego Arias (Sep 08 2021 at 07:44):

Regarding your second question, I'd use a private theory [one that is not attacked to a package] and add the files to the runtest alias? Maybe open an issue in https://github.com/ejgallego/coq-plugin-template so we add your use case

Jerome Hugues (Sep 08 2021 at 14:47):

Emilio Jesús Gallego Arias said:

Regarding your second question, I'd use a private theory [one that is not attacked to a package] and add the files to the runtest alias? Maybe open an issue in https://github.com/ejgallego/coq-plugin-template so we add your use case

I was thinking of providing to the community a "sister" project to yours. My need is not to develop a plugin but to extract code and test elements. So I need to build the extracted code (figured it out) and run tests by 1/ processing Coq files and 2/ running some examples on the generated binary. Do you think it is better to extend your example (but with the risk of making it too big for newcomers), or is it fine to contribute a new one?

Karl Palmskog (Sep 08 2021 at 15:07):

there is not all that much interesting going on during extraction. The interesting use case for Dune (where coq_makefile breaks down badly) is arguably reflective plugins which use extracted code. See here: https://github.com/coq-community/stalmarck/tree/master/tactic

Emilio Jesús Gallego Arias (Sep 10 2021 at 16:59):

Hi @Jerome Hugues , actually it would make sense to keep the templates in the repos we already have, an once stable move it to Coq community. I will update the repos very soon [and merge @Karl Palmskog contributions], but I am working on large Dune update first, in particular to enable all the features we promised for coq-lang 1.0

Emilio Jesús Gallego Arias (Sep 10 2021 at 16:59):

I'd suggest for now we coordinate on the existing repos, I'd be happy to give you folks commit access if that's still not the case

Karl Palmskog (Sep 10 2021 at 17:01):

in this context, see also my program verification Dune based repo template: https://github.com/palmskog/coq-program-verification-template

Emilio Jesús Gallego Arias (Sep 10 2021 at 17:02):

Indeed, we should merge them !

Emilio Jesús Gallego Arias (Sep 10 2021 at 17:03):

Or maybe have several repos?

Emilio Jesús Gallego Arias (Sep 10 2021 at 17:03):

That could be more convenient for users doing git clone to start a project

Emilio Jesús Gallego Arias (Sep 10 2021 at 17:03):

then we could have in coq-community a dune-templates one, just the readme

Karl Palmskog (Sep 10 2021 at 17:28):

I think it will be confusing to merge templates, since requirements and file organization are quite different. For a verification project, one will want to target stable Coq, probably support both coq_makefile and Dune, etc.

Karl Palmskog (Sep 10 2021 at 17:30):

I don't mind if we put the template repos in the same organization though (e.g., coq-community) and call them something similar, for example:

coq-template-plugin
coq-template-verification

Jerome Hugues (Sep 10 2021 at 17:31):

I am fine with whatever option you prefer. I reviewed Karl's template a while back but I have different needs: I want to extract to Coq, run a test on the binary produced and run a test on the Coq files as well. The test on the Coq files is basically a .v file that illustrates some aspects of the Coq API (think of it like the examples some devs have like coq-json). Nothing fancy, but it could provide a starter kit for this kind of projects. I would prefer different repos, one per use cases, as long as this is in a convenient place for the community.

Emilio Jesús Gallego Arias (Sep 13 2021 at 17:10):

@Karl Palmskog @Jerome Hugues I have created a follow up issue here https://github.com/coq-community/templates/issues/105

Karl Palmskog (Sep 13 2021 at 17:25):

the current configuration templates are very limited by the Mustache language. Théo raised the issue of changing to a more expressive language, but no consensus on what so far. We would need to express complicated relationships between "subprojects" in a repository and so on

Karl Palmskog (Sep 13 2021 at 17:27):

but thanks for creating the issue, I'll try to comment there later this week.

Last updated: Oct 13 2024 at 01:02 UTC