Stream: Coq devs & plugin devs

Topic: coqide & dune wrapper


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:04):

There does not seem to be an issue reported yet.

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:14):

there is nothing to rebuild

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:14):

I mean in general.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:14):

it's probably just looking at files

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:14):

But passing COQLIB should work just fine.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:14):

if I can call the binary directly I'd be happy

view this post on Zulip Gaëtan Gilbert (Apr 27 2021 at 12:15):

If you know there's nothing to rebuild you can call it directly

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:15):

what's the expected value for COQLIB?

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:15):

Do you build with make or with make -f Makefile.dune ?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:16):

make but it doesn't do a different now, does it?

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:16):

Well, the theories files will be somewhere different.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:17):

setting COQLIB to point to _build_vo/default seems to do the trick

view this post on Zulip 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.)

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:18):

No, it really doesn't, I've set the verbose option.

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:19):

OK

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:19):

It's just taking 2-3s checking there is nothing to rebuild I believe

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:19):

Sounds plausible.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:19):

but I don't mind now that I can call the binary directly.

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:19):

I'll try to write a fix for the binding warnign

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 12:20):

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.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:22):

2.7.1

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:23):

regarding the warning, coqide is looking for the file in coqlib it seems

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Apr 27 2021 at 12:33):

what syntax coloring?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 12:35):

Tho ocaml-lsp + vscode should do their own thing I guess

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:36):

I am neither an Emacs user nor a vscode user so...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:44):

it's more like 1-1.5s now

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:45):

it's necessary to build the shim instead

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:46):

I am thus surprised this invocation produces anything at all

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 12:51):

coqide is defined in Makefile.ide , it should build idetop and prelude tho

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:52):

but where is that made available to Makefile.dune?

view this post on Zulip Gaëtan Gilbert (Apr 27 2021 at 12:53):

Makefile.dune is not used unless you -f it or use the env variable

view this post on Zulip Gaëtan Gilbert (Apr 27 2021 at 12:53):

(COQ_USE_DUNE)

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:53):

aha, I see

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:54):

I get Handshake with proofworker:0 failed: End_of_file

view this post on Zulip 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]

view this post on Zulip Emilio Jesús Gallego Arias (Apr 27 2021 at 12:55):

the fix seems easy, just a missing dep

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Apr 27 2021 at 12:55):

OK I'll open a bug report

view this post on Zulip Théo Zimmermann (Apr 27 2021 at 13:25):

Emilio Jesús Gallego Arias said:

So you can do dune coqtop --ide foo.v and you get all the things needed up to foo.v updated

Curious: why dune coqtop --ide and not dune coqide?


Last updated: Oct 21 2021 at 21:03 UTC