Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Setting up development environment


view this post on Zulip Ali Caglayan (Feb 15 2022 at 09:33):

Hi, if you have any questions about setting up your development environment, this is the place to ask! There is some documentation in https://github.com/coq/coq/tree/master/dev/doc but some of it might be outdated. Feel free to ask!

view this post on Zulip Tomás Díaz (Feb 16 2022 at 18:16):

While following the docs to build Coq I had some issues with some bits, which I'm not sure if they were obvious or if the docs could be improved on that regard. The docs say:

Today, the recommended method for building Coq is to use dune. Run make -f Makefile.dune to get help on the various available targets, Additional documentation can be found in dev/doc/build-system.dune.md, and in the official Dune documentation.

I went with make -f Makefile.dune (plus checking the Coq dune doc and saw that:

- check: build all ML files as fast as possible

(which also appears in other parts of the doc) So I ran it since it sounds obvious to go for that xd, and the build completed ok. I then went with dune exec -- dev/shim/coqtop-prelude , as I've seen other people do to get this.... REPL form (?) just to try it out, but failed due to Findlib error: coq-core.plugins.ltac not found in: .... Eventually found in the docs that

the check target is faster, as it doesn't link the binaries and uses the non-optimizing compiler.

So I guessed that maybe I needed the full thing? And so I built it with make -f Makefile.dune world and then the shim worked.

view this post on Zulip Tomás Díaz (Feb 16 2022 at 18:18):

Anyway, don't know if it was obvious, but I feel it was kind of missing something there (maybe because it's not a how-to guide :shrug: , idk)

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 18:21):

dune exec -- dev/shim/coqtop-prelude

this should work regardless of how little was previously compiled, I guess you hit some bug

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 18:26):

were you testing before https://github.com/coq/coq/pull/15601 ?

view this post on Zulip Tomás Díaz (Feb 16 2022 at 18:37):

huh.. no, this was a fresh pull (working on a Mac btw)

view this post on Zulip Ana de Almeida Borges (Feb 16 2022 at 19:05):

Even if this was a bug, I agree that the current description of the compilation targets is not completely obvious for me. For example, what is the difference between states: build a minimal functional coqtop and check: build all ML files as fast as possible?

view this post on Zulip Ana de Almeida Borges (Feb 16 2022 at 19:07):

One thing I've noticed is that make check doesn't work on my machine because I don't have the CoqIDE dependencies installed.

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 19:08):

states does not included eg extraction (or any other plugin not used by the prelude)
check only builds bytecode and does not produce executables

view this post on Zulip Paolo Giarrusso (Feb 16 2022 at 19:14):

@Tomás Díaz making these docs more accessible is part of the goal of this meeting (I guess)

view this post on Zulip Paolo Giarrusso (Feb 16 2022 at 21:53):

Now building with OCaml 4.14alpha2 ... is dune build --profile release the least invasive way to disable warning-as-error? --release enables more flags

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 22:09):

depends what you call invasive I guess
you can also edit the dune file to add something to (dev (flags :standard -rectypes -w -9-27+40+60-70 \ -short-paths))

view this post on Zulip Paolo Giarrusso (Feb 16 2022 at 22:11):

Thanks. Just found set break_on_load off to avoid breaking Module(s) Firstorder_plugin__Ground loaded., but am I doing something wrong or is it needed because of 4.14?

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 22:22):

I think break_on_load default on is probably meant for programs which don't usually load plugins at startup

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 22:22):

unlike coq

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 22:23):

AFAIK it's there since the ability to set breakpoints in dynlinked programs (4.12 IIRC), but ofc we can't use that until 4.14

view this post on Zulip Paolo Giarrusso (Feb 16 2022 at 22:32):

indeed, (dev (flags :standard -rectypes -w -3-9-27+40+60-70 \ -short-paths)) got me through make check

view this post on Zulip Paolo Giarrusso (Feb 16 2022 at 22:35):

https://ocaml.org/manual/debugger.html explains break_on_load exactly as you say, I was just wondering how to explain it in https://github.com/coq/coq/wiki/OCamldebug. I added something anyway.

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 09:20):

I confirm that calling only dune exec -- dev/shim/coqtop-prelude fails with Findlib error: coq-core.plugins.ltac not found in: [...] on latest master.

view this post on Zulip Ali Caglayan (Feb 17 2022 at 09:22):

Does dune build @check work?

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 09:24):

The command itself works, but calling dune exec -- dev/shim/coqtop-prelude afterwards still fails.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 09:27):

FWIW, dune exec -- dev/shim/coqtop-prelude does works for me on master

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 09:29):

From a clean tree?

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 09:32):

interesting... no:

