Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(.github/workflows): increase olean generation timeout (#15784)
Browse files Browse the repository at this point in the history
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 <[email protected]>
  • Loading branch information
collares and bentoner committed Aug 31, 2022
1 parent fe5e4ce commit 13618c1
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/bors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ jobs:
leanpkg configure
echo "::set-output name=started::true"
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py
- name: push release to azure
if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ jobs:
leanpkg configure
echo "::set-output name=started::true"
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py
- name: push release to azure
if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/build.yml.in
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ jobs:
leanpkg configure
echo "::set-output name=started::true"
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py

- name: push release to azure
if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/build_fork.yml
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ jobs:
leanpkg configure
echo "::set-output name=started::true"
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T150000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py
- name: push release to azure
if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
Expand Down

0 comments on commit 13618c1

Please sign in to comment.