Quinn (Nov 07 2021 at 18:18): 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?
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.
Karl Palmskog (Nov 07 2021 at 18:21):see for example:
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
Quinn (Nov 07 2021 at 18:29):great, thanks!
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.
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)
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).
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.
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.
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
Karl Palmskog (Nov 07 2021 at 18:47):Dune works well for monorepo setups, but is near-unsupported by editors.
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.
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
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
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: Oct 05 2023 at 02:01 UTC