Hi there! For those interested who haven't seen it yet, the VsCoq 2 roadmap is here: https://github.com/orgs/coq-community/projects/2/views/4
Feel free to open feature requests!
dune coq top, etc.? I can open, but is this realistic?
You mean support for building coq projects which use Dune, when they are opened in a workspace?
I don't care for actually building anything. What I'd like to see support for in all UIs is just passing the right
-R based on what is in the
dune files, so we could potentially drop
a user just wants to run
dune build and then be able to step through any file
Ah, I see. So yes, this looks realistic. But I'm not sure if Coq has documented a standard Dune layout for Coq projects yet (I haven't followed this topic TBH).
VsCoq2 could use
dune coq top to get the information needed in meantime: https://github.com/ocaml/dune/pull/5457
Does it work for custom toplevels?
Oh it is discussed in the PR
no idea, but PG support for
dune coq top has apparently stalled: https://github.com/ProofGeneral/PG/issues/477
Anyway, yes, this deserves a feature request for sure
there is already https://github.com/coq-community/vscoq/issues/134 - should there be another for VsCoq2?
No, I'll just integrate it in the VsCoq 2 backlog, thanks!
for the record, the workaround with
-Q _build/default/theories D in
_CoqProject is terrible for my use case since it breaks coq_makefile builds. In many of my projects, I'd like to support both Dune and coq_makefile, both UI and in CI
FWIW, https://github.com/coq-community/vscoq/pull/319 has an alpha version for VsCoq1 (just swapping the backend) and you can probably get that far easily: that's enough for daily use, but
dune coq top _will_ rebuild dependencies if needed and that can take a while:
dune rpcinstead to let multiple clients launch concurrent builds
We were discussing it with @Laurent Théry indeed, it would be nice to merge it. As long as there are no regressions on
_CoqProject-based workflows, it is a strict improvement.
That was at least a design goal. But please let me revise a couple details...
(doing it today)
Currently the Dune devs are working on RPC support for top level commands (so they connect to watch mode). The current blocker is recieving error messages over RPC as only the server knows how to display them.
For commands like
dune exec there exist workarounds such as
--no-build to circurmvent locking of _build.
A lot of the slow down with Coq builds comes from coqdep being called individually. We can and shoud make this one call per theory. (Or remove coqdep but thats more work).
If you feel as though there are missing features in Dune support for Coq, please open issues so that we can track them.
the RPC issue is the main one I know of — I don't know if it's tracked but I knew at least you knew
Last updated: Jun 04 2023 at 22:30 UTC