Paolo Giarrusso (Dec 12 2022 at 03:42): Paolo Giarrusso (Dec 12 2022 at 03:42):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.
Paolo Giarrusso (Jan 03 2023 at 02:39):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
Paolo Giarrusso (Jan 03 2023 at 02:39):I guess the right fix for this would involve dune RPC?
Ali Caglayan (Jan 03 2023 at 20:03):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.
Ali Caglayan (Jan 03 2023 at 20:04):We could get dune coq top to do RPC however in the mean time.
Ali Caglayan (Jan 08 2023 at 16:31):Thanks for testing it out btw @Paolo Giarrusso
Paolo Giarrusso (Jan 08 2023 at 16:46):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
Ali Caglayan (Jan 08 2023 at 23:14):@Paolo Giarrusso Could you open an issue in Dune? We should be able to add some support for it.
Paolo Giarrusso (Jan 09 2023 at 00:04):filed https://github.com/ocaml/dune/issues/6847 (including a link here)
Ali Caglayan (Jan 09 2023 at 01:12):I submitted a fix
Last updated: Jun 04 2023 at 22:30 UTC