mathlib3
13618c1c - chore(.github/workflows): increase olean generation timeout (#15784)

Commit
3 years ago
chore(.github/workflows): increase olean generation timeout (#15784) We are currently experiencing timeouts when saving some oleans (leanprover-community/lean#749). Since Lean does not error out when deterministic timeouts happen during olean generation (leanprover-community/lean#750) and we already run Lean twice when compiling mathlib, Ben Toner suggested the following clever hack: Increase the timeout, but only on the second lean run. This effectively means anything that was reported as a timeout before is still reported as a timeout (by the first call), while olean generation gets more heartbeats. Co-authored-by: Ben Toner <bentoner@bentoner.com>
Author
Parents
Loading