Is there a make target that builds coq, but not the stdlib? (except for the prelude needed for Require-free .v files to behave the same as when everything is compiled)
make states
thanks, that greatly speeds up the bisect for coq/coq#13657. Somehow, the evar id of the goal does not get printed in the xml-protocol in 8.13
For my use case, also need the ltac_plugin.cmxs, but just building this file after make states
does not work
Try building Ltac.vo
shouldn't states build ltac_plugin since the prelude has ltac?
it should, but it broke at some point
I think my problem was that I did not build coq(ide)top, which was what I'm actually testing, and the broken cmxs was just a symptom of not cleaning
I have a magic invocation for a basic fully functional coq
make -j -l4 bin/coqc pluginsbyte tools miniopt coqide states printers bin/coqc.byte bin/coqchk miniopt states
wow, 14 seconds is fast :) thanks EDIT: ok, 14 seconds was because i did not cleanly build, but it still is fast
Doing bisect with make is always pretty painful, dune is faster and usually works better, dune build foo.vo
will work, or there is an special target jus the minimally functioning coqc with prelude dune exec -- dev/shim/coqc-prelude file.v
make states
should not be broken by the way
Oh, I see you were having problems with cleaning, indeed, that's the main problem, dune avoids this problems as the incremental build is sound
@Emilio Jesús Gallego Arias it's not broken, CoqIDE is not part of it.
For bisecting coqide + stdlib dev/shim/coqide-prelude
works and is sound
by the way my original motivation to start dune support was pain with bisects
sorry with bisects
Indeed, it's probably better to use dune for bisects.
Note that the bug was in coqidetop, which is used by more than just coqide.
Yup, you can also just build coqidetop if you want
tho the coqide target will take care of it and the overhead should be very low
(And the problem was basically that something got changed there for coqide, but without noticing that other users of coqidetop (e.g. vscoq) also use that feature, so it is good to highlight this here ^^
I was talking about the make
part of the bisect, but indeed, the test suite for the protocol is far from complete
(I don,t currently use dune as I only compile/hack coq once every month, and I use make all the other days of the month)
there are some tests tho , so they could be extended
As you have witnessed make is broken for incremental builds of OCaml projects so indeed if you are bisecting it is worth it
but I might should look into dune, probably after a git clean -Xf
it is not so complicated
I guess you will only need it if you plan to bisect again
but as a pointer here, my common bisect setup is fairly easy, the command I often run is dune build $deps.vo && dune exec dev/shim/coqc-prelude test.v
where $deps are the dependencies of test.v
, a new command dune coqc test.v
will automatically update test.v deps
similary for dune coqtop
so you don't need to know a lot to use, just have a clean tree and use that command
so depending on a vo file means that coq itself is also recompiled? (which is the selling point for dune as far as I heard from reading it's advertisement)
that also happens for the make setup
IIANW
rules for vo files do indeed depend on the hash of coqc plus deps of the v file
so if coqc needs updating it will be updated
dune is quite different from make so indeed there are many selling points if you want, in this context the main advantage is that dune build foo
will always produce a working build, incrementally
as compared to make, where you have to worry about other stuff, and most times make clean
is your only choice
dune build bin/coqidetop
does not do what I hoped
dune build _build/install/default/bin/coqidetop.opt is the right target
binaries are a bit special
or
dune build ide/coqide/idetop.exe
which is the "internal" binary name
or many other rules that would pull it
for example dune exec coqidetop.opt
the package rules, etc...
usually for testing is better to have a target as the ones defined in dev/shim/dune
In a rule you can write %{bin:coqidetop.opt}
, but that is not yet supported on the command line, may be fixed already in master
tho
why the above rules? For coqidetop, dune builds first idetop.exe
, then it installs it as coqidetop.opt
, you can depend on the build object or on the installed object
that's for example the rule for coqide testing:
(rule
(targets coqide-prelude)
(deps
%{bin:coqqueryworker.opt}
%{bin:coqtacticworker.opt}
%{bin:coqproofworker.opt}
%{project_root}/theories/Init/Prelude.vo
%{project_root}/coqide-server.install
%{project_root}/coqide.install)
(action
(with-stdout-to coqide-prelude
(progn
(echo "#!/usr/bin/env bash\n")
(bash "echo '$(dirname $0)/%{bin:coqide} -coqlib $(dirname $0)/%{project_root}' \\$@")
(run chmod +x %{targets})))))
We should probably have a few more aliases.
which says "build the workers, the prelude, the full two packages coqide and coqide-server", then generate the wrapper with the right paths
Sure @Pierre-Marie Pédrot
And document them well...
Sure also, documentation is a problem and the progress is not always monotonous
But overall Coq's setup is not so complex at all, these targets are the only ones that are a bit special, also the ocamldebug ones, which will hopefully supported by dune soon.
but the rest is very vanilla
The whole thing is just a dependency DAG, you tell dune which node you want built, and that it is
You need to know what the targets are tho, so in the Coq case, you have all OCaml standard ones https://dune.readthedocs.io/en/stable/usage.html?highlight=targets#built-in-aliases https://dune.readthedocs.io/en/stable/usage.html?highlight=targets#interpretation-of-targets
and the ones for .vo / .glob / .aux
files
we will introduce more targets upstream on the way, for example for deps of a file, and for the set of all .vo files of a theory
can I suggest to paste this chat into coq "build system" docs? fi "not so complex" ~= 60 msgs, it sounds like when mathematicians talk for hours and then conclude "oh, it's trivial!" :-P
Last updated: Dec 07 2023 at 14:02 UTC