Stream: Coq devs & plugin devs

Topic: minimal coq make target

Fabian Kunze (Dec 18 2020 at 11:55):

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)

Pierre-Marie Pédrot (Dec 18 2020 at 11:56):

make states

Fabian Kunze (Dec 18 2020 at 11:58):

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

Fabian Kunze (Dec 18 2020 at 12:04):

For my use case, also need the ltac_plugin.cmxs, but just building this file after make states does not work

Pierre-Marie Pédrot (Dec 18 2020 at 12:05):

Try building Ltac.vo

Gaëtan Gilbert (Dec 18 2020 at 12:08):

shouldn't states build ltac_plugin since the prelude has ltac?

Enrico Tassi (Dec 18 2020 at 12:16):

it should, but it broke at some point

Fabian Kunze (Dec 18 2020 at 12:46):

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

Pierre-Marie Pédrot (Dec 18 2020 at 12:48):

I have a magic invocation for a basic fully functional coq

Pierre-Marie Pédrot (Dec 18 2020 at 12:48):

make -j -l4  bin/coqc pluginsbyte tools miniopt coqide states printers bin/coqc.byte bin/coqchk miniopt states

Fabian Kunze (Dec 18 2020 at 12:51):

wow, 14 seconds is fast :) thanks EDIT: ok, 14 seconds was because i did not cleanly build, but it still is fast

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:10):

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

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:10):

make states should not be broken by the way

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:10):

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

Pierre-Marie Pédrot (Dec 18 2020 at 15:10):

@Emilio Jesús Gallego Arias it's not broken, CoqIDE is not part of it.

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:11):

For bisecting coqide + stdlib dev/shim/coqide-prelude works and is sound

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:12):

by the way my original motivation to start dune support was pain with bisects

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:12):

sorry with bisects

Pierre-Marie Pédrot (Dec 18 2020 at 15:12):

Indeed, it's probably better to use dune for bisects.

Fabian Kunze (Dec 18 2020 at 15:12):

Note that the bug was in coqidetop, which is used by more than just coqide.

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:12):

Yup, you can also just build coqidetop if you want

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:12):

tho the coqide target will take care of it and the overhead should be very low

Fabian Kunze (Dec 18 2020 at 15:13):

(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 ^^

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:14):

I was talking about the make part of the bisect, but indeed, the test suite for the protocol is far from complete

Fabian Kunze (Dec 18 2020 at 15:14):

(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)

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:14):

there are some tests tho , so they could be extended

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:15):

As you have witnessed make is broken for incremental builds of OCaml projects so indeed if you are bisecting it is worth it

Fabian Kunze (Dec 18 2020 at 15:15):

but I might should look into dune, probably after a git clean -Xf

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:15):

it is not so complicated

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:15):

I guess you will only need it if you plan to bisect again

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:16):

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

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:16):

where $deps are the dependencies of test.v, a new command dune coqc test.v will automatically update test.v deps

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:16):

similary for dune coqtop

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:17):

so you don't need to know a lot to use, just have a clean tree and use that command

Fabian Kunze (Dec 18 2020 at 15:17):

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)

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:17):

that also happens for the make setup

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:17):

IIANW

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:18):

rules for vo files do indeed depend on the hash of coqc plus deps of the v file

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:18):

so if coqc needs updating it will be updated

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:19):

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

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:19):

as compared to make, where you have to worry about other stuff, and most times make clean is your only choice

Fabian Kunze (Dec 18 2020 at 15:23):

dune build bin/coqidetop does not do what I hoped

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:31):

dune build _build/install/default/bin/coqidetop.opt is the right target

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:31):

binaries are a bit special

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:31):

or

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:32):

dune build ide/coqide/idetop.exe

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:32):

which is the "internal" binary name

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:33):

or many other rules that would pull it

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:33):

for example dune exec coqidetop.opt

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:34):

the package rules, etc...

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:34):

usually for testing is better to have a target as the ones defined in dev/shim/dune

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:35):

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

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:36):

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

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:36):

that's for example the rule for coqide testing:

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:36):

(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})))))

Pierre-Marie Pédrot (Dec 18 2020 at 15:37):

We should probably have a few more aliases.

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:38):

which says "build the workers, the prelude, the full two packages coqide and coqide-server", then generate the wrapper with the right paths

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:38):

Sure @Pierre-Marie Pédrot

Kenji Maillard (Dec 18 2020 at 15:38):

And document them well...

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:38):

Sure also, documentation is a problem and the progress is not always monotonous

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:39):

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.

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:39):

but the rest is very vanilla

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:41):

The whole thing is just a dependency DAG, you tell dune which node you want built, and that it is

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:42):

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

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:42):

and the ones for .vo / .glob / .aux files

Emilio Jesús Gallego Arias (Dec 18 2020 at 15:43):

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

Paolo Giarrusso (Dec 18 2020 at 19:18):

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: Jun 08 2023 at 04:01 UTC