Stream: Coq devs & plugin devs

Topic: coqc usage


view this post on Zulip Gregg Reynolds (Apr 01 2021 at 03:18):

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]

Is that normal? The last bit is:

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

What should my command look like? Is there a detailed guide to coqc somewhere?

view this post on Zulip Guillaume Melquiond (Apr 01 2021 at 06:46):

Your -R . Coq part looks wrong, it should be -R theories Coq.

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

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

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

view this post on Zulip Gregg Reynolds (Apr 01 2021 at 11:43):

Same result:

 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.

(...omitted... meaning I added -I for each plugin subdir)

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 12:43):

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

The cmxs files [or cma if in bytecode mode]

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 12:46):

Building ocaml is pretty challenging as you can see :)

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 13:08):

Yup, plugins have to be cmxs files [for the native case]

How does bazel handle composition of Coq theories?

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.

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

view this post on Zulip Théo Zimmermann (Apr 01 2021 at 13:24):

@Enrico Tassi See the answer to my similar question here: https://coq.discourse.group/t/building-coq-with-bazel-need-help-with-plugins/1257/4

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

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

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

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

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

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

view this post on Zulip Enrico Tassi (Apr 01 2021 at 14:29):

Sorry Théo, but this is not really my question.

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 14:35):

I think a bazel + dune integration is much more likely for now

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 14:40):

editor wars pale in comparison to this :)

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 15:05):

Here it is for those intersted [note it is in heavy development these days for Dune 3.0] https://github.com/ocaml/dune/blob/main/src/dune_engine/action_builder.mli

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

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

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

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Apr 01 2021 at 16:59):

coqdep looks at mlpack
the build system doesn't care about DECLARE_PLUGIN

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)

view this post on Zulip Gregg Reynolds (Apr 01 2021 at 17:00):

Very interesting, thanks.

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

view this post on Zulip Gaëtan Gilbert (Apr 01 2021 at 17:11):

dune already doesn't use -pack
We may end up with just empty mlpacks

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 17:50):

Indeed they are empty for now in the make-free build

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

but using ocamlfind solves this problem as it can keep track of the deps

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 17:52):

between plugins

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 17:59):

as you gotta stage your build

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 17:59):

i was under the impression that bazel would allow that

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

but that's a bug as rules have to be "functional"

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 18:00):

in the sense of "same input" , "same output"

view this post on Zulip Gregg Reynolds (Apr 01 2021 at 18:49):

"You need to link statically a few files," - meaning, use -linkall?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 01 2021 at 18:54):

Use linkall + the set of cma containing all the modules in the codebase

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

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

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

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

What is check all ml files?

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

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

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

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

view this post on Zulip Enrico Tassi (Apr 02 2021 at 12:41):

IOW, use the bytecode compiler along with whatever flags are needed for the fastest possible builds?

yes

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2021 at 14:01):

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 you need to run this target manually before you can compile .vo files?

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2021 at 15:38):

You didn't compile coq and the plugin with the same set of common deps

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2021 at 15:39):

I'm not sure dynamic deps are every truly necessary.

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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2021 at 15:40):

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.

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.

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2021 at 15:42):

In general I don't know the deps until generation.

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 02 2021 at 15:43):

How does Bazel compute the set of deps for that .ml file before building it?

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

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

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

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

I dunno if coq_module is the right name, but it'll do for now.

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

view this post on Zulip Gregg Reynolds (Apr 03 2021 at 22:43):

coqdep reports that Bool.v has no deps. But when I run

  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

I get:

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

What am I missing?

view this post on Zulip Gregg Reynolds (Apr 04 2021 at 00:13):

Never mind. I needed to add -ri Coq.Init.Prelude

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

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

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

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

view this post on Zulip Gregg Reynolds (Apr 04 2021 at 02:13):

Anything special about theories/setoid_ring/Ring_tac.v? I'm getting

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

even with -ri Coq.Init.Prelude and plugins/ltac:ltac_plugin.

view this post on Zulip Gregg Reynolds (Apr 04 2021 at 02:33):

If I omit -boot -noinit then I get

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?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 12:58):

plugins dirs should be passed with -I

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

view this post on Zulip Gregg Reynolds (Apr 04 2021 at 12:59):

Yep, I do pass the plugin dirs with -I

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

I also get:

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 16:10):

Actually coqc should already produce the vos files, tho they should be optional

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 16:10):

what is the concrete error

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

But that's because the build outputs are in Bazel dirs:

$ ./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.

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 23:35):

