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
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
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.
It's just taking 2-3s checking there is nothing to rebuild I believe
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/defaultseems 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?
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
aha, I see
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
I confirm that for Makefile.make, coqide is not runnable after a clean +
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.vand you get all the things needed up to
dune coqtop --ide and not
Last updated: Dec 06 2023 at 14:01 UTC