Building Coq with Bazel - need help with plugins

Developing the Coq system
#1

Hi folks. I’m almost done building the OCaml parts of Coq with OBazl. Caveat: OBazl is new and undergoing some changes, so the docs are a little outdated.

I’ve run into problems building some of the plugins. I posted a message to the Coq channel of the OCaml discord server. Which is the most appropriate forum?

I will also need some help with the next phase, which is building the .v files. I have very little experience with Coq, so I’ll need some guidance for that.

Thanks,

Gregg

#2

You should probably join https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs

1 Like
#3

What is your use case for wanting to build Coq with OBazl? Is it just because it’s a gigantic test case? In any case, we’ve already had a long and difficult experience migrating to Dune over the last two and half years and there is still a lot to do, so this is not really a good time to propose yet another build system. I think we’ll want some stability for a while.

#4

That’s an interesting project, but indeed building OCaml is not so easy. Quoting your message:

Hi folks. I need some help from anybody familiar with the Coq build system. I’m building Coq with Bazel, and I’ve got almost all of it working, but I’ve run into problems with some of the plugins. I’m using -pack and here’s the kind of problem I’m encountering:

$ bazel build plugins/ltac:Ltac_plugin
...
File "bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl/Ltac_plugin.cmx", line 1:
Error: File bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl/Pptactic.cmx
      was compiled without access to the .cmx file for module Tacarg,
      which was produced by `ocamlopt -for-pack'.
      Please recompile bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl/Pptactic.cmx
      with the correct `-I' option so that Tacarg.cmx is found.

I need help interpreting the precise meaning of this message. As far as I can tell, module Pptactic.cmx did have access to Tacarg.cmx , built with -for-pack Ltac_plugin , and all the relevant files are on the search path - the source files (.mli, .ml) and Tacarg.cmi , Tacarg.cmx , Tacarg.o are all right there in bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl , which was passed using -I to the build command for Pptactic .

I spent most of today trying to figure this one out, and I’m out of ideas. I suspect it must have something to do with the .cmi file, but I need to know exactly what “was compiled without access to” means, etc. If you can help let me know and I can post more info, here or in the OBazl discord server, or wherever is appropriate.

First note that Coq master will stop using -pack in (hopefully) a matter of days, we instead use module aliases for packing, you can check the OCaml manual for an overview of the differences between these two packing methods. As for your concrete problem, it is hard to say anything as you provided little information such as the build log of the project and the concrete ocamlc invocations.

A quick way to debug this is just compare the two build logs, and in concrete, the calls to ocamlc for Pptactic.ml and Tacarg.ml{,i}.

#5
Zimmi48
March 31

What is your use case for wanting to build Coq with OBazl? Is it just because it’s a gigantic test case? In any case, we’ve already had a long and difficult experience migrating to Dune over the last two and half years and there is still a lot to do, so this is not really a good time to propose yet another build system. I think we’ll want some stability for a while.

Yeah, mostly wanted to see how hard it would be to add Bazel support now that rules_obazl are getting close to finished and Coq is the flagship OCaml app. It’s not that gigantic, believe it or not - my original test case, and the reason I set about writing rules_obazl in the first place, was Mina, which is a bit more complicated (the build, not the code).

Whether and when the Coq project wants to officially support Bazel is of course a whole 'nother matter. Two and a half years migrating to Dune, yikes. Well having spent many painful months trying to grok OCaml build logic and make it work with Bazel, believe me when I say: I feel your pain.

On the bright side, it only took me a few days to get all the OCaml code in Coq building, and most of that time was consumed by the trivial and tedious task of writing the BUILD.bazel files by hand (automated tooling to do this is planned). Building with -pack is still giving me problems,. but OBazl has pretty good support for using aliasing modules (with or without automatic renaming) and that works fine.

Of course, whether or not I’ve covered everything, and whether all the builds are correct, is another issue, that’s where I’m hoping somebody who knows the territory would be willing to help out.

Then there’s the coqc and .v files stuff, which I think calls for some new Bazel rules. I’m going to spend a couple days tackling that so you’ll probably see some heart-rending pleas for help from me.

Thanks,

Gregg

#6
ejgallego
March 31

That’s an interesting project, but indeed building OCaml is not so easy. Quoting your message:

…snip…

First note that Coq master will stop using -pack in (hopefully) a matter of days, we instead use module aliases for packing

Cool, I already switched to this technique since I couldn’t get -pack to work. I will probably spend a little more time working on -pack support, just to make sure that rules_obazl supports such legacy methods.

BTW I’ve added a little bit of documentation to the README of my fork, in case anybody wants to play around with it. (Caveat: I’m going to be updating it off and on over the next few days.) https://github.com/obazl/coq

, you can check the OCaml manual for an overview of the differences between these two packing methods. As for your concrete problem, it is hard to say anything as you provided little information such as the build log of the project and the concrete ocamlc invocations.

Yeah, did not want to spam the list until I was sure somebody might be interested. I’ll put together a gist or something with all the details.

Thanks,

Gregg