coqc usage · Coq devs & plugin devs

I'm using Bazel to build Coq, and and I need help with coqc usage (I've never used it before). My command line is
bazel-out/host/bin/topbin/coqc theories/Init/Prelude.v -coqlib . -q -noinit -R . Coq. The output is a bunch of warnings like

Warning:
/private/var/tmp/_bazel_gar/8c949035aafa6229d33cef095568e3f8/sandbox/darwin-sandbox/1/execroot/coq/theories/btauto
was previously bound to Coq.btauto; it is remapped to Coq.theories.btauto
[overriding-logical-loadpath,loadpath]

File "./theories/Init/Prelude.v", line 11, characters 15-24:
Error: Syntax error: entry [global] is empty.

Guillaume Melquiond (Apr 01 2021 at 06:46):

Guillaume Melquiond (Apr 01 2021 at 06:51):

Also, possibly, when building the .v files from the Init directory, you might want to pass the -boot option.

Emilio Jesús Gallego Arias (Apr 01 2021 at 09:08):

Indeed if you pass -R dir Coq, you want to use -boot so Coq doesn't add that path automatically

Emilio Jesús Gallego Arias (Apr 01 2021 at 09:09):

Tho, you will have in that case to manually add -I plugins/p1 ... -i plugins/p2 to your command line, as -boot also removes the automatic ml path additions

Gregg Reynolds (Apr 01 2021 at 11:43):

 bazel-out/host/bin/topbin/coqc theories/Init/Prelude.v -boot -noinit -I plugins/btauto ...omitted... -I plugins/syntax -coqlib . -q -noinit -R theories Coq
...
File "./theories/Init/Prelude.v", line 11, characters 15-24:
Error: Syntax error: entry [global] is empty.

Question: what does coqc expect to see in the plugin dirs? OCaml source, or the compiled plugins?

Gregg Reynolds (Apr 01 2021 at 11:47):

FYI, Bazel requires that the build program explicitly list all inputs required by an action (in this case, running coqc). So I guess what I really need to know is the list of stuff upon which coqc implicitly depends. For example, it needs to find a "plugins" dir, but I need to enumerate the actual files it wants to use (I can glob this if I know what to glob.)

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:43):

You didn't link coqc correctly it seems, you must use -linkall and pass the corresponding g_* grammar files

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:43):

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:44):

To compile file.v, if you called coqdep correctly, it will list all inputs needed, tho there is a transitivity condition if you are sandboxing

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:45):

In the sense that if foo.v Require bar., then coqdep will emit a dependency on bar.vo

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:45):

however the dependencies of bar.vo must also be in scope as Coq does "dynamic loading" of .vo files

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:46):

Gregg Reynolds (Apr 01 2021 at 12:58):

Haha, it took me six months to get the Bazel rules mostly correct; it seems like every time I think I've got it all figured out I run into a new problem.

I was wondering about the dep structure; I have not used coqdep yet, that's obviously the next step.

Regarding cmxs files: for the plugins currently I just build a cmxa file that includes the aliasing file (Foo_plugin.cmx); evidently I need to output cmxs files too?

Regarding the coqc build: I do use -linkall, and I _think_ all the g_* files are correctly handled, but I'll double check, thanks.

A little background info In case bazel-out/host/bin/topbin/coqc looks funny: I build everything where its (main) sources live. So since coqc is built from coqc_bin.ml, which is in toplevel, that's where I build it. It simplifies things, and it works in Bazel since one always refers to stuff using Bazel labels, which Bazel resolves to file system locations, and it just arranges things so they work. So here is where the executable build targets live:

$ bazel query 'kind(ocaml_executable, //...)' | sort
//checker:coqchk
//checker:votour
//config:genOpcodeFiles
//config:list_plugins
//coqpp:coqpp
//ide/coqide:default_bindings_src
//ide/coqide:fake_ide
//kernel:genOpcodeFiles
//plugins/micromega:csdpcert
//tools/coqdoc:coqdoc
//tools:coq-tex
//tools:coq_makefile
//tools:coqdep
//tools:coqdep_boot
//tools:coqwc
//tools:coqworkmgr
//tools:ocamllibdep
//topbin:coqc
//topbin:coqproofworker
//topbin:coqqueryworker
//topbin:coqtacticworker
//topbin:coqtop.byte
//topbin:coqtop.opt

Emilio Jesús Gallego Arias (Apr 01 2021 at 13:08):

Are you aware of the current work on Dune for Coq? This makes 99% of Bazel features redundant [as I discussed on twitter] , I can say there is a lot of work ahead yet IMHO to get the Bazel build feature complete.

Enrico Tassi (Apr 01 2021 at 13:15):

May I ask why you are writing bazel support @Gregg Reynolds ? Are you developing some coq plugin or coq feature, and you found the build system not covering your needs?

Théo Zimmermann (Apr 01 2021 at 13:24):

Gregg Reynolds (Apr 01 2021 at 13:25):

Mostly to test my build rules, and for fun. Sadly I have not used Coq much, it's been on my list for years but I never seem to find the time. But it's the flagship app for OCaml, so its a good test. The rules seem to work great for the OCaml parts of Coq. coqc is a whole 'nother animal, but since it's needed to get a complete Coq build, I might as well try to write a Bazel rule for it. I'm sure to learn a little more about it at the very least.

Gregg Reynolds (Apr 01 2021 at 13:41):

@Emilio Jesús Gallego Arias Regarding composition of Coq theories: I'll let you know once I figure out how to compile .v files.

Yes, I am aware of the Dune work. Whether or not that makes "99% of Bazel features redundant" is debatable, but in any case I don't see it as an either/or proposition. If I can get a good Bazel build going with a reasonable amount of effort, great, we'll have another build option that people can use or not, it would be an engineering decision at that point. I expect I'll spend another day or two trying to figure out coqc and then decide whether it's worth the effort to try to get to feature complete.

Emilio Jesús Gallego Arias (Apr 01 2021 at 13:41):

Bazel provides very nice features in terms for example of multi-language repositories [which is quite common on industrial contexts for Coq] and build times in particular build sharing which is also pretty important in industrial contexts

Gregg Reynolds (Apr 01 2021 at 13:47):

