Dune + proof general

Using Coq
1

So far my understanding is that a project should contain

  1. the dune related files because it is overall a better build system (especially when one has pluggins

  2. Should contain the _CoqProject file and may be the generate make file so that Proof general is easily able to locate the .vo files in interactive setup.

Is my understanding wrong ? Can I setup proof general to look for the .vo files as generated by dune and be done with it ? I would prefer to switch completely to dune because of the overall awesomeness of it.

2

In the common case, the _CoqProject can list -Q prefix _build/default/theories etc — basically, prepend _build/default (or the appropriate path) to all the filesystem paths (even for plugins). Then you can omit the Makefile, and probably disable Proof General’s support for automatically building code. This is what I do these days.

An example is in Dune support · Issue #477 · ProofGeneral/PG · GitHub — the rest of that issue describes plans for better support.

2 Likes
3

Thanks it seems to work fine for me. For me the proofgeneral was in default configuration which meant it was anyway not automatically building. One more question do you do a dune --watch while developing ?

4

I never tried that, but I should! I’d hope it’d just work for Coq…