Stream: Coq devs & plugin devs

Topic: Distributed builds for Coq


view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:00):

I folks I start this thread to keep the discussion a bit more organized, please move the messages here

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:00):

as the FRO thread is about a lot of things

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:00):

In my opinion, build technology is one of the things Coq has still some significant advantages

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:01):

thanks to all the cool tech developed in Dune that we have adopted.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:02):

On the other hand trying to have Coq use this very cool tech has been an absolute hell, due to a variety of reasons.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:02):

Including people oppossing it without any real technical reason I could see, other than "I like my 70s unsound build system, please don't make me change, I'm happy alone in my own island"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:03):

Which is a very valid (non technical) reason, but harms a lot of people needing more from the build system

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:05):

Making builds unsound may sound appealing, but there is a large amount of evidence that it is a shortcut that creates many problems in the long-term.

view this post on Zulip Pierre Roux (Oct 18 2023 at 14:20):

Huỳnh Trần Khanh said:

we can download prebuilt object files off of a server and get up and running

Note that this is already done for some coq-community and math-comp projects using Nix and cachix.

view this post on Zulip Notification Bot (Oct 18 2023 at 14:26):

A message was moved here from #Coq devs & plugin devs > Lean FRO meeting by Emilio Jesús Gallego Arias.

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 15:30):

let's go. this is a very important topic. I want to see a future where coq packages are prebuilt and I can download object files instead of or in addition to source code

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 15:30):

I also want to see a future where I can say goodbye to _CoqProject and nonportable makefiles

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 15:31):

honestly it'd be pretty rad if esy were to be the recommended package manager for coq

view this post on Zulip Huỳnh Trần Khanh (Oct 20 2023 at 15:37):

this is also relevant https://proofassistants.stackexchange.com/questions/2468/iris-algebra-auth-vo-has-bad-version-number-81700-expected-81601-for-iris-coq

view this post on Zulip Pierre Roux (Oct 21 2023 at 07:43):

Huỳnh Trần Khanh said:

honestly it'd be pretty rad if esy were to be the recommended package manager for coq

My understanding is that it's quite close from Nix (but I don't know esy very well) and Nix is, besides OPAM, the package manager/collection offering the largest number of Coq devs.

view this post on Zulip Karl Palmskog (Oct 21 2023 at 13:37):

I think the Coq Docker images (and MathComp images) are a form of distributed builds, especially the rebuilds of dev every night


Last updated: Oct 13 2024 at 01:02 UTC