Paolo Giarrusso (May 16 2020 at 10:46): 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
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
Emilio Jesús Gallego Arias (May 16 2020 at 10:57):For Ocaml, the modes do understand _build
Paolo Giarrusso (May 16 2020 at 10:59):oh, you mean the trick that I tried? Time to try proof general again...
Emilio Jesús Gallego Arias (May 16 2020 at 10:59):Yes Proof General will correctly pass -Q _build/default/theories to Coq
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
Paolo Giarrusso (May 16 2020 at 11:00):let me try harder
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!
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!
Paolo Giarrusso (May 16 2020 at 11:21):can dune call coqdoc?
Paolo Giarrusso (May 16 2020 at 11:22):with support for that I could probably drop makefiles entirely
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 :-)
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
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
Emilio Jesús Gallego Arias (May 16 2020 at 11:47):which are pretty easy to add
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...
Paolo Giarrusso (May 16 2020 at 13:45):(guess that's easy to fix for you...)
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
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
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
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.
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: Apr 19 2024 at 10:02 UTC