Stream: Coq users

Topic: Bazel for Coq


view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:38):

Has anybody looked into building Coq projects with Bazel?

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:38):

Anybody care to guess how hard that would be?

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:39):

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

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 18:39):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 21:17):

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

view this post on Zulip Paolo Giarrusso (Dec 04 2020 at 21:18):

(either would be cool)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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: Jan 28 2023 at 05:02 UTC