Has anybody looked into building Coq projects with Bazel?
Anybody care to guess how hard that would be?
(I think "hard", some colleagues thought "easy", so we thought we'd ask outsiders).
@Karl Palmskog cites Bazel so he must have wondered a bit...
That's something that's on the long todo list of dune. Of course, what we'd like is something that is no way coq specific and is able to run any dune builds. We've had a prototype that sort of worked by ejecting the rules into a makefile at one point.
Wait, do you plan to do remote caching, or delegating to bazel?
(either would be cool)
How stable is the cache BTW? I assume it carries over at least the same docker image...
We plan to do our own remote caching. Generating bazel rules would obviously delegate the bazel. The main motivation for emitting bazel rules is to play nice with existing monorepos people might have, not for performance.
The dune cache is quite stable and I wholeheartedly recommend to use it. What's stopping its adoption is opam's sandboxing mechanism and abundance of non deterministic rules.
Last updated: Jan 28 2023 at 05:02 UTC