Case in point: Mina uses Go and Rust libs, and used to use some big C++ libs. Bazel makes that kind of integration a breeze.

Another feature that I've found extremely useful is the query feature. Very easy to print the dependency paths between two targets for example, if if a target is failing, you can ask Bazel to print the build command and list of all inputs without actually running the build. Huge time saver.

Enrico Tassi (Apr 01 2021 at 14:12):

Naive question: is obazl going to superseed dune anytime soon? To my eyes bazl seems more mature and widely adopted than dune, but dune obviously comes with good ocaml support out of the box. Is obazl filling (all) that gap? (I could not find a good comparison of obazl and dune, and from what I can tell bazl and dune's core ideas are close)

Théo Zimmermann (Apr 01 2021 at 14:26):

AFAICT, the investment of the OCaml community is on Dune. Given that, there's no reason for a general shift to Bazel.

Enrico Tassi (Apr 01 2021 at 14:29):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:30):

If the question is "is obazl going to superseed dune anytime soon?" the answer is no

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:33):

Tho there has been a lot of work in the Dune team understanding other build systems, of course bazel, please.build, yarn and jest, pulp, spago, psc-package, and likely others upcomig

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:34):

So indeed Dune's weakest point is lack of programability, but this is a real problem

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:34):

but regarding to Coq, dune will offer some integration with the OCaml toolchain [such as composing with the compiler itself] that would be a huge amount of work

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:35):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:40):

One non-trivial problem with bazel is the dependency on the python toolchain, etc... so there is a lot of discussion to do here, build systems is the much improved emacs vs vim :)

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:40):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:41):

but I'm happy to see Bazel implement Coq build rules, but getting close to what dune can do for Coq devs will be a lot of work, so it will be useful for those willing to integrate into their existing bazel setup, which is not a small number of people

Gregg Reynolds (Apr 01 2021 at 15:01):

@Enrico Tassi Whether Coq ever decides to use OBazl is of course an open question for the Coq devs to decide, but in general OBazl will never supersede Dune. To be clear, it was never the intention to replace or even compete with Dune, which is a fine piece of software. I just happen to like Bazel. When I came across Mina I had trouble with the build, and could not (easily) see what Dune was doing. Since I already had some experience working with Bazel I decided to try to Bazelize Mina (and the Mina team generously provided a token grant to support the work). Of course if I had known then what I know now I never would have started, heheh. In any case, rules_obazl is now (mostly) done. I _think_ it covers just about everything needed so support OCaml (but won't be surprised if that's not quite the case). The major difference is probably just design philosophy. The Dune language is quite high level, so there's a certain amount of magic involved. OBazl is deliberately low-level and compositional, and tries to expose everything to the programmer. FWIW its possible in principle to use the Dune language with OBazl, all we need is a tool to convert dune files to BUILD.bazel files. I've got a primitive tool to do this, but its written in Clojure, and it doesn't get the dependencies 100% right, which is quite hard to do.

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:03):

Note that Dune has an internal low-level language and build engine which is 100% agnostic, it is just not exposed as it is not stable yet, but indeed you can access it .

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:03):

This is how coq rules are implemented, and for the amount of features they provide it is remarkably compact

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:05):

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:06):

I think the current engine is fairly powerful in terms of build graph dynamism, likely more than most existing build systems but I'm not so expert on the other systems as to know

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:07):

dune files are just evaluated to this monad [for building], plus a far from trivial amount of work setting up the context, library database, etc...

Gregg Reynolds (Apr 01 2021 at 15:15):

"Build graph dynamism' reminds me, a huge difference between Dune and OBazl is that the former (I believe) discovers and orders dependencies at build time. Bazel rules could analyze and order deps at build time, but all of them must be explicitly listed. The OBazl rules do no reordering, they just maintain the ordering induced by the dependency tree (under a postorder traversal).

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:20):

Yup, tho it is a bit more complex mix of static vs dynamic. Dune 3.0 will be way more dynamic so for example you can generate a dune file with a rule, and update the graph in that way; this is actually needed by many use cases due to staging / cross compilation / and other stuff.

Gregg Reynolds (Apr 01 2021 at 15:53):

It'll be fun to translate that to Bazel, which disallows dynamic deps since they compromise replicability.

Gregg Reynolds (Apr 01 2021 at 16:08):

@Emilio Jesús Gallego Arias Can you elaborate on "pass the corresponding g_* grammar files"? I have them all processed with coqpp, compiled as modules, and listed as deps for those modules that need them. Is there more to it?

Gregg Reynolds (Apr 01 2021 at 16:46):

What are the rules governing resolution of Declare ML Module statements in a .v file? For example, theories/Init/Prelude.v contains Declare ML Module "cc_plugin".. If I run coqdep without -I plugins/cc then I get a warning: !<>*** Warning: in file theories/Init/Prelude.v, declared ML module cc_plugin has not been found!. There are two places cc_plugin is used in plugins/cc: the filename cc_plugin.mlpack and in file g_congruence.mlg, which has DECLARE_PLUGIN "cc_plugin". So: 1) does coqdep look at mlpack filenames? 2) presumably the DECLARE is resolved when a corresponding DECLARE_PLUGIN is found, yes? 3) does coqdep only look in .mlg files to resolve such refs? 4) Is this kind of stuff documented somewhere?

Gaëtan Gilbert (Apr 01 2021 at 16:59):

The rules are
foo.mlg -> foo.ml
foo.ml -> foo.cmx
every foo.cmx listed in bar.mlpack -> bar.cmxs (cmo or byte compilation, cma for byte and mllib)

coqdep on Declare ML Module looks for mlpack (and mllib)
coqc/coqtop looks for cmxs (cmo and cma if byte compiled)

Gregg Reynolds (Apr 01 2021 at 17:00):

Gregg Reynolds (Apr 01 2021 at 17:03):

I understand Coq is going to move away from -pack to use of aliasing. In that case, what will happen to the mlpack files and coqdep resolution logic? Just replaced by mllib?

Gaëtan Gilbert (Apr 01 2021 at 17:11):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:50):

You need to link statically a few files, some in tactics and some in parsing vernac , usually the ones starting by g_

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:51):

