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