Skip to content

Commit 40eadec

Browse files
faenucciofaenuccio
committed
Merge branch 'master' into fae_MilmanPettis
2 parents 7118513 + bbd46d7 commit 40eadec

2,126 files changed

Lines changed: 36032 additions & 21445 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/build.in.yml‎

Lines changed: 93 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ jobs:
277277
!pr-branch/.git/
278278
279279
# The cache secrets are available here, so we must not run any untrusted code.
280-
- name: upload cache
280+
- name: Upload cache to Azure
281281
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
282282
# but not if any earlier step failed or was cancelled.
283283
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
@@ -288,19 +288,50 @@ jobs:
288288
289289
# Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
290290
export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
291-
export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
292291
293292
# Use the trusted cache tool from master-branch
294293
# TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
295294
# ../master-branch/.lake/build/bin/cache commit || true
296295
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
297296
# ../master-branch/.lake/build/bin/cache put!
298297
# do not try to upload files just downloaded
299-
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
298+
299+
echo "Uploading cache to Azure..."
300+
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
300301
env:
301302
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
303+
304+
# The cache secrets are available here, so we must not run any untrusted code.
305+
- name: Upload cache to Cloudflare
306+
id: cloudflare-upload-mathlib
307+
if: ${{ always() && steps.get.outcome == 'success' }}
308+
continue-on-error: true
309+
shell: bash
310+
run: |
311+
cd pr-branch
312+
313+
# Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
314+
export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
315+
316+
echo "Uploading cache to Cloudflare..."
317+
USE_FRO_CACHE=1 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
318+
env:
302319
MATHLIB_CACHE_S3_TOKEN_RAW: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
303320

321+
- name: Report Cloudflare upload failure on Zulip
322+
if: steps.cloudflare-upload-mathlib.outcome == 'failure'
323+
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
324+
with:
325+
api-key: ${{ secrets.ZULIP_API_KEY }}
326+
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
327+
organization-url: 'https://leanprover.zulipchat.com'
328+
to: 'nightly-testing'
329+
type: 'stream'
330+
topic: 'Cloudflare cache upload failure'
331+
content: |
332+
❌ Cloudflare cache upload (Mathlib) [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) for PR #${{ github.event.pull_request.number || 'push' }} on commit ${{ github.sha }}
333+
continue-on-error: true
334+
304335
# Note: we should not be including `Archive` and `Counterexamples` in the cache.
305336
# We do this for now for the sake of not rebuilding them in every CI run
306337
# even when they are not touched.
@@ -342,21 +373,50 @@ jobs:
342373
exit 1
343374
344375
# The cache secrets are available here, so we must not run any untrusted code.
345-
- name: put archive and counterexamples cache
376+
- name: Upload Archive and Counterexamples cache to Azure
346377
shell: bash
347378
run: |
348379
cd pr-branch
349380
350381
# Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
351382
export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
352-
export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
353383
354-
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
355-
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
384+
echo "Uploading Archive and Counterexamples cache to Azure..."
385+
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
386+
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
356387
env:
357388
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
389+
390+
- name: Upload Archive and Counterexamples cache to Cloudflare
391+
id: cloudflare-upload-archive
392+
continue-on-error: true
393+
shell: bash
394+
run: |
395+
cd pr-branch
396+
397+
# Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
398+
export MATHLIB_CACHE_S3_TOKEN="${MATHLIB_CACHE_S3_TOKEN_RAW%"${MATHLIB_CACHE_S3_TOKEN_RAW##*[![:space:]]}"}"
399+
400+
echo "Uploading Archive and Counterexamples cache to Cloudflare..."
401+
USE_FRO_CACHE=1 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
402+
USE_FRO_CACHE=1 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
403+
env:
358404
MATHLIB_CACHE_S3_TOKEN_RAW: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
359405

406+
- name: Report Cloudflare Archive/Counterexamples upload failure on Zulip
407+
if: steps.cloudflare-upload-archive.outcome == 'failure'
408+
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
409+
with:
410+
api-key: ${{ secrets.ZULIP_API_KEY }}
411+
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
412+
organization-url: 'https://leanprover.zulipchat.com'
413+
to: 'nightly-testing'
414+
type: 'stream'
415+
topic: 'Cloudflare cache upload failure'
416+
content: |
417+
❌ Cloudflare cache upload (Archive/Counterexamples) [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) for PR #${{ github.event.pull_request.number || 'push' }} on commit ${{ github.sha }}
418+
continue-on-error: true
419+
360420
- name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
361421
if: always()
362422
run: |
@@ -460,18 +520,39 @@ jobs:
460520
with:
461521
auto-config: false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
462522
use-github-cache: false
463-
use-mathlib-cache: true
523+
use-mathlib-cache: false # This can be re-enabled once we are confident in the cache again.
464524
reinstall-transient-toolchain: true
465525

466-
# TODO: this step should not be necessary, "Configure Lean" above should already achieve this.
526+
- name: retrieve and test the Cloudflare caches, but don't fail, just report to Zulip, if anything goes wrong
527+
id: cloudflare-cache
528+
continue-on-error: true
529+
run: |
530+
lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
531+
lake build --no-build -v Mathlib
532+
lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get Archive Counterexamples
533+
lake build --no-build -v Archive Counterexamples
534+
535+
- name: Report Cloudflare cache failure on Zulip
536+
if: steps.cloudflare-cache.outcome == 'failure'
537+
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
538+
with:
539+
api-key: ${{ secrets.ZULIP_API_KEY }}
540+
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
541+
organization-url: 'https://leanprover.zulipchat.com'
542+
to: 'nightly-testing'
543+
type: 'stream'
544+
topic: 'Cloudflare cache failure'
545+
content: |
546+
❌ Cloudflare cache retrieval/test [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) for PR #${{ github.event.pull_request.number || 'push' }} on commit ${{ github.sha }}
547+
continue-on-error: true
548+
467549
- name: get cache for Mathlib
468550
run: |
469551
# Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
470552
lake exe cache get
471553
# Run again with --repo, so ensure we actually get the oleans.
472554
lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
473555
474-
475556
- name: get cache for Archive and Counterexamples
476557
run: |
477558
# Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
@@ -551,7 +632,7 @@ jobs:
551632
if: FORK_CONDITION
552633
runs-on: ubuntu-latest
553634
steps:
554-
- uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
635+
- uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
555636
with:
556637
mode: check
557638
lint-bib-file: true
@@ -574,10 +655,9 @@ jobs:
574655
runs-on: ubuntu-latest
575656
steps:
576657
# This action is used to determine the PR metadata in the event of a push.
577-
# If it is called from a PR from a fork, it will find nothing/irrelevant data.
578658
- if: github.event_name != 'pull_request_target'
579659
id: PR_from_push
580-
uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
660+
uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
581661
# TODO: this may not work properly if the same commit is pushed to multiple branches:
582662
# https://github.com/8BitJonny/gh-get-current-pr/issues/8
583663
with:

0 commit comments

Comments
 (0)