There is a PR an issue named something like "remove -linkall from Coq" which is more precise about what is needed, actually indeed I think we manage to land ocamlfind support for plugins in 8.14, then we can stop using -linkall to build Coq

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

as we can have coq.plugins.ltac load the tactics that are not used by coqc dynamically then, see the issues / PR for more details

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

when I wrote the "no linkall" PR, I had to try manually until I found the right setup

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:53):

that's a lot of logic that dune already knows, which is quite a bit work to replicate

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:54):

but going back to the static linking, you need to link coqc_bin.cms which all the corresponding cmxa coming from the libs

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:54):

mlpack / mllib files are not necessary in dune as usually the default for (modules ...) is "all .ml files in the current directory", including the _generated_ ones

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:55):

Dune has a view of the filesystem including generated stuff so it can properly track them, and above all, implement cleanup for incremental builds, otherwise you get stale objects / files in the build tree

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:56):

this feature by the way was my original motivation two years ago to implement dune support, as make cannot track stale objects, git bisect is usually broken unless you do make clean or you are lucky that the set of object files is the same among two revisions

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:58):

having dynamic deps is pretty convenient when calling ocamldep, otherwise you get into trouble quickly if you are generating a .v file for example

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:59):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

for dune, if rules are deterministic and sound w.r.t. sandboxing, you get deterministic build despite the dynamic deps

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

but that's something not enforced indeed, you can write rules that are not deterministic

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

Gregg Reynolds (Apr 01 2021 at 18:49):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:54):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:57):

so you need to sure all the cma contain all the modules + pass all the cmas to the command line

Gregg Reynolds (Apr 01 2021 at 23:15):

Well, I managed to compile theories/Init/Notation.v under Bazel, hoorah - I hereby declare victory for the day; tomorrow I'll tackle the rest of the .v files.

Emilio Jesús Gallego Arias (Apr 02 2021 at 10:57):

@Gregg Reynolds very nice! Congrats, I know how it feels :) How do you handle coqdep in bazel then? I'd b very curious to hear speed for example to do common ops such as check all ml files.

Gregg Reynolds (Apr 02 2021 at 12:03):

All hand-rolled, I'm afraid. I run the tool at the command line and convert the results by hand into dep lists in my build rules. Tedious but easy.
Remember we cannot use a tool like coqdep to discover deps at build-time, we have to do that ahead of time, so that our rules list all deps explicitly. Once I figure this stuff out I can address tooling that would automate this.

Emilio Jesús Gallego Arias (Apr 02 2021 at 12:07):

I was wondering as indeed, in order to run coqdep you need to build it first, so you then need some kind of build staging right?

"check all ml files" is the most common operation I do in day-to-day development: I have a tree with Coq + some plugins / libs, and usually want to check that all ml files do compile correctly, fix errors otherwise. Dune provides this target which is optimized for speed [the whole tree is checked almost instantly in common cases]

Gregg Reynolds (Apr 02 2021 at 12:21):

Well, I have a build target for everything, so I just run bazel build tools:coqdep, and the output goes to bazel-bin/tools/coqdep.

So check all ml files just means "build all the ml files"? You don't really need to do that with Bazel, it caches everything and will always rebuild only what needs to be rebuilt for a given target (i.e. anything that has changed, plus anything that depends on what has changed). But you can use wildcards in target labels; for example to build every target in kernel I would run bazel build kernel:*. That will still only build what needs to be rebuilt, but it will do it for each target in the package. So to build everything: bazel build //...:*. That's sometimes helpful to catch broken build rules, but I rarely use it.

Enrico Tassi (Apr 02 2021 at 12:31):

I think Emilio is thinking about the @check target of dune which builds as fast as possible (eg not even using the optimized compiler) all .ml files. It is quite useful in git rebase to check each commit compiles, or to get all the .cmt* stuff the language-server uses to give intellisense completion in vscode for example

Gregg Reynolds (Apr 02 2021 at 12:36):

IOW, use the bytecode compiler along with whatever flags are needed for the fastest possible builds? The Obazl rules do not currently directly support that but it would be easy to add, probably as a build flag, e.g. bazel build //...:* --@ocaml//check or some such. Default compile mode is native; to build in bytecode mode: bazel build foo:bar --@ocaml//mode=bytecode.

Enrico Tassi (Apr 02 2021 at 12:41):

Emilio Jesús Gallego Arias (Apr 02 2021 at 14:01):

Emilio Jesús Gallego Arias (Apr 02 2021 at 14:02):

check indeed just mean "check my project compiles ok", you run it after changes of course, and it should be incremental of course, calling check twice should be a no-op.

Gregg Reynolds (Apr 02 2021 at 15:00):

Yes, you need to run coqdep(or otherwise discover deps) before you can build. That's a PITA the first time, but after that you do it only when the dep structure changes, which presumably is not often. The same is true of the OCaml deps, by the way. This is admittedly kind of a "broken as designed" feature, but it can be addressed with tooling in the future. For now, my experience has been that it's a relatively minor inconvenience.

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:04):

For some uses cases Coq devs have this is a bit of a limitation tho, one motivation to replace the make-based build system is that indeed it required some staging, that made things such as bisect not to work properly; nowadays we are working in a setup where even the OCaml compiler itself is part of the build tree so we can hack in Coq and ocamlc at the same time, so it is a pity if bazel has this problem, I was under the impression it could handle dynamic deps

Gregg Reynolds (Apr 02 2021 at 15:14):

I'm not sure dynamic deps are every truly necessary. It should always be possible to list all possible deps; if it isn't, there's a problem. Choosing which dep to use at build time is a different thing, and I think that's the general Bazelish way to go.

Gregg Reynolds (Apr 02 2021 at 15:19):

bazel-out/darwin-opt-exec-2B5CBBC6/bin/topbin/coqc -boot -noinit -coqlib . -q -R theories Coq -I bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl -o bazel-out/darwin-fastbuild/bin/theories/Init/Ltac.vo theories/Init/Ltac.v
...
File "./theories/Init/Ltac.v", line 11, characters 0-32:
Error: Dynlink error: interface mismatch on Vmvalues