that's only used when not -boot

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 23:37):

Then for coq-stdlib

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 23:37):

you need to install it in lib/coq/theories

view this post on Zulip Emilio Jesús Gallego Arias (Apr 04 2021 at 23:37):

that's hardcoded

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

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

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

In any case, as-is it finds my plugins in the plugins/ dir, but:

$ ./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.

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 01:42):

Progress, sorta. Found some problems in my dep structure. Now I get

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.

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 04:11):

Yay!

$ ./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 <

'Course it doesn't entirely work:

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

I declare victory anyway, for the weekend, at least.

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

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 11:04):

Thanks! That worked!

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 15:58):

Regarding layout indeed there are two options for now:

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:09):

In Dune we allow to declare that using a flag.

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:10):

Yeah bootstrapping needs some special setup as you can see

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:14):

Yup, for the rest of files you need to add Init/Prelude.vo as dependency

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 16:14):

I'll add that as the rule default, with some kind of override option.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:14):

if it is not, then don't add, as it means Prelude is installed globally

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:17):

See https://github.com/ocaml/dune/blob/main/src/dune_rules/coq_rules.ml#L319 and https://github.com/ocaml/dune/blob/main/src/dune_rules/coq_rules.ml#L52

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 16:19):

Thanks. Question: stdlib - this is everything in theories except Init?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:19):

It includes Init

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:19):

it is everything under Coq.*

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:19):

it could be further split, in Dune we have this notion of "theory"

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:20):

so that Coq.Init.* is compiled with -no-init

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:20):

and the rest is compiled normally, but of course depends on init.prelude

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 16:21):

And Coq.* standardly maps to fs dir theories?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:21):

yes

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:21):

but that's the only case for now, stdlib2 will work the same way

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

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

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

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

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 16:46):

will do, thanks for the warning.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 16:58):

You got some timings of bazel vs dune for example?

For dune, you can try:

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 17:43):

Interesting, thanks for the data!

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

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

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

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

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 17:51):

Enrico Tassi said:

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

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.

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

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

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 17:57):

Emilio Jesús Gallego Arias said:

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)

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.

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 18:45):

since it does not run ocamldep or any other dep analysis tool at all

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 19:03):

If you add/remove a dep, you must edit the BUILD.bazel file accordingly.

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 19:05):

Of course this could be automated in the future.

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

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

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

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

view this post on Zulip Paolo Giarrusso (Apr 05 2021 at 21:42):

Gregg Reynolds said:

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

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

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 21:47):

Paolo Giarrusso said:

Gregg Reynolds said:

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

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

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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 21:49):

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

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.

The first version of obazl_rules_ocaml tried to discover and analyze deps

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 .

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 21:52):

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

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*: }

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 21:55):

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

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]

You could use that one, it is actually trivial.

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 22:04):

:joy: :joy: :innocent: :innocent:

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 22:12):

Of course let us know if we can be of help, for a start you can generate the deps for the stdlib using this script as I mentioned before: https://github.com/coq/coq/blob/a99776e10e0b2198d2b811ad82631111fb450f8a/tools/coq_dune.ml

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 22:12):

That should help you a lot IMVHO.

view this post on Zulip Gregg Reynolds (Apr 05 2021 at 22:13):

Thanks!

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 22:16):

This is the call to generate the file which is an input for coq_dune:

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 22:17):

So all you need to do is to change the output format to be a single BUILD file

view this post on Zulip Emilio Jesús Gallego Arias (Apr 05 2021 at 22:17):

that should be not too hard

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

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

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

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

view this post on Zulip Gregg Reynolds (Apr 06 2021 at 19:10):

Can you point me to some code that demonstrates the problem you see?

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2021 at 19:39):

This is pretty common workflow on some users

view this post on Zulip Gregg Reynolds (Apr 06 2021 at 19:43):

Thanks. I don't suppose you know of a basic tutorial for that?

view this post on Zulip Gregg Reynolds (Apr 06 2021 at 19:46):

Never mind, I see Software Foundations covers it.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2021 at 19:47):

Of extraction? It is documented in the Coq manual https://coq.inria.fr/distrib/current/refman/addendum/extraction.html

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2021 at 19:47):

I have a project that is doing something like that today, for example.

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2021 at 19:50):

And actually in a Coq document, there are not separate at all

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2021 at 19:50):

the graph changes a lot dynamically and interactions are complex

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2021 at 19:50):

when editing a document I mean


Last updated: Oct 16 2021 at 02:03 UTC