Stream: Dune devs & users

Topic: ✔ Dune, _CoqProject and tests


view this post on Zulip Notification Bot (Sep 08 2021 at 07:21):

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

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 10 2021 at 17:02):

Indeed, we should merge them !

view this post on Zulip Emilio Jesús Gallego Arias (Sep 10 2021 at 17:03):

Or maybe have several repos?

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

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

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

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

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

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

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

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