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?
Your -R . Coq
part looks wrong, it should be -R theories Coq
.
Also, possibly, when building the .v
files from the Init
directory, you might want to pass the -boot
option.
Indeed if you pass -R dir Coq
, you want to use -boot
so Coq doesn't add that path automatically
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
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?
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.)
You didn't link coqc
correctly it seems, you must use -linkall
and pass the corresponding g_* grammar files
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]
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
In the sense that if foo.v
Require bar.
, then coqdep will emit a dependency on bar.vo
however the dependencies of bar.vo
must also be in scope as Coq does "dynamic loading" of .vo files
Building ocaml is pretty challenging as you can see :)
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
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.
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?
@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
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.
@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.
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
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.
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)
AFAICT, the investment of the OCaml community is on Dune. Given that, there's no reason for a general shift to Bazel.
Sorry Théo, but this is not really my question.
If the question is "is obazl going to superseed dune anytime soon?" the answer is no
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
So indeed Dune's weakest point is lack of programability, but this is a real problem
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
I think a bazel + dune integration is much more likely for now
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 :)
editor wars pale in comparison to this :)
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
@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.
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 .
This is how coq rules are implemented, and for the amount of features they provide it is remarkably compact
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
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
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...
"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).
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.
It'll be fun to translate that to Bazel, which disallows dynamic deps since they compromise replicability.
@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?
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?
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)
Very interesting, thanks.
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?
dune already doesn't use -pack
We may end up with just empty mlpacks
Indeed they are empty for now in the make-free build
You need to link statically a few files, some in tactics and some in parsing
vernac
, usually the ones starting by g_
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
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
when I wrote the "no linkall" PR, I had to try manually until I found the right setup
but using ocamlfind solves this problem as it can keep track of the deps
between plugins
that's a lot of logic that dune already knows, which is quite a bit work to replicate
but going back to the static linking, you need to link coqc_bin.cms
which all the corresponding cmxa
coming from the libs
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
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
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
having dynamic deps is pretty convenient when calling ocamldep, otherwise you get into trouble quickly if you are generating a .v file for example
as you gotta stage your build
i was under the impression that bazel would allow that
for dune, if rules are deterministic and sound w.r.t. sandboxing, you get deterministic build despite the dynamic deps
but that's something not enforced indeed, you can write rules that are not deterministic
but that's a bug as rules have to be "functional"
in the sense of "same input" , "same output"
"You need to link statically a few files," - meaning, use -linkall
?
Use linkall + the set of cma
containing all the modules in the codebase
so you need to sure all the cma contain all the modules + pass all the cmas to the command line
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.
@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
.
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
?
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]
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.
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
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
.
IOW, use the bytecode compiler along with whatever flags are needed for the fastest possible builds?
yes
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?
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.
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.
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
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.
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?
The error is due to stale files resulting from unsound build rules or some other problem
You didn't compile coq and the plugin with the same set of common deps
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.
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.
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.
Aren't those just dependency chains? For file generation, at least, there is no need for multiple stages, just a tree of dependencies.
But if I generate a .v
file, I need to run coqdep
after generation to build its dep set, right?
In general I don't know the deps until generation.
Yeah, you can do that (hack the compiler dependency and Coq simultaneously), it's actually pretty easy.
So if my build rules in bazel generate a .ml file, I cannot compile it in the same build?
How does Bazel compute the set of deps for that .ml file before building it?
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.
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.
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!
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.
Everything in theories/Init
now builds. That wasn't so bad. Maybe I can get the rest of the theories done over the weekend.
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?
Never mind. I needed to add -ri Coq.Init.Prelude
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.
files in theory/Init/
do indeed need -boot -noinit, the rest should be compiled as normal.
Note that coqdep won't also emit the dependency for Init/Prelude.vo
so you need to adjust that manually.
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.
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
.
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?
plugins dirs should be passed with -I
That error seems like you forgot to statically link some part of a plugin or coqc?
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.
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.
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
?
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.
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.
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?
Actually coqc should already produce the vos files, tho they should be optional
what is the concrete error
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.
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]
The code for locating things is a mess, fortunately we are very close to doing a big rework
-coqlib dir needs to point to a directory where theories
is present, and in particular theories/Init/Prelude.vo
that's only used when not -boot
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.
Then for coq-stdlib
you need to install it in lib/coq/theories
that's hardcoded
when not using -boot, moreover it will also expect plugins in lib/coq-core/plugins
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]
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.
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.
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
.
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.
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.
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.
If you do Require Import Prelude.
in that coqtop
, and it succeeds, then Check nat.
should work.
Thanks! That worked!
Regarding layout indeed there are two options for now:
-I
-coqlib
-boot
-R dir Coq
to fully specify the Coq working path [dune does this so it can place build artifacts where it wants`lib/coq
and lib/coq-core
.We have an ongoing PR which will make this more flexible, but as of today the second rules are hardcoded among different tools.
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.
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
In Dune we allow to declare that using a flag.
As of today the -noinit
flag for Init/*.v
is hardcoded, but we will make it a parameter
Yeah bootstrapping needs some special setup as you can see
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.
Yup, for the rest of files you need to add Init/Prelude.vo
as dependency
Dune has a special case for this dependency, which is "if Coq's stdlib is in the workspace, then add the dependency"
I'll add that as the rule default, with some kind of override option.
if it is not, then don't add, as it means Prelude is installed globally
This is required as indeed in Dune it is common to blend several libraries together in a build workspace
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
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.
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
Thanks. Question: stdlib - this is everything in theories
except Init
?
It includes Init
it is everything under Coq.*
it could be further split, in Dune we have this notion of "theory"
so what we call "a boot theory" in Dune, is something that includes Coq.Init.Prelude
so that Coq.Init.*
is compiled with -no-init
and the rest is compiled normally, but of course depends on init.prelude
And Coq.*
standardly maps to fs dir theories
?
yes
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
there is the HoTT library which doesn't use the stdlib, so indeed it uses always -no-init
but that's the only case for now, stdlib2 will work the same way
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)
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.
Hehehe. But indeed be sure to document the special case for prelude clearly, as indeed this is a problem users will find often
The concrete problem is "when building my regular Coq library, and Coq is installed, things work fine"
"however if I build it together with Coq, the dependency on the prelude has to be added by the build system"
will do, thanks for the warning.
You got some timings of bazel vs dune for example?
For dune, you can try:
dune build _build/install/default/bin/coqc.byte
dune build theories/Reals/Reals.vo
$ 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.
Interesting, thanks for the data!
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
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
Yeah sys time seems high, but could be due to many factors including memory pressure or different filesystems [or even the cache]
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
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.
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.
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 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.
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.
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.
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.
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
If you add/remove a dep, you must edit the BUILD.bazel file accordingly.
Of course this could be automated in the future.
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.
Yep, sadly that's the way it works, for now at least. But you have to do that with Dune too, no?
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).
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.
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).
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.
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 .
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*: }
Not sure if that has been even already added to master, as the only thing missing is the syntax
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.)
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.
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.
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.
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.
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.
:joy: :joy: :innocent: :innocent:
@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.
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
That should help you a lot IMVHO.
Thanks!
[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]
This is the call to generate the file which is an input for coq_dune
:
(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`"))))
The coq_dune reads the file generated by the above coqdep call, builds the dep map, and dumps it in several dune files
So all you need to do is to change the output format to be a single BUILD file
that should be not too hard
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.
@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.
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.
First problem tho are generated files, in this scenario you have a non-trivial scenario, dynamic deps do provide a nice model for that.
Can you point me to some code that demonstrates the problem you see?
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
This is pretty common workflow on some users
Thanks. I don't suppose you know of a basic tutorial for that?
Never mind, I see Software Foundations covers it.
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
I have a project that is doing something like that today, for example.
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
And actually in a Coq document, there are not separate at all
the graph changes a lot dynamically and interactions are complex
when editing a document I mean
Last updated: Dec 05 2023 at 12:01 UTC