Stream: Coq users

Topic: Bazel for Coq

Paolo Giarrusso (Dec 04 2020 at 18:38):

Has anybody looked into building Coq projects with Bazel?

Paolo Giarrusso (Dec 04 2020 at 18:38):

Anybody care to guess how hard that would be?

Paolo Giarrusso (Dec 04 2020 at 18:39):

(I think "hard", some colleagues thought "easy", so we thought we'd ask outsiders).

Paolo Giarrusso (Dec 04 2020 at 18:39):

@Karl Palmskog cites Bazel so he must have wondered a bit...

Rudi Grinberg (Dec 04 2020 at 20:17):

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.

Paolo Giarrusso (Dec 04 2020 at 21:17):

Wait, do you plan to do remote caching, or delegating to bazel?

Paolo Giarrusso (Dec 04 2020 at 21:18):

(either would be cool)

Paolo Giarrusso (Dec 04 2020 at 21:19):

How stable is the cache BTW? I assume it carries over at least the same docker image...

Rudi Grinberg (Dec 05 2020 at 01:11):

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.

Rudi Grinberg (Dec 05 2020 at 01:12):

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: Sep 23 2023 at 06:01 UTC