I hate interface mismatches. Any suggestions here? Where should module Vmvalues be located? coqc? ltac_plugin? other?

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:38):

The error is due to stale files resulting from unsound build rules or some other problem

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:38):

Gregg Reynolds (Apr 02 2021 at 15:39):

FYI having the build tools (including compiler) in the dep tree is not only routine but recommended for (hermetic) Bazel builds. I have not exposed this yet in OBazl, but for example Bazel rules_go will download and build the Go compiler automatically.

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:39):

In many cases yes, they are, or an equivalent multi-stage build. Simple example, Coq extraction mechanism, or in general, any kind of file generation, which is very common in Coq workflows.

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:40):

Note that what I mean here is not only downloading the compiler, but actually hacking the Go compiler toghether with some libraries, then having a full incremental bulid.

Gregg Reynolds (Apr 02 2021 at 15:41):

Aren't those just dependency chains? For file generation, at least, there is no need for multiple stages, just a tree of dependencies.

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:41):

But if I generate a .v file, I need to run coqdep after generation to build its dep set, right?

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:42):

Gregg Reynolds (Apr 02 2021 at 15:42):

Yeah, you can do that (hack the compiler dependency and Coq simultaneously), it's actually pretty easy.

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:42):

So if my build rules in bazel generate a .ml file, I cannot compile it in the same build?

Emilio Jesús Gallego Arias (Apr 02 2021 at 15:43):

Gregg Reynolds (Apr 02 2021 at 15:53):

Sure you can. I've got to run now but for an example take a look at targets _G_proofs, _G_vernac, and gvernac in obazl/coq. You can find some ocaml_lex rules too, wherever there's a .mll file, it's the same pattern. genrule is basically a wrapper for a shell script; ocaml_lex is just a convenience rule that does that automatically. The critical bit is that Bazel rule deps form one depgraph, but each rule must register its file deps, which is a different depgraph, the latter is the one Bazel uses to decide what to build. So that's how Bazel knows the depgraph - the build rules must register all deps.

Gregg Reynolds (Apr 02 2021 at 15:56):

Also, let's distinguish between multi-stage and multi-pass. If A depends on B depends on C, then they will be built C, then B, then A, which is literally multistage but not multi-pass.

Gregg Reynolds (Apr 02 2021 at 19:08):

Huzzah! Got theories/Init/Ltac to build Ltac.vo! The problem was due to what I think may be a Bazel bug - I asked on the mailing list, we'll see. In any case, on to the rest .v files. Thanks for all the help!

Gregg Reynolds (Apr 02 2021 at 21:12):

An example of what seems to work to produce a .vo file (in theories/Init/BUILD.bazel):

coq_module(
    tool = "//topbin:coqc",
    name = "Specif",
    src  = "Specif.v",
    plugins = [
        "//plugins/ltac:ltac_plugin"
    ],
    deps = [  # targets that produce .vo files
        ":Datatypes",
        ":Notations",
        ":Ltac",
        ":Logic"
    ]
)

Gregg Reynolds (Apr 03 2021 at 01:27):

Everything in theories/Init now builds. That wasn't so bad. Maybe I can get the rest of the theories done over the weekend.

Gregg Reynolds (Apr 03 2021 at 22:43):

  bazel-out/darwin-fastbuild/bin/topbin/coqc -coqlib . -q -R bazel-out/darwin-fastbuild/bin/theories Coq -boot -noinit -I bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl -o bazel-out/darwin-fastbuild/bin/theories/Bool/Bool.vo theories/Bool/Bool.v

File "./theories/Bool/Bool.v", line 19, characters 0-4:
Error: Syntax error: illegal begin of vernac.

Gregg Reynolds (Apr 04 2021 at 00:13):

Gregg Reynolds (Apr 04 2021 at 00:34):

Now a question: I see that some .v files need Coq.Init.Prelude and some don't. Is there any way I can tell coqdep to print such deps? I tried adding -boot but it did not seem to make much difference.

Emilio Jesús Gallego Arias (Apr 04 2021 at 00:47):

files in theory/Init/ do indeed need -boot -noinit, the rest should be compiled as normal.

Emilio Jesús Gallego Arias (Apr 04 2021 at 00:47):

Note that coqdep won't also emit the dependency for Init/Prelude.vo so you need to adjust that manually.

Emilio Jesús Gallego Arias (Apr 04 2021 at 00:49):

So for bool you can just use coqc -coqlib $build_dir Bool/Bool.v , but keep in mind that the dependency to prelude is implicit.

Gregg Reynolds (Apr 04 2021 at 02:13):

File "./theories/setoid_ring/Ring_tac.v", line 388, characters 41-43:
Error: Syntax error: ')' expected after [ltac_expr] (in [ltac_expr]).

Gregg Reynolds (Apr 04 2021 at 02:33):

Warning: Cannot determine user home directory, using '.' .
Error: Cannot find plugins directory

maybe because the effective plugins directory is bazel-out/darwin-fastbuild/bin/plugins. How can I tell it that?

Emilio Jesús Gallego Arias (Apr 04 2021 at 12:58):

That error seems like you forgot to statically link some part of a plugin or coqc?

Gregg Reynolds (Apr 04 2021 at 12:59):

I wondered about the links. I checked the mlg files, they look ok to me, but something must be off.

File "./theories/Program/Wf.v", line 75, characters 0-10:
Error: Syntax error: illegal begin of vernac.

Gregg Reynolds (Apr 04 2021 at 13:00):

In general, I seem to be able to compile any of the .v files under theories, with the above exceptions. Most of them anyway, I'm working through them one-by-one.

Gregg Reynolds (Apr 04 2021 at 13:06):

Ring_tac is the blocker, lots of things depend on it. Just rebuilt with -linkall everywhere, same result. Any particular I should be looking for, given the error involves ltac_expr?

Gregg Reynolds (Apr 04 2021 at 13:07):

The odd thing is that I have come across the exact same error message with other .v files, and adding -ri Coq.Init.Prelude fixed the problem in those cases.

Gregg Reynolds (Apr 04 2021 at 13:11):

Aha! I spoke too soon - my ring_plugin was missing a dep on g_ring.mlg - problem solved. Sorry about the noise, I should have seen that a long time ago.

