When launching coqide through the dune wrapper, I get a warning "file ide/default.binding missing", is that a known problem?
There does not seem to be an issue reported yet.
(Also the wrapper is agonizingly slow, it takes like 3s to fire, but I guess I'll have to live with tat.)
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?
If you call the wrapper through dune exec
, then it will rebuild anything that needs to be.
there is nothing to rebuild
I mean in general.
it's probably just looking at files
But passing COQLIB
should work just fine.
if I can call the binary directly I'd be happy
If you know there's nothing to rebuild you can call it directly
As for the missing default.binding issue, indeed, I've seen that too recently, it was not there before I believe.
what's the expected value for COQLIB?
Do you build with make
or with make -f Makefile.dune
?
make
but it doesn't do a different now, does it?
Well, the theories files will be somewhere different.
setting COQLIB to point to _build_vo/default
seems to do the trick
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
.)
No, it really doesn't, I've set the verbose option.
OK
It's just taking 2-3s checking there is nothing to rebuild I believe
Sounds plausible.
but I don't mind now that I can call the binary directly.
I'll try to write a fix for the binding warnign
Pierre-Marie Pédrot said:
setting COQLIB to point to
_build_vo/default
seems to do the trick
That might be worth documenting. I don't think it was done yet.
@Pierre-Marie Pédrot that timing for the empty rebuild seems slow, what dune version you are using?
2.7.1
regarding the warning, coqide is looking for the file in coqlib it seems
but the directory doesn't seem to be correctly set in coqide for some reason
File a bug and I will fix it, there are still some adjustments to make, likely this bug is just some missing dep.
Let me know if dune 2.8.5 is faster in the no-op build
no-op build is benchmarked often for performance, I will profile it myself to see what is going on
but indeed anything less that instantaneous for a no-op build is considered a Dune bug
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]
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.
what syntax coloring?
A very basic regexp, maybe I should upstream it so we have a dune-log-mode
in emacs
Tho ocaml-lsp + vscode should do their own thing I guess
I am neither an Emacs user nor a vscode user so...
Well, same applies, you can just keep _build/log
watched using your favorite tool.
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
it's more like 1-1.5s now
also, just doing make coqide
is not enough to actually launch coqide, it doesn't compile the server
it's necessary to build the shim instead
I don't quite understand where the coqide
target is defined in the Makefile wrapper actually
I am thus surprised this invocation produces anything at all
coqide
is defined in Makefile.ide
, it should build idetop and prelude tho
but where is that made available to Makefile.dune?
Makefile.dune is not used unless you -f it or use the env variable
(COQ_USE_DUNE)
aha, I see
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
So you can do dune coqtop --ide foo.v
and you get all the things needed up to foo.v
updated
I confirm that for Makefile.make, coqide is not runnable after a clean + make coqide
I get Handshake with proofworker:0 failed: End_of_file
Ok, noted [you can file a bug if you want but I've added this to my todo list]
the fix seems easy, just a missing dep
a quick look at the binary available show that coqidetop.opt is there but the worker binaries are not
OK I'll open a bug report
Emilio Jesús Gallego Arias said:
So you can do
dune coqtop --ide foo.v
and you get all the things needed up tofoo.v
updated
Curious: why dune coqtop --ide
and not dune coqide
?
Last updated: Jun 04 2023 at 19:30 UTC