Ali Caglayan (Feb 15 2022 at 09:33): 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!
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.
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)
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
Gaëtan Gilbert (Feb 16 2022 at 18:26):were you testing before https://github.com/coq/coq/pull/15601 ?
Tomás Díaz (Feb 16 2022 at 18:37):huh.. no, this was a fresh pull (working on a Mac btw)
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?
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.
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
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)
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
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))
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?
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
Gaëtan Gilbert (Feb 16 2022 at 22:22):unlike coq
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
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
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.
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.
Ali Caglayan (Feb 17 2022 at 09:22):Does dune build @check work?
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.
Paolo Giarrusso (Feb 17 2022 at 09:27):FWIW, dune exec -- dev/shim/coqtop-prelude does works for me on master
Jean-Christophe Léchenet (Feb 17 2022 at 09:29):From a clean tree?
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
ah!
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)
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
@Enrico Tassi Do you know what might be going wrong?
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?
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.
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
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
Gaëtan Gilbert (Feb 17 2022 at 10:05):maybe they're the same bug though, I don't know
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"
Paolo Giarrusso (Feb 17 2022 at 10:41):Okay, I do have dune 3.0 with caches
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.
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.
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 :-|
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.
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.
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: Jun 10 2023 at 23:01 UTC