Stream: Coq users

Topic: dune support


view this post on Zulip Paolo Giarrusso (May 16 2020 at 10:46):

Trying out dune, caching is really cool, but of course IDEs (at least VsCoq) can't step through .v files — generated .vo files are in _build, so I either need make vos or I step through the copies of .v files in _build (which can't be edited).

But I can't find this mentioned in
https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20?u=blaisorblade or any of the links, so did _I_ do something wrong?

Also, is there a known easy workaround? Replacing -Q theories D with -Q _build/default/theories D in _CoqProject doesn't do it.
cc @Emilio Jesús Gallego Arias

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 10:57):

@Paolo G. Giarrusso , using the _CoqProject trick is what we have been doing in Proof General, it is very hacky but it does work fine until we reach a better solution. As of today I'm afraid that IDEs need to understand that the build directory is not the source directory, usually it should be easy to patch VsCoq so _build is used if it exists

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 10:57):

For Ocaml, the modes do understand _build

view this post on Zulip Paolo Giarrusso (May 16 2020 at 10:59):

oh, you mean the trick that I tried? Time to try proof general again...

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 10:59):

Yes Proof General will correctly pass -Q _build/default/theories to Coq

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 10:59):

VsCoq should do that too, I wonder otherwise how it can work in the non-Dune case

view this post on Zulip Paolo Giarrusso (May 16 2020 at 11:00):

let me try harder

view this post on Zulip Paolo Giarrusso (May 16 2020 at 11:01):

I’ll report back once I’ve investigated properly, but got other things to do first. Thanks!

view this post on Zulip Paolo Giarrusso (May 16 2020 at 11:20):

Well seems to work now — guess I made a mistake, but if something happens I'll complain again... however!

view this post on Zulip Paolo Giarrusso (May 16 2020 at 11:21):

can dune call coqdoc?

view this post on Zulip Paolo Giarrusso (May 16 2020 at 11:22):

with support for that I could probably drop makefiles entirely

view this post on Zulip Paolo Giarrusso (May 16 2020 at 11:24):

otherwise, I guess I could auto-generate a different _CoqProject with sed for invoking coq_makefile, it doesn't even seem hard :-)

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 11:47):

We will add coqdoc rules pretty soon I hope, also a method for PG / VsCoq to call Coq properly

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 11:47):

in fact I delayed the call for beta testers as I'd like to finish these features

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 11:47):

which are pretty easy to add

view this post on Zulip Paolo Giarrusso (May 16 2020 at 13:44):

But for coqdoc you need .glob files, and dune doesn't seem to produce them? In fact I can't even call coqdoc by hand using the dune output...

view this post on Zulip Paolo Giarrusso (May 16 2020 at 13:45):

(guess that's easy to fix for you...)

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 14:21):

yes, that should be easy to fix; it is waiting actually on better integration w.r.t. flags; for example if you pass -noglob to Coq dune will be confused as to why the .glob file was not produced

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 14:21):

I will tweak that shorly, as of today I'm short of cycles, but likely June will be fine

view this post on Zulip Enrico Tassi (May 16 2020 at 17:53):

Paolo G. Giarrusso said:

Well seems to work now — guess I made a mistake, but if something happens I'll complain again... however!

If this is the best way of using VSCoq with a dune built Coq project, it may be worth opening an issue (or a PR on the README) so that others can find it

view this post on Zulip Paolo Giarrusso (May 17 2020 at 13:29):

I've judged this to be best left to an issue, and filed https://github.com/coq-community/vscoq/issues/134 — I'd rather not waste Maxime's limited time on reviewing actual docs for this hack, and wait for better support.

view this post on Zulip Paolo Giarrusso (May 17 2020 at 13:31):

(sorry, that might have come off slightly wrong; I was just very uncertain and defending my choice, not criticizing anybody).


Last updated: Feb 01 2023 at 13:03 UTC