Pierre-Marie Pédrot (Apr 27 2021 at 12:04): Pierre-Marie Pédrot (Apr 27 2021 at 12:04):When launching coqide through the dune wrapper, I get a warning "file ide/default.binding missing", is that a known problem?
Pierre-Marie Pédrot (Apr 27 2021 at 12:04):There does not seem to be an issue reported yet.
Pierre-Marie Pédrot (Apr 27 2021 at 12:04):(Also the wrapper is agonizingly slow, it takes like 3s to fire, but I guess I'll have to live with tat.)
Pierre-Marie Pédrot (Apr 27 2021 at 12:08):if I read correctly the wrapper the only point of it is to pass the -coqlib option, shouldn't I simply export the COQLIB var and call the binaries as before?
Théo Zimmermann (Apr 27 2021 at 12:14):If you call the wrapper through dune exec, then it will rebuild anything that needs to be.
Pierre-Marie Pédrot (Apr 27 2021 at 12:14):there is nothing to rebuild
Théo Zimmermann (Apr 27 2021 at 12:14):I mean in general.
Pierre-Marie Pédrot (Apr 27 2021 at 12:14):it's probably just looking at files
Théo Zimmermann (Apr 27 2021 at 12:14):But passing COQLIB should work just fine.
Pierre-Marie Pédrot (Apr 27 2021 at 12:14):if I can call the binary directly I'd be happy
Gaëtan Gilbert (Apr 27 2021 at 12:15):If you know there's nothing to rebuild you can call it directly
Théo Zimmermann (Apr 27 2021 at 12:15):As for the missing default.binding issue, indeed, I've seen that too recently, it was not there before I believe.
Pierre-Marie Pédrot (Apr 27 2021 at 12:15):what's the expected value for COQLIB?
Théo Zimmermann (Apr 27 2021 at 12:15):Do you build with make or with make -f Makefile.dune ?
Pierre-Marie Pédrot (Apr 27 2021 at 12:16):make but it doesn't do a different now, does it?
Théo Zimmermann (Apr 27 2021 at 12:16):Well, the theories files will be somewhere different.
Pierre-Marie Pédrot (Apr 27 2021 at 12:17):setting COQLIB to point to _build_vo/default seems to do the trick
Théo Zimmermann (Apr 27 2021 at 12:18):The coqide-prelude wrapper is really thought for using with the full Dune build system. Sometimes it can be slow because it's rebuilding stuff. Unfortunately, it doesn't print anything when it does. (As opposed to dune build dev/shims/coqide-prelude.)
Pierre-Marie Pédrot (Apr 27 2021 at 12:18):No, it really doesn't, I've set the verbose option.
Théo Zimmermann (Apr 27 2021 at 12:19):OK
Pierre-Marie Pédrot (Apr 27 2021 at 12:19):It's just taking 2-3s checking there is nothing to rebuild I believe
Théo Zimmermann (Apr 27 2021 at 12:19):Sounds plausible.
Pierre-Marie Pédrot (Apr 27 2021 at 12:19):but I don't mind now that I can call the binary directly.
Pierre-Marie Pédrot (Apr 27 2021 at 12:19):I'll try to write a fix for the binding warnign
Théo Zimmermann (Apr 27 2021 at 12:20):Pierre-Marie Pédrot said:
setting COQLIB to point to
_build_vo/defaultseems to do the trick
That might be worth documenting. I don't think it was done yet.
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:22):@Pierre-Marie Pédrot that timing for the empty rebuild seems slow, what dune version you are using?
Pierre-Marie Pédrot (Apr 27 2021 at 12:22):2.7.1
Pierre-Marie Pédrot (Apr 27 2021 at 12:23):regarding the warning, coqide is looking for the file in coqlib it seems
Pierre-Marie Pédrot (Apr 27 2021 at 12:23):but the directory doesn't seem to be correctly set in coqide for some reason
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:25):File a bug and I will fix it, there are still some adjustments to make, likely this bug is just some missing dep.
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:25):Let me know if dune 2.8.5 is faster in the no-op build
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:25):no-op build is benchmarked often for performance, I will profile it myself to see what is going on
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:26):but indeed anything less that instantaneous for a no-op build is considered a Dune bug
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:29):By the way @Pierre-Marie Pédrot there are many things yet to improve / fix in the setup, so don't hesitate to report bugs / write here.
You could tho try to set COQ_USE_DUNE=1 as for devs should provide a much better experience [and you can use things like dune build @check in a supported way]
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:33):Also, I rarely use verbose, I just watch _build/log directly inside an emacs buffer and use syntax coloring; in case of errors, Dune usually spits out the right command to reproduce the error just by cut and past.
Gaëtan Gilbert (Apr 27 2021 at 12:33):what syntax coloring?
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:35):A very basic regexp, maybe I should upstream it so we have a dune-log-mode in emacs
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:35):Tho ocaml-lsp + vscode should do their own thing I guess
Pierre-Marie Pédrot (Apr 27 2021 at 12:36):I am neither an Emacs user nor a vscode user so...
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:42):Well, same applies, you can just keep _build/log watched using your favorite tool.
Pierre-Marie Pédrot (Apr 27 2021 at 12:43):dune 2.8.5 seems to be a bit faster not to do anything but there is still a noticeably latency compared with bare binary calling
Pierre-Marie Pédrot (Apr 27 2021 at 12:44):it's more like 1-1.5s now
Pierre-Marie Pédrot (Apr 27 2021 at 12:45):also, just doing make coqide is not enough to actually launch coqide, it doesn't compile the server
Pierre-Marie Pédrot (Apr 27 2021 at 12:45):it's necessary to build the shim instead
Pierre-Marie Pédrot (Apr 27 2021 at 12:45):I don't quite understand where the coqide target is defined in the Makefile wrapper actually
Pierre-Marie Pédrot (Apr 27 2021 at 12:46):I am thus surprised this invocation produces anything at all
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:51):coqide is defined in Makefile.ide , it should build idetop and prelude tho
Pierre-Marie Pédrot (Apr 27 2021 at 12:52):but where is that made available to Makefile.dune?
Gaëtan Gilbert (Apr 27 2021 at 12:53):Makefile.dune is not used unless you -f it or use the env variable
Gaëtan Gilbert (Apr 27 2021 at 12:53):(COQ_USE_DUNE)
Pierre-Marie Pédrot (Apr 27 2021 at 12:53):aha, I see
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:53):Yup, for Makefile.dune there is no target for coqide, that is taken care by dev/shim/dune, and will be moved to dune coqtop --ide for 2.9
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:54):So you can do dune coqtop --ide foo.v and you get all the things needed up to foo.v updated
Pierre-Marie Pédrot (Apr 27 2021 at 12:54):I confirm that for Makefile.make, coqide is not runnable after a clean + make coqide
Pierre-Marie Pédrot (Apr 27 2021 at 12:54):I get Handshake with proofworker:0 failed: End_of_file
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:54):Ok, noted [you can file a bug if you want but I've added this to my todo list]
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:55):the fix seems easy, just a missing dep
Pierre-Marie Pédrot (Apr 27 2021 at 12:55):a quick look at the binary available show that coqidetop.opt is there but the worker binaries are not
Pierre-Marie Pédrot (Apr 27 2021 at 12:55):OK I'll open a bug report
Théo Zimmermann (Apr 27 2021 at 13:25):Emilio Jesús Gallego Arias said:
So you can do
dune coqtop --ide foo.vand you get all the things needed up tofoo.vupdated
Curious: why dune coqtop --ide and not dune coqide?
Last updated: Dec 06 2023 at 14:01 UTC