Gregg Reynolds (Apr 04 2021 at 15:40):

Ok, I can now produce .vo files for all the .v files under theories. But coqtop seems to want .vos files. Then there are .vio and .vok files. What do I need to produce, when? Should I be producing .vos instead of .vo?

Emilio Jesús Gallego Arias (Apr 04 2021 at 16:10):

Gregg Reynolds (Apr 04 2021 at 21:05):

The short answer is that I need to spend a little more time figuring out how to match the expectations of the coq tools wrt filesystem layout etc. with the way Bazel does things. The error I was getting was

$ ./bazel-bin/topbin/coqtop.opt -coqlib .
Welcome to Coq 8.14+alpha
Error: Unable to locate library
Prelude with prefix Coq. (While searching for a .vos file.)

$ ./bazel-bin/topbin/coqtop.opt -coqlib bazel-out/darwin-fastbuild/bin -I bazel-out/darwin-fastbuild/bin
Warning: Cannot open bazel-out/darwin-fastbuild/bin/theories
[cannot-open-path,filesystem]
Welcome to Coq 8.14+alpha
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix Coq.

Which means I have to do a little more work getting the deps/outputs structures right for Bazel and figuring out the right cmd switches. I don't think this should be terribly difficult, might take a day or two of experimenting. Which means... see you in two months!!! hahah.

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:34):

Oh, I think the .vos missing message is confusing and a bug [it will search for the vo, then the vos, both fail, you see the later]

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:34):

The code for locating things is a mess, fortunately we are very close to doing a big rework

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:35):

-coqlib dir needs to point to a directory where theories is present, and in particular theories/Init/Prelude.vo

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:35):

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:37):

So as of today you have two packages, coq-core, which is the OCaml stuff, that you have to build a filesystem layout that makes OCaml tooling happy, the build of Coq in that regards is very standard in the sense that we declare libs in dune that is.

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:37):

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:38):

when not using -boot, moreover it will also expect plugins in lib/coq-core/plugins

Emilio Jesús Gallego Arias (Apr 04 2021 at 23:38):

we are working in replacing that part with OCaml find so you could install a meta and be done, however that is gonna take a bit more time as this setup doesn't work for building coq yet [as the meta is not yet in place]

Gregg Reynolds (Apr 05 2021 at 00:51):

Now my build output contains the built stuff in directories corresponding to the source layout, rooted at bazel-out/darwin-fastbuild/bin; in particular I have bazel-out/darwin-fastbuild/bin/theories and bazel-out/darwin-fastbuild/bin/plugins. Are you saying I need to move those to bazel-out/darwin-fastbuild/bin/lib/coq/theories and bazel-out/darwin-fastbuild/bin/lib/coq-core/plugins, respectively?

$ ./bazel-bin/topbin/coqtop.opt -q -coqlib bazel-out/darwin-fastbuild/bin
Welcome to Coq 8.14+alpha
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"dlopen(/private/var/tmp/_bazel_gar/8c949035aafa6229d33cef095568e3f8/execroot/coq/bazel-out/darwin-fastbuild/bin/plugins/ltac/ltac_plugin.cmxs, 10): Symbol not found: _camlAutorewrite\\n  Referenced from: /private/var/tmp/_bazel_gar/8c949035aafa6229d33cef095568e3f8/execroot/coq/bazel-out/darwin-fastbuild/bin/plugins/ltac/ltac_plugin.cmxs\\n  Expected in: flat namespace\\n in /private/var/tmp/_bazel_gar/8c949035aafa6229d33cef095568e3f8/execroot/coq/bazel-out/darwin-fastbuild/bin/plugins/ltac/ltac_plugin.cmxs\")")

I built with -linkall everywhere. Autorewrite is in tactics. Is it supposed to be linked into ltac_plugin.cmxs? Seems like it should be found in tactics/Autorewrite.cmx at load time.

Gregg Reynolds (Apr 05 2021 at 01:00):

Autorewrite is a dep of two modules in ltac_plugin: Extratactics and Rewrite. When I look that the cmx files for those, I see that the interface for Autorewrite is imported, with a line like 865c1a07bba2e2e2932066229ea6608a Autorewrite. But in the Implementations imported section, I have -------------------------------- Autorewrite. Does that make sense? I've tried everything I can think of to get a number instead of ----------... in the implementations section, with no luck. Which puzzles me, since I see that deps are listed with numbers in the implementation section for lots of modules in OPAM.

Gregg Reynolds (Apr 05 2021 at 01:42):

Welcome to Coq 8.14+alpha
No level labelled "0" in entry "term"
Error:
                                      Dynlink error: execution of module initializers in the shared library failed: Failure("Grammar.extend")

Any idea what that means? AFAIK my gramlib target builds an archive that matches gramlib/gramlib.mllib.

Gregg Reynolds (Apr 05 2021 at 01:46):

BTW, I hate to hijack a Coq forum for bazel stuff. Feel free to respond on the obazl discord server if you think it more appropriate.

Gregg Reynolds (Apr 05 2021 at 04:11):

$ ./bazel-bin/topbin/coqtop.opt -noinit -coqlib bazel-out/darwin-fastbuild/bin -R bazel-out/darwin-fastbuild/bin/theories/ Coq
Welcome to Coq 8.14+alpha

Coq <

Coq < Check nat.
Toplevel input, characters 7-10:
> Check nat.
>       ^^^
Error: The reference nat was not found in the current environment.

Jasper Hugunin (Apr 05 2021 at 04:31):

Well, that's because of the -noinit flag, which tells Coq to not automatically load the prelude, so you get a completely blank slate (nat is defined in theories/Init/Datatypes.v). Take away -no-init and it might complain about not being able to find the prelude, but that's a different problem.

Jasper Hugunin (Apr 05 2021 at 04:34):

If you do Require Import Prelude. in that coqtop, and it succeeds, then Check nat. should work.

Gregg Reynolds (Apr 05 2021 at 11:04):

Emilio Jesús Gallego Arias (Apr 05 2021 at 15:58):

We have an ongoing PR which will make this more flexible, but as of today the second rules are hardcoded among different tools.

