Arthur Charguéraud (Sep 09 2020 at 11:13): Arthur Charguéraud (Sep 09 2020 at 11:13):It seems that something has changed a couple months ago, now my NIX build is taking 30mins instead of 3mins.
https://travis-ci.com/github/charguer/tlc/builds
because Coq now gets compiled in full. Do you know why it is so?
It makes me feel bad to recompile Coq over and over again, for no good reason. Thanks
Karl Palmskog (Sep 09 2020 at 11:18):@Arthur Charguéraud if this is Nix builds on Coq master using Cachix, then we have had the same issues in coq-community. See https://github.com/coq-community/templates/issues/69 and in particular this comment.
The short version is that unless the right "magic" set of parameters are used, Cachix binary archives will not be used, forcing Nix to build the Coq revision from scratch. The magic parameters seem to change over time, however.
Karl Palmskog (Sep 09 2020 at 11:21):also slightly OT question: is https://github.com/charguer/tlc nowadays the canonical URL/repo for the TLC library?
Arthur Charguéraud (Sep 09 2020 at 11:28):@Karl Palmskog yes TLC is now hosted on github. I have a branch that exploits the new features of Coq v8.12, I'll merge it into master in the near future, when support for 8.11 is no longer needed.
Karl Palmskog (Sep 11 2020 at 11:13):@Théo Zimmermann @Arthur Charguéraud it seems coq-community Cachix Travis has started working properly again. This means the TLC Travis builds can be fixed also, I can whip up a PR later today.
Last updated: Oct 13 2024 at 01:02 UTC