hello chaps. Has anyone made any progress on generating the
coq.theory dune stanza from a traditional
I don't think this is going to be done except as a hack. The discussion has much more been towards going from
_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.
see for example:
if you're looking for Dune boilerplate autogeneration, we have some basic stuff for that here: https://github.com/coq-community/templates
_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
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)
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).
it seems like proof general and vscoq interop are really important to target. I think of coq as primarily interactive.
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.
I think both
_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
Dune works well for monorepo setups, but is near-unsupported by editors.
yeah if you look at
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.
I've gotten decent proof general results in
hs-to-coq (a monorepo) with a chain of
_CoqProject files, somehow
when you want library reuse, the hard problem in my opinion is to figure out how installation should work
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