Maxime Dénès (Feb 10 2023 at 09:36): Maxime Dénès (Feb 10 2023 at 09:36):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!
Karl Palmskog (Feb 10 2023 at 09:38):Dune support? dune coq top, etc.? I can open, but is this realistic?
Maxime Dénès (Feb 10 2023 at 09:43):You mean support for building coq projects which use Dune, when they are opened in a workspace?
Karl Palmskog (Feb 10 2023 at 09:45):I don't care for actually building anything. What I'd like to see support for in all UIs is just passing the right -Q/-R based on what is in the dune files, so we could potentially drop _CoqProject
Karl Palmskog (Feb 10 2023 at 09:45):a user just wants to run dune build and then be able to step through any file
Maxime Dénès (Feb 10 2023 at 09:46):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).
Karl Palmskog (Feb 10 2023 at 09:47):VsCoq2 could use dune coq top to get the information needed in meantime: https://github.com/ocaml/dune/pull/5457
Maxime Dénès (Feb 10 2023 at 09:49):Does it work for custom toplevels?
Maxime Dénès (Feb 10 2023 at 09:49):Oh it is discussed in the PR
Karl Palmskog (Feb 10 2023 at 09:49):no idea, but PG support for dune coq top has apparently stalled: https://github.com/ProofGeneral/PG/issues/477
Maxime Dénès (Feb 10 2023 at 09:51):Anyway, yes, this deserves a feature request for sure
Karl Palmskog (Feb 10 2023 at 09:53):there is already https://github.com/coq-community/vscoq/issues/134 - should there be another for VsCoq2?
Maxime Dénès (Feb 10 2023 at 09:57):No, I'll just integrate it in the VsCoq 2 backlog, thanks!
Karl Palmskog (Feb 10 2023 at 10:06):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
Paolo Giarrusso (Feb 10 2023 at 13:21):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 rpc instead to let multiple clients launch concurrent builds Maxime Dénès (Feb 10 2023 at 13:31):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.
Paolo Giarrusso (Feb 10 2023 at 13:56):That was at least a design goal. But please let me revise a couple details...
Paolo Giarrusso (Feb 10 2023 at 13:56):(doing it today)
Ali Caglayan (Feb 10 2023 at 17:36):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.
Ali Caglayan (Feb 10 2023 at 17:38):For commands like dune exec there exist workarounds such as --no-build to circurmvent locking of _build.
Ali Caglayan (Feb 10 2023 at 17:39):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).
Ali Caglayan (Feb 10 2023 at 17:39):If you feel as though there are missing features in Dune support for Coq, please open issues so that we can track them.
Paolo Giarrusso (Feb 10 2023 at 17:51):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