Stream: Coq users

Topic: ✔ IDE support for Dune

Huỳnh Trần Khanh (Sep 30 2022 at 10:36):

After fumbling around, I managed to create a Coq project with Dune. But one thing I've noticed—the VsCoq extension does not recognize the project at all! So my From PackageName Require Import filename lines don't work in VS Code but my project still compiles nevertheless with dune build. I worked around by using _CoqProject. Is it true that there is no way the extension can recognize a Dune project? I took a look at the source code and looks like this is the case.

Karl Palmskog (Sep 30 2022 at 11:17):

Dune builds all its files under _build directory, and this is not recognized by VsCoq yet, to my knowledge

Karl Palmskog (Sep 30 2022 at 11:19):

for now, a not-so-satisfactory solution is to use coq_makefile as a parallel build system for the Coq project, and use this when developing with VsCoq. I go through all the boilerplate here for both Dune and Make: https://github.com/palmskog/coq-program-verification-template#file-and-directory-structure

Karl Palmskog (Sep 30 2022 at 11:41):

maybe worth repeating here this caveat, which I think still mostly holds:

coq_makefile and Dune builds are independent. However, for local development, it is recommended to use coq_makefile, since Coq IDEs may not be able find files compiled by Dune. Due to its build hygiene requirements, Dune will refuse to build when compiled (.vo) files are present in the theories directory; run make clean to remove them.

Paolo Giarrusso (Sep 30 2022 at 12:07):

What Karl said is still true — but dune now supports the dune coq top command

Paolo Giarrusso (Sep 30 2022 at 12:08):

it would be a matter of making VSCoq use this command instead of calling coqidetop directly

Paolo Giarrusso (Sep 30 2022 at 12:09):

but yes, you'd definitely need to patch vscoq a bit

Karl Palmskog (Sep 30 2022 at 12:09):

also, only recent Dune has dune coq top, 3.X something? So should be detected by VsCoq if supported or not

Paolo Giarrusso (Sep 30 2022 at 12:12):

True, and the first version had a serious enough bug

Théo Zimmermann (Sep 30 2022 at 12:25):

IIUC the first version of dune coq top did not support coqidetop correctly. Is that fixed?

Théo Zimmermann (Sep 30 2022 at 12:25):

If it is fixed, would it be sufficient to use the right settings in VsCoq (until VsCoq can detect this on its own)?

Paolo Giarrusso (Sep 30 2022 at 13:33):

I'm not aware of this problem, nor is the dune bug tracker: https://github.com/ocaml/dune/issues?q=is%3Aissue+is%3Aopen+coqidetop

Paolo Giarrusso (Sep 30 2022 at 13:33):

dune does support --toplevel=CMD (absent=coqtop) and IIRC it did early on

Paolo Giarrusso (Sep 30 2022 at 13:34):

the bug I hinted at earlier was fixed by https://github.com/ocaml/dune/pull/5901 in 3.4.0

Théo Zimmermann (Sep 30 2022 at 13:50):

I don't think I tested it myself so I'm just repeating what other said somewhere that I don't recall.

Karl Palmskog (Sep 30 2022 at 13:52):

the problem with debating IDEs for Coq: most people who weigh in on X probably don't use X, or it was so long ago the knowledge is obsolete

Karl Palmskog (Sep 30 2022 at 13:54):

(I admit it was something like 3-4 months ago I even opened a file in VsCoq)

Ali Caglayan (Sep 30 2022 at 13:57):

I do this trick in my _CoqProject file for HoTT to allow for Dune support:

-R theories HoTT
-R _build/default/theories HoTT

Ali Caglayan (Sep 30 2022 at 13:58):

I've never managed to get dune coq top to work for coqide. It was implemented for use with coqtop which is the backend to proof general.

Ali Caglayan (Sep 30 2022 at 13:59):

I have little idea if it works there either.

Paolo Giarrusso (Sep 30 2022 at 13:59):

oh yeah me too re _CoqProject

Paolo Giarrusso (Sep 30 2022 at 13:59):

@Ali Caglayan have you tried --toplevel=...?

Paolo Giarrusso (Sep 30 2022 at 14:01):

I assume you'd need to patch coqide for the right syntax

Ali Caglayan (Sep 30 2022 at 14:01):

But the issue is that dune coq top is meant to be called like dune coq top --toplevel=coqide file.v if you open an new file inside it won't work

Ali Caglayan (Sep 30 2022 at 14:01):

makes sense for PG since it calls coqtop seperately on each buffer

Paolo Giarrusso (Sep 30 2022 at 14:02):

that's how vscoq works too

Ali Caglayan (Sep 30 2022 at 14:03):

So the correct thing would be to intercept the call to coqidetop inside coqide so that it calls dune coq top

Ali Caglayan (Sep 30 2022 at 14:03):

and last I tried that didn't work for me

Ali Caglayan (Sep 30 2022 at 14:03):

We could at some point make it work, but I would just say use vscoq at this point :)

Paolo Giarrusso (Sep 30 2022 at 14:04):

intercept the call to coqidetop inside coqide so that it calls dune coq top

agreed, was there another option?

Paolo Giarrusso (Sep 30 2022 at 14:04):

and that would probably still not work for new files that you haven't saved

Notification Bot (Sep 30 2022 at 16:27):

Huỳnh Trần Khanh has marked this topic as resolved.

Last updated: Sep 23 2023 at 08:01 UTC