(0 : 10:31:27) pgiarrusso1@KillBill(arm64):~/git-bedrock/coq$ dune clean
(0 : 10:31:29) pgiarrusso1@KillBill(arm64):~/git-bedrock/coq$ dune exec -- dev/shim/coqtop-prelude
File "theories/Init/_unknown_", line 1, characters 0-0:
Error: File unavailable:
/Users/pgiarrusso1/git-bedrock/coq/_build/install/default/lib/coq-core/META

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 09:32):

ah!

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 09:33):

the instructions in https://github.com/coq/coq/wiki/OCamldebug cover this, through a terrible hack:

get files in _build/install: dune build until it says something (after that you can interrupt). You only need to do this once, files in _build/install are symlinked so will pick up new builds Alternatively just dune build until it finishes (but takes more time)

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 09:33):

$ dune build @check
$ dune exec -- dev/shim/coqtop-prelude
File "theories/Init/_unknown_", line 1, characters 0-0:
Error: File unavailable:
/Users/pgiarrusso1/git-bedrock/coq/_build/install/default/lib/coq-core/META
$ dune build
      ocamlc ide/coqide/idetop.bc
    ocamlopt ide/coqide/coqide_gui.{a,cmxa}
    ocamlopt ide/coqide/coqide_main.exe
      coqdep theories/Arith/Compare_dec.v.d
      coqdep theories/Arith/Arith.v.d
      coqdep theories/Arith/Bool_nat.v.d
      coqdep theories/Arith/Cantor.v.d
    ocamlopt ide/coqide/idetop.exe
      coqdep theories/Arith/Arith_base.v.d
      coqdep theories/Arith/Between.v.d
      coqdep theories/Arith/Compare.v.d
      coqdep theories/Arith/Arith_prebase.v.d
<Ctrl-C>
$ dune exec -- dev/shim/coqtop-prelude
Welcome to Coq KillBill.local:/Users/pgiarrusso1/git-bedrock/coq/_build/default,master (87f54b09c80566736b30471590cd20f702ed0558)

Coq < ^D

view this post on Zulip Ali Caglayan (Feb 17 2022 at 09:34):

@Enrico Tassi Do you know what might be going wrong?

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 09:43):

@Paolo Giarrusso Indeed, Gaëtan also mentioned this trick during his presentation yesterday, but I had not understood why it was needed. Does this mean that these targets should depend on some install rules so that everything work out of the box?

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 09:51):

At least, I can confirm that the trick works also in my case. As soon as dune build prints something, everything works.

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 10:02):

Paolo Giarrusso said:

the instructions in https://github.com/coq/coq/wiki/OCamldebug cover this, through a terrible hack:

get files in _build/install: dune build until it says something (after that you can interrupt). You only need to do this once, files in _build/install are symlinked so will pick up new builds Alternatively just dune build until it finishes (but takes more time)

that's supposed to be only an ocamldebug bug, the shim is supposed to avoid this need

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 10:03):

Paolo Giarrusso said:

interesting... no:

(0 : 10:31:27) pgiarrusso1@KillBill(arm64):~/git-bedrock/coq$ dune clean
(0 : 10:31:29) pgiarrusso1@KillBill(arm64):~/git-bedrock/coq$ dune exec -- dev/shim/coqtop-prelude
File "theories/Init/_unknown_", line 1, characters 0-0:
Error: File unavailable:
/Users/pgiarrusso1/git-bedrock/coq/_build/install/default/lib/coq-core/META

that's https://github.com/coq/coq/issues/15608
but note the error message doesn't mention findlib, so @Jean-Christophe Léchenet may have another bug

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 10:05):

maybe they're the same bug though, I don't know

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 10:31):

not sure. It _might_ be they're both cases of "not enough is built" and different messages just mean "there's more or less stuff around"

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 10:41):

Okay, I do have dune 3.0 with caches

view this post on Zulip Gaëtan Gilbert (Feb 17 2022 at 10:43):

note that the "file unavailable" error is raised/printed by dune without running coq (AFAICT), the findlib error is from running coq.

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 10:46):

Actually, I cannot reproduce https://github.com/coq/coq/issues/15608. I have dune 2.9.3. I always get the same findlib error. I tried with and without the cache (not sure I did everything right though), still the same error.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 10:57):

either way, we have multiple shim bugs, with the same workaround. Until somebody can fix it, at least we can keep it in mind/document it :-|

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 11:07):

Interestingly, in my setup at least, you can "ctrl + c" right after the call to dune build. It seems dune refuses to get interrupted before setting up the symlinks.

view this post on Zulip Jean-Christophe Léchenet (Feb 17 2022 at 11:10):

Oh, but it not only creates symlinks, it also adds META files for instance. Let's say dune refuses to get interrupted before doing the unknown stuff that makes all the dune exec command work.

view this post on Zulip Paolo Giarrusso (Feb 17 2022 at 12:42):

New Q, I tried applying ocamldebug to coqide but got stuck on dlopen: https://github.com/coq/coq/issues/15486#issuecomment-1042909065


Last updated: Jan 29 2023 at 14:02 UTC