Zulip Chat Archive
Stream: combinatorial-games
Topic: GitHub actions
Violeta Hernández (Dec 12 2025 at 12:28):
Just realized that our build action succeeds even when there's sorry in the proofs. Is this something we want? Can we make it so that the action fails on warnings? @Tristan Figueroa-Reid
Some example logs: https://github.com/vihdzp/combinatorial-games/actions/runs/20166085232/job/57889703216?pr=263
Violeta Hernández (Dec 12 2025 at 16:14):
Also, does it make sense for the GitHub pages action to run on every PR? Given that it takes 20 minutes to run it seems a bit wasteful to do so
Violeta Hernández (Jan 26 2026 at 02:47):
All the builds are suddenly failing
Violeta Hernández (Jan 26 2026 at 02:47):
Any idea what's going on?
Violeta Hernández (Jan 26 2026 at 02:48):
Aaron Liu (Jan 26 2026 at 02:58):
this is the same error I get when I am offline
Aaron Liu (Jan 26 2026 at 02:58):
though it could be the case of multiple errors with the same error message
Violeta Hernández (Jan 26 2026 at 11:27):
Bumped Mathlib and that seems to have fixed it. Weird.
Last updated: Feb 28 2026 at 14:05 UTC