Stream: Coq users

Topic: `_CoqProject` -> `dune`


view this post on Zulip Quinn (Nov 07 2021 at 18:18):

hello chaps. Has anyone made any progress on generating the coq.theory dune stanza from a traditional _CoqProject file?

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:20):

I don't think this is going to be done except as a hack. The discussion has much more been towards going from dune to _CoqProject and everyone dropping their _CoqProject files in repos. Essentially, _CoqProject is a largely undocumented format used by some Coq interfaces like ProofGeneral and VsCoq. _CoqProject is not required by Make/coq_makefile.

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:21):

see for example:

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:25):

if you're looking for Dune boilerplate autogeneration, we have some basic stuff for that here: https://github.com/coq-community/templates

view this post on Zulip Quinn (Nov 07 2021 at 18:29):

great, thanks!

view this post on Zulip Guillaume Melquiond (Nov 07 2021 at 18:29):

While _CoqProject is technically not required by coq_makefile, they are still closely related. The content of _CoqProject should be exactly what you fed to coq_makefile, in practice. So, as long as one uses coq_makefile, there is no good reason not to have a _CoqProject file.

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:32):

if you have a monorepo with 3-4 projects, you may not want to have a joint _CoqProject for all of them (e.g., since the build would take forever)

view this post on Zulip Guillaume Melquiond (Nov 07 2021 at 18:40):

Sure, but that is an argument against coq_makefile, not against _CoqProject, or am I misunderstanding? If you have several projects, you would have one _CoqProject file per project (as the name implies).

view this post on Zulip Quinn (Nov 07 2021 at 18:42):

it seems like proof general and vscoq interop are really important to target. I think of coq as primarily interactive.

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:43):

sure, it's nice to support editors and so on, but not needed in all contexts. I typically use Dune whenever I can in CI and keep some kind of _CoqProject build using coq_makefile as fallback for development.

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:45):

I think both coq_makefile and _CoqProject are essentially unsuited to monorepos. There is no good way to divide files into packages inside a single _CoqProject, and the editor will only read one _CoqProject per directory

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:47):

Dune works well for monorepo setups, but is near-unsupported by editors.

view this post on Zulip Quinn (Nov 07 2021 at 18:49):

yeah if you look at hs-to-coq's main Makefile they call coq_makefile on the _CoqProjects of subdirs before calling the make targets of those subdirs. Idk if it was the right way to do it (I'm the most recent committer on that Makefile), I just figured it worked well enough. I'm new to make but it doesn't strike me as being very opinionated about "correct" usage, it seems like you pretty much hack till it works.

view this post on Zulip Quinn (Nov 07 2021 at 18:52):

I've gotten decent proof general results in hs-to-coq (a monorepo) with a chain of _CoqProject files, somehow

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:53):

when you want library reuse, the hard problem in my opinion is to figure out how installation should work

view this post on Zulip Karl Palmskog (Nov 07 2021 at 18:56):

for a monorepo, this usually works nearly out of the box with Dune, but is likely to take a lot of make hacking with coq_makefile, if you want anything beyond "each directory is a completely self-contained project"


Last updated: Jan 31 2023 at 14:03 UTC