I folks I start this thread to keep the discussion a bit more organized, please move the messages here
as the FRO thread is about a lot of things
In my opinion, build technology is one of the things Coq has still some significant advantages
thanks to all the cool tech developed in Dune that we have adopted.
On the other hand trying to have Coq use this very cool tech has been an absolute hell, due to a variety of reasons.
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"
Which is a very valid (non technical) reason, but harms a lot of people needing more from the build system
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.
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.
A message was moved here from #Coq devs & plugin devs > Lean FRO meeting by Emilio Jesús Gallego Arias.
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
I also want to see a future where I can say goodbye to _CoqProject and nonportable makefiles
honestly it'd be pretty rad if esy were to be the recommended package manager for coq
this is also relevant https://proofassistants.stackexchange.com/questions/2468/iris-algebra-auth-vo-has-bad-version-number-81700-expected-81601-for-iris-coq
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.
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