Gregg Reynolds (Apr 05 2021 at 16:08):

Thanks, by trial and error I've rediscovered the first option, which works for bazel too.

Question: is it always the case that all .v files ("sublibraries"?) depend on Coq.Init.Prelude? Except for those in Prelude, I mean. IOW, is it safe to hardcode that dependency in my build rule for such files? Currently I pass it as a parameter, but they all seem to need it.

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:09):

Yes, it is safe to assume that all regular libraries do depend on Init.Prelude, except for a few special ones such as HoTT that use -noinit

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:09):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:10):

As of today the -noinit flag for Init/*.v is hardcoded, but we will make it a parameter

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:10):

Gregg Reynolds (Apr 05 2021 at 16:13):

Great, then it sounds like I'm on the right track. I have a build rule for each .v file; for Init/*v, I pass -noinit, and in the rule I've hardcoded -boot -R dir Coq and some -I stuff.

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:14):

Dune has a special case for this dependency, which is "if Coq's stdlib is in the workspace, then add the dependency"

Gregg Reynolds (Apr 05 2021 at 16:14):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:14):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:15):

This is required as indeed in Dune it is common to blend several libraries together in a build workspace

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:15):

so we need first to build the DB of libraries in scope, and if we find the stdlib, then the implicit dependency should be added

Gregg Reynolds (Apr 05 2021 at 16:17):

I've got a param that looks like with_libs = {"//theories/Init:Prelude": "Coq.Init.Prelude"}, which should generalize to other filesystem-path, module-path pairs.

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:17):

Gregg Reynolds (Apr 05 2021 at 16:19):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:19):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:20):

so what we call "a boot theory" in Dune, is something that includes Coq.Init.Prelude

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:20):

Gregg Reynolds (Apr 05 2021 at 16:21):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:21):

This will be made a bit more generic in the future, for now it is hardcoded, and if you want to bypass it you need to use -no-init

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:21):

there is the HoTT library which doesn't use the stdlib, so indeed it uses always -no-init

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:21):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:22):

in the past it used to be the case that the stdlib was coupled to Coq, but we did some work to decouple it and now libraries can register with Coq properly (almost)

Gregg Reynolds (Apr 05 2021 at 16:24):

Cool, thanks. For now I'm going to be satisfied with a minimal Proof-of-Concept implementation for the standard Coq source tree, and worry about more general stuff later. LIke when I convince somebody to fund a feature-complete Bazel lib, hahaha.

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:28):

Hehehe. But indeed be sure to document the special case for prelude clearly, as indeed this is a problem users will find often

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:29):

The concrete problem is "when building my regular Coq library, and Coq is installed, things work fine"

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:29):

"however if I build it together with Coq, the dependency on the prelude has to be added by the build system"

Gregg Reynolds (Apr 05 2021 at 16:46):

Emilio Jesús Gallego Arias (Apr 05 2021 at 16:58):

Gregg Reynolds (Apr 05 2021 at 17:41):

$ time dune build theories/Reals/Reals.vo
Done: 4639/4640 (jobs: 1)
real    3m43.803s
user    5m9.451s
sys 3m25.399s

$ time bazel build theories/Reals:Reals
...
INFO: Elapsed time: 255.515s, Critical Path: 217.83s
INFO: 1775 processes: 152 internal, 1623 darwin-sandbox.
INFO: Build completed successfully, 1775 total actions

real    4m15.576s
user    0m0.064s
sys 0m0.062s

They probably don't have quite the same dep graphs. I haven't done any optimization.

Emilio Jesús Gallego Arias (Apr 05 2021 at 17:43):

Emilio Jesús Gallego Arias (Apr 05 2021 at 17:44):

dune build is still missing one optimization that will impact 10-20 sec on most systems, after that the build should be "optimal" modulo the dune overhead itself

Enrico Tassi (Apr 05 2021 at 17:45):

Looks like bazel uses a daemon which is not counted in that stats (0 user time, 0 sys time...). Is it the case? BTW, the sys time of dune is quite fishy as well

Emilio Jesús Gallego Arias (Apr 05 2021 at 17:47):

Yeah sys time seems high, but could be due to many factors including memory pressure or different filesystems [or even the cache]

Emilio Jesús Gallego Arias (Apr 05 2021 at 17:48):

Build systems do a lot of copy / read / write around and that takes a lot of sys time, usual figures in my setup:

$ time dune build theories/Lists/List.vo

real    0m52,879s
user    2m33,525s
sys 0m40,373s

Gregg Reynolds (Apr 05 2021 at 17:49):

I tried doing the fastbuild, but I discombobulated bytecode builds somehow so that'll have to wait.

Dunno if I'll be able to match Dune's speed. The Bazel engine itself I would expect to be pretty efficient, but the OBazl rules I wrote are another matter, there's probably plenty of room for optimization there. Then of course there's the remote compilation and remote caching which could be very helpful in some situations, although I have not tried either.

Gregg Reynolds (Apr 05 2021 at 17:51):

Yes, it runs a daemon. It's Java, so initial startup is a little slow, but then in stays in memory for some (configurable) period, so I never notice it.

Emilio Jesús Gallego Arias (Apr 05 2021 at 17:51):

Rules on the dune side are not too complex, you start to see the benefits for the more refined setup in incremental dev builds, but here we are building from scratch so there are no savings due to incremental. A likely source of difference is that dune uses ocamldep -modules which allows for a bit better parallelism (+ other features)

Gregg Reynolds (Apr 05 2021 at 17:53):

I also did not show timing for real from scratch (after bazel clean -expunge) which involves downloading, building, and configure the tooling; in this case that means configuring Xtools. All of which can take 20-30 seconds some times. A bazel clean leaves that stuff in place.

Gregg Reynolds (Apr 05 2021 at 17:55):

Yeah, I saw in the Coq docs also that the .vo, .vos, .vok stuff involves parallelization and optimisations. But that will have to wait until The Funder decides it's important enough to pay for, heh.

Gregg Reynolds (Apr 05 2021 at 17:57):

I would expect Bazel (i.e. the obazl rules) to be a little faster in that respect, since it does not run ocamldep or any other dep analysis tool at all. Bazel does parallelize aggressively, too. They also have some kind of profiler, which I have not used. Might take a look at it once I get rules_coq in a little better shape.

Gregg Reynolds (Apr 05 2021 at 18:07):

Of course the major difference is that under OBazl we have one build rule per source file, plus rules for aggregates like archives and executables. I think that's bound to have a performance impact at least for the analysis phase, but it's a price I'm willing to pay in return for simplicity, clarity, etc.

Emilio Jesús Gallego Arias (Apr 05 2021 at 18:45):

that part I don't follow, if I edit a ml file surely bazel has to run ocamldep as to get updated deps

Gregg Reynolds (Apr 05 2021 at 19:03):

Gregg Reynolds (Apr 05 2021 at 19:05):

Emilio Jesús Gallego Arias (Apr 05 2021 at 19:16):

So if I edit foo.ml to add open Bar , I need to manually update the bazel file? That seems weird, I'm not sure we are talking about the same thing.

Gregg Reynolds (Apr 05 2021 at 20:26):

Yep, sadly that's the way it works, for now at least. But you have to do that with Dune too, no?

Gregg Reynolds (Apr 05 2021 at 20:29):

That is, if Bar is not already in the transitive closure of the depgraph for foo.ml. If it is, then you don't need to add it, it's already there, even if it is not listed as a direct dep of foo.ml. All deps in OBazl are "sticky" (transitive).

Gregg Reynolds (Apr 05 2021 at 20:49):

One upside of this (IMO) is that you can "normalize" the deps to the minimum required. E.g. if a.ml depends on B and C, and B depends on C, you only have to list B as a dependency of A. A query for the deps will then show only what's required. There is no primitive way to make a set ("library") of modules depend on a list of deps; to do that you have to use a variable and list it for each depending module.

Paolo Giarrusso (Apr 05 2021 at 21:42):

At least for Coq you don't, thanks to coqdep; I'd expect ocamldep to do the same (but I'll let Emilio confirm). Autogenerating these dependencies correctly is not trivial. (This might be unique to built-in rules for now, pending https://github.com/ocaml/dune/issues/4089, but that includes rules for OCaml and Coq already).

Gregg Reynolds (Apr 05 2021 at 21:47):

You can say that again. The first version of obazl_rules_ocaml tried to discover and analyze deps, sorta like Dune does it. After a few agonizing weeks (or was it months, that kind of trauma can mess with your memory) I decided that was a form of premature optimization to be avoided in favor of the simplest and clearest solution to start with.

Emilio Jesús Gallego Arias (Apr 05 2021 at 21:49):

Nope, Dune will discover the deps dynamically, otherwise for such a large system like Coq + CI in a composed build, specifying deps manually would be just be unworkable.

I see, unfortunately deps change very often so the build definition rule will be pretty hard to maintain unless generated automatically. It is even more surprising that Bazel is slower then, as coqdep/ocamldep add non trivial overhead to the Dune build .

Emilio Jesús Gallego Arias (Apr 05 2021 at 21:52):

Yup, unfortunately the full rules API which supports a lot of cool stuff in master is only available from OCaml, but there is a lot of discussion on how to expose it for rules writers and for sure Dune 3.0 will support something such as %{read*: }

Emilio Jesús Gallego Arias (Apr 05 2021 at 21:52):

Not sure if that has been even already added to master, as the only thing missing is the syntax

Gregg Reynolds (Apr 05 2021 at 21:53):

Good, then I will have a nice design challenge once the minimal Bazel rules stablize! (I knew this might be an issue at least for some folks, but decided to pretend not - can't solve everything at once, heh.)

Emilio Jesús Gallego Arias (Apr 05 2021 at 21:54):

By the way, one of the keys reasons we did write the dune support for Coq in OCaml was because we needed this to have a nice workflow with coqdep, pity we couldn't write it directly in the rules lang.

Emilio Jesús Gallego Arias (Apr 05 2021 at 21:55):

First version of dune for Coq actually generated a static build rule file similar to the one in bazel , at the cost of having to do two passes. You can check the script in the coq tree under tools coq_dune [use git to recover a commit with it]

Gregg Reynolds (Apr 05 2021 at 21:56):

I'll have to seriously revisit the whole coqdep thing later. Who knows, maybe there's a way to accomodate it in Bazel that I don't know about. I know the rules for Go use tooling that does stuff outside of Bazel's control in some way, maybe that's possible here.

Emilio Jesús Gallego Arias (Apr 05 2021 at 21:59):

I've been reading a bit and it seems that indeed there is no easy way short of generating BUILD files.

If that is the case I have to say that then Bazel is just not the right tool for the job in the case of Coq + OCaml , dynamic deps are almost essential in our context IMVHO.

Gregg Reynolds (Apr 05 2021 at 22:03):

Oh dear, I wish you hadn't said that, now I'll probably spend the next six months obsessively trying to figure out a way to make it work, just to show that it's possible.

Emilio Jesús Gallego Arias (Apr 05 2021 at 22:04):

Emilio Jesús Gallego Arias (Apr 05 2021 at 22:10):

@Gregg Reynolds well if Bazel doesn't support dynamic deps, I'm positive you will have a very hard time to have things work in the context of Coq + Projects, just extraction will give you big headaches; keep in mind that I am talking about a repository size with several million lines of code, so manual update of deps is just out of the question. Do you know the build system chart in "Build Systems à la Carte" ?

IMHO not every build system is a good fit for every context [even make is one of the poorest choice for OCaml / Coq] and now that I'm being bold in what my thoughts are I think using make for Coq is just a loss of time for everyone. The previous build maintainer in Coq was well aware of this, unfortunately there was no good alternative until Dune appeared.

In fact Coq requires something way more advanced that most build systems can do today and is integration with the compiler / AST; in the case of Coq this requires and incremental computation model extremely dynamic as even parsing is in the dep chain, as opposed to common incremental updates today for example with VDom model.

Emilio Jesús Gallego Arias (Apr 05 2021 at 22:12):

Gregg Reynolds (Apr 05 2021 at 22:13):

Emilio Jesús Gallego Arias (Apr 05 2021 at 22:14):

[by the way this thread is 100% ontopic in this forum, and indeed I'd love to see Bazel + Coq support progress more, but it is unfortunate the limitation regarding the computation model, otherwise I think it would have potential]

Emilio Jesús Gallego Arias (Apr 05 2021 at 22:16):

   (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \
          `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \
          `find theories user-contrib -type f -name *.v`"))))

Emilio Jesús Gallego Arias (Apr 05 2021 at 22:17):

The coq_dune reads the file generated by the above coqdep call, builds the dep map, and dumps it in several dune files

Emilio Jesús Gallego Arias (Apr 05 2021 at 22:17):

Gregg Reynolds (Apr 05 2021 at 23:19):

Oops, forgot to mention I wrote a little clojure program yesterday to parse the output of coqdep and generate BUILD.bazel files for everything in theories. I didn't use all the params in your script (e.g.-dyndep , -noglob) but it seemed to work.

Gregg Reynolds (Apr 06 2021 at 17:19):

@Emilio Jesús Gallego Arias Actually there is a very simple solution to this problem, I don't know why I did not think of it months ago. All we need is fswatch or some similar filesystem watcher. I just finished a Proof-of-Concept implementation - I added Require Export Bool. to theories/Arith/Arith.v and presto-chango, the new dep was added to theories/Arith/BUILD.bazel, almost instantly.

Gregg Reynolds (Apr 06 2021 at 17:23):

The larger point being that dependency munging and building are separate and distinct concerns. Nothing says the same code/process must handle them both; in fact no matter how you slice it, you must handle the deps before you can build. OBazl just explicitly cuts the dependency munging stuff out of the build logic, so it must be handled in some manner before the build launches.

Emilio Jesús Gallego Arias (Apr 06 2021 at 18:14):

First problem tho are generated files, in this scenario you have a non-trivial scenario, dynamic deps do provide a nice model for that.

Gregg Reynolds (Apr 06 2021 at 19:10):

Emilio Jesús Gallego Arias (Apr 06 2021 at 19:39):

I don't know how to do bazel rules, but for example consider extraction, I may want to generate some .ml files from .v files, then these .ml files are used to generate some Coq 's .v which we compile

Emilio Jesús Gallego Arias (Apr 06 2021 at 19:39):

Gregg Reynolds (Apr 06 2021 at 19:43):

Gregg Reynolds (Apr 06 2021 at 19:46):

Emilio Jesús Gallego Arias (Apr 06 2021 at 19:47):

The rest is typical workflow used in the verification of large scale software, I think if you ask in the Coq users about it people should be able to point out different workflows

Emilio Jesús Gallego Arias (Apr 06 2021 at 19:47):

Emilio Jesús Gallego Arias (Apr 06 2021 at 19:49):

Tho my point is that the sentence "The larger point being that dependency munging and building are separate and distinct concerns." it is actually far from accurate in many contexts. c.f. Build Systems à la Carte for example

Stream: Coq devs & plugin devs

Topic: coqc usage

Gregg Reynolds (Apr 01 2021 at 03:18):

Guillaume Melquiond (Apr 01 2021 at 06:46):

Guillaume Melquiond (Apr 01 2021 at 06:51):

Emilio Jesús Gallego Arias (Apr 01 2021 at 09:08):

Emilio Jesús Gallego Arias (Apr 01 2021 at 09:09):

Gregg Reynolds (Apr 01 2021 at 11:43):

Gregg Reynolds (Apr 01 2021 at 11:47):

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:43):

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:43):

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:44):

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:45):

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:45):

Emilio Jesús Gallego Arias (Apr 01 2021 at 12:46):

Gregg Reynolds (Apr 01 2021 at 12:58):

Emilio Jesús Gallego Arias (Apr 01 2021 at 13:08):

Enrico Tassi (Apr 01 2021 at 13:15):

Théo Zimmermann (Apr 01 2021 at 13:24):

Gregg Reynolds (Apr 01 2021 at 13:25):

Gregg Reynolds (Apr 01 2021 at 13:41):

Emilio Jesús Gallego Arias (Apr 01 2021 at 13:41):

Gregg Reynolds (Apr 01 2021 at 13:47):

Enrico Tassi (Apr 01 2021 at 14:12):

Théo Zimmermann (Apr 01 2021 at 14:26):

Enrico Tassi (Apr 01 2021 at 14:29):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:30):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:33):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:34):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:34):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:35):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:40):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:40):

Emilio Jesús Gallego Arias (Apr 01 2021 at 14:41):

Gregg Reynolds (Apr 01 2021 at 15:01):

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:03):

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:03):

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:05):

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:06):

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:07):

Gregg Reynolds (Apr 01 2021 at 15:15):

Emilio Jesús Gallego Arias (Apr 01 2021 at 15:20):

Gregg Reynolds (Apr 01 2021 at 15:53):

Gregg Reynolds (Apr 01 2021 at 16:08):

Gregg Reynolds (Apr 01 2021 at 16:46):

Gaëtan Gilbert (Apr 01 2021 at 16:59):

Gregg Reynolds (Apr 01 2021 at 17:00):

Gregg Reynolds (Apr 01 2021 at 17:03):

Gaëtan Gilbert (Apr 01 2021 at 17:11):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:50):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:50):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:51):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:53):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:54):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:54):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:55):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:56):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:58):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:59):

Emilio Jesús Gallego Arias (Apr 01 2021 at 17:59):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

Gregg Reynolds (Apr 01 2021 at 18:49):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:54):

Emilio Jesús Gallego Arias (Apr 01 2021 at 18:57):

Gregg Reynolds (Apr 01 2021 at 23:15):

Emilio Jesús Gallego Arias (Apr 02 2021 at 10:57):

Gregg Reynolds (Apr 02 2021 at 12:03):

Emilio Jesús Gallego Arias (Apr 02 2021 at 12:07):

Gregg Reynolds (Apr 02 2021 at 12:21):

Enrico Tassi (Apr 02 2021 at 12:31):

Gregg Reynolds (Apr 02 2021 at 12:36):

Enrico Tassi (Apr 02 2021 at 12:41):

Emilio Jesús Gallego Arias (Apr 02 2021 at 14:01):