I finally sat down and spent a moment to get basic support
dune coq top. This probably isn't even an Alpha, but it Works For Me and does the basic thing — I noted some limitations in the pull request: https://github.com/coq-community/vscoq/pull/319.
status report: I've been using this for a while, and the main problem on the dune side is with https://github.com/ocaml/dune/pull/6360: that MR is correct, but it prevents starting interaction with a file A while dune is active in the same repo — because you're building another file, or because another
dune coq top process is running
I guess the right fix for this would involve dune RPC?
There is a plan in the works for all Dune build commands to go through RPC eventually. This will allow dune builds to join a watch mode session etc. cc @Rudi Grinberg who can provide some more info.
We could get
dune coq top to do RPC however in the mean time.
Thanks for testing it out btw @Paolo Giarrusso
Welcome! It was overdue honestly.
Another small issue: dune passes -q to coqtop (from the :standard flags), which skips loading .coqrc, but that's not the standard workflow.
Not a huge deal of course, but coqrc is useful for "quick-n-dirty" settings like Nested Proof Allowed
@Paolo Giarrusso Could you open an issue in Dune? We should be able to add some support for it.
filed https://github.com/ocaml/dune/issues/6847 (including a link here)
I submitted a fix
Last updated: Jun 04 2023 at 22:30 UTC