Stream: Coq devs & plugin devs

Topic: minimal coq make target


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

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 11:56):

make states

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

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

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 12:05):

Try building Ltac.vo

view this post on Zulip Gaëtan Gilbert (Dec 18 2020 at 12:08):

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

view this post on Zulip Enrico Tassi (Dec 18 2020 at 12:16):

it should, but it broke at some point

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

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 12:48):

I have a magic invocation for a basic fully functional coq

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:10):

make states should not be broken by the way

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:11):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:12):

sorry with bisects

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 15:12):

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

view this post on Zulip Fabian Kunze (Dec 18 2020 at 15:12):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:12):

Yup, you can also just build coqidetop if you want

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:14):

there are some tests tho , so they could be extended

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

view this post on Zulip Fabian Kunze (Dec 18 2020 at 15:15):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:15):

it is not so complicated

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:15):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:16):

similary for dune coqtop

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:17):

that also happens for the make setup

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:17):

IIANW

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:18):

so if coqc needs updating it will be updated

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

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

view this post on Zulip Fabian Kunze (Dec 18 2020 at 15:23):

dune build bin/coqidetop does not do what I hoped

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:31):

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:31):

binaries are a bit special

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:31):

or

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:32):

dune build ide/coqide/idetop.exe

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:32):

which is the "internal" binary name

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:33):

or many other rules that would pull it

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:33):

for example dune exec coqidetop.opt

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:34):

the package rules, etc...

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:36):

that's for example the rule for coqide testing:

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

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 15:37):

We should probably have a few more aliases.

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:38):

Sure @Pierre-Marie Pédrot

view this post on Zulip Kenji Maillard (Dec 18 2020 at 15:38):

And document them well...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:38):

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:39):

but the rest is very vanilla

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 18 2020 at 15:42):

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

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

view this post on Zulip 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: Oct 16 2021 at 03:02 UTC