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.
Dune builds all its files under _build
directory, and this is not recognized by VsCoq yet, to my knowledge
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
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; runmake clean
to remove them.
What Karl said is still true — but dune
now supports the dune coq top
command
it would be a matter of making VSCoq use this command instead of calling coqidetop
directly
but yes, you'd definitely need to patch vscoq a bit
also, only recent Dune has dune coq top
, 3.X something? So should be detected by VsCoq if supported or not
True, and the first version had a serious enough bug
IIUC the first version of dune coq top
did not support coqidetop
correctly. Is that fixed?
If it is fixed, would it be sufficient to use the right settings in VsCoq (until VsCoq can detect this on its own)?
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
dune does support --toplevel=CMD (absent=coqtop)
and IIRC it did early on
the bug I hinted at earlier was fixed by https://github.com/ocaml/dune/pull/5901 in 3.4.0
I don't think I tested it myself so I'm just repeating what other said somewhere that I don't recall.
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
(I admit it was something like 3-4 months ago I even opened a file in VsCoq)
I do this trick in my _CoqProject
file for HoTT to allow for Dune support:
-R theories HoTT
-R _build/default/theories HoTT
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.
I have little idea if it works there either.
oh yeah me too re _CoqProject
@Ali Caglayan have you tried --toplevel=...
?
I assume you'd need to patch coqide for the right syntax
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
makes sense for PG since it calls coqtop seperately on each buffer
that's how vscoq works too
So the correct thing would be to intercept the call to coqidetop inside coqide so that it calls dune coq top
and last I tried that didn't work for me
We could at some point make it work, but I would just say use vscoq at this point :)
intercept the call to coqidetop inside coqide so that it calls dune coq top
agreed, was there another option?
and that would probably still not work for new files that you haven't saved
Huỳnh Trần Khanh has marked this topic as resolved.
Last updated: Sep 23 2023 at 08:01 UTC