merge master

Author: Joris van Winden

.github/workflows/PR_summary.yml

@@ -216,8 +216,23 @@ jobs:
         echo "Compute technical debt changes"
         techDebtVar="$(../master-branch/scripts/technical-debt-metrics.sh pr_summary)"
 
+        echo "Compute documentation reminder"
+        workflowFilesChanged="$(grep '^\.github/workflows/' changed_files.txt || true)"
+        if [ -n "${workflowFilesChanged}" ]
+        then
+          # Format each changed workflow path as a Markdown bullet: "- `path`"
+          workflowFilesChangedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${workflowFilesChanged}")"
+          workflowDocsReminder="$(printf "### Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
+        else
+          workflowDocsReminder=""
+        fi
+
         # store in a file, to avoid "long arguments" error.
         printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > please_merge_master.md
+        if [ -n "${workflowDocsReminder}" ]
+        then
+          printf '\n\n---\n\n%s\n' "${workflowDocsReminder}" >> please_merge_master.md
+        fi
 
         echo "Include any errors about removed or renamed files without deprecation,"
         echo "as well as errors about extraneous deprecated_module additions."

.github/workflows/actionlint.yml

@@ -16,4 +16,16 @@ jobs:
         uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
         with:
           tool_name: actionlint
-          fail_level: error
+          fail_level: any
+
+  ensure-sha-pinned-actions:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      # Using our fork's PR branch until upstream merges the improved error reporting:
+      # https://github.com/zgosalvez/github-actions-ensure-sha-pinned-actions/pull/288
+      # TODO: Update to upstream release once merged.
+      - name: Ensure all actions are pinned to SHA
+        uses: kim-em/github-actions-ensure-sha-pinned-actions@00f51cdb5bbc21f5bc873ef3a2dceef45df213af # improve-error-reporting

.github/workflows/build_template.yml

@@ -243,6 +243,31 @@ jobs:
             echo "✅ All inputRevs in lake-manifest.json are valid"
           fi
 
+      - name: validate ProofWidgets source repository
+        # Only enforce this on the main mathlib4 repository, not on nightly-testing
+        if: github.repository == 'leanprover-community/mathlib4'
+        shell: bash
+        run: |
+          cd pr-branch
+
+          expected_url='https://github.com/leanprover-community/ProofWidgets4'
+          proofwidgets_count=$(jq '[.packages[] | select(.name == "proofwidgets")] | length' lake-manifest.json)
+          if [ "$proofwidgets_count" -ne 1 ]; then
+            echo "❌ Error: expected exactly one proofwidgets entry in lake-manifest.json, found $proofwidgets_count"
+            exit 1
+          fi
+
+          proofwidgets_url=$(jq -r '.packages[] | select(.name == "proofwidgets") | .url' lake-manifest.json)
+          normalized_url="${proofwidgets_url%.git}"
+          if [ "$normalized_url" != "$expected_url" ]; then
+            echo "❌ Error: invalid ProofWidgets source URL in lake-manifest.json"
+            echo "  expected: $expected_url"
+            echo "  found:    $proofwidgets_url"
+            exit 1
+          fi
+
+          echo "✅ ProofWidgets source URL is trusted: $proofwidgets_url"
+
       - name: verify ProofWidgets lean-toolchain matches on versioned releases
         # Only enforce this on the main mathlib4 repository, not on nightly-testing
         if: github.repository == 'leanprover-community/mathlib4'
@@ -298,7 +323,7 @@ jobs:
 
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
           echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
+          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Mathlib/Init.lean
 
       - name: get cache (2/3 - test Mathlib.Init cache)
         id: get_cache_part2_test
@@ -318,15 +343,23 @@ jobs:
           if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then
             echo "Fetching all remaining cache..."
 
-            ../tools-branch/.lake/build/bin/cache get
+            ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get
 
             # Run again with --repo, to ensure we actually get the oleans.
-            ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
+            ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --skip-proofwidgets get
           else
             echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
             echo "No cache for 'Mathlib.Init' available or it could not be prepared."
           fi
 
+      - name: fetch ProofWidgets release
+        # We need network access for ProofWidgets frontend assets.
+        # Run inside landrun so PR-controlled code remains sandboxed.
+        shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
+        run: |
+          cd pr-branch
+          lake build proofwidgets:release
+
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
@@ -380,8 +413,8 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../tools-branch/.lake/build/bin/cache get Archive.lean
-          ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Archive.lean
+          ../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Counterexamples.lean
 
       - name: build archive
         id: archive
@@ -399,37 +432,38 @@ jobs:
           ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
-      - name: prepare cache staging directory
-        if: ${{ steps.build.outcome == 'success' }}
+      - name: prepare staging directory
+        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
         shell: bash
         run: |
+          # Clean the staging directory first, though it should be empty at this point, to be safe
           rm -rf cache-staging
           mkdir -p cache-staging
 
       - name: stage Mathlib cache files
-        if: ${{ steps.build.outcome == 'success' }}
-        shell: bash
+        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
+        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
         run: |
           cd pr-branch
           lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage
 
       - name: stage Archive cache files
         if: ${{ steps.archive.outcome == 'success' }}
-        shell: bash
+        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
         run: |
           cd pr-branch
           lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Archive.lean
 
       - name: stage Counterexamples cache files
         if: ${{ steps.counterexamples.outcome == 'success' }}
-        shell: bash
+        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
         run: |
           cd pr-branch
           lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Counterexamples.lean
 
       - name: check cache staging contents
         id: cache_staging_check
-        if: ${{ steps.build.outcome == 'success' }}
+        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
         shell: bash
         run: |
           if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .; then
@@ -439,7 +473,7 @@ jobs:
           fi
 
       - name: upload cache staging artifact
-        if: ${{ steps.cache_staging_check.outputs.has_files == 'true' }}
+        if: ${{ always() && steps.cache_staging_check.outputs.has_files == 'true' }}
         uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
         with:
           name: cache-staging
@@ -609,7 +643,7 @@ jobs:
     # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
     # but not if any earlier step failed or was cancelled.
     # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
-    if: ${{ always() && needs.build.outputs.build-outcome == 'success' && needs.build.outputs.get-cache-outcome == 'success' && needs.build.outputs.cache-staging-has-files == 'true' }}
+    if: ${{ always() && needs.build.outputs.cache-staging-has-files == 'true' }}
     steps:
       - name: Checkout tools branch
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
@@ -655,6 +689,7 @@ jobs:
   post_steps:
     name: Post-Build Step
     needs: [build, upload_cache]
+    if: ${{ always() && needs.build.result == 'success' && (needs.upload_cache.result == 'success' || needs.upload_cache.result == 'skipped') }}
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
 
@@ -744,7 +779,8 @@ jobs:
 
   final:
     name: Post-CI job
-    if: ${{ inputs.run_post_ci }}
+    # ensure that this runs iff direct dependencies succeeded even if transitive dependencies  were skipped
+    if: ${{ always() && inputs.run_post_ci && needs.style_lint.result == 'success' && needs.build.result == 'success' && needs.post_steps.result == 'success' }}
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:

.github/workflows/daily.yml

@@ -314,7 +314,7 @@ jobs:
           reinstall-transient-toolchain: true
 
       - name: Install Rust
-        uses: dtolnay/rust-toolchain@stable
+        uses: dtolnay/rust-toolchain@631a55b12751854ce901bb631d5902ceb48146f7 # stable
 
       - name: Check Mathlib using nanoda # make sure this name is consistent with "Get job status and URLs" in the notify job
         id: nanoda

.github/workflows/export_telemetry.yaml

@@ -15,14 +15,14 @@ permissions:
 
 jobs:
   otel-export:
-    if: github.repository == 'leanprover-community/mathlib4'
+    if: ${{ github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' }}
     runs-on: ubuntu-latest
     steps:
       - name: Export workflow telemetry
         uses: corentinmusard/otel-cicd-action@7e307f7baefcf4929d94d2844bc72d87566a75c3 # v3.0.0
         with:
-          otlpEndpoint: ${{ secrets.OTLP_ENDPOINT_ALT }}
-          otlpHeaders: ${{ secrets.OTLP_HEADERS_ALT }}
+          otlpEndpoint: ${{ vars.OTLP_ENDPOINT }}
+          otlpHeaders: ${{ secrets.OTLP_HEADERS }}
           otelServiceName: "mathlib-ci"
           githubToken: ${{ secrets.GITHUB_TOKEN }}
           runId: ${{ github.event.workflow_run.id }}

.github/workflows/nightly-docgen.yml

@@ -18,7 +18,7 @@ jobs:
           rm -rf "$HOME/.cache/mathlib"
 
       - name: Checkout mathlib
-        uses: actions/checkout@v6.0.2
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           repository: leanprover-community/mathlib4-nightly-testing
           ref: nightly-testing-green

.github/workflows/nightly_bump_and_merge.yml

@@ -59,8 +59,15 @@ jobs:
 
     - name: Get latest release tag from leanprover/lean4-nightly
       id: get-latest-release
+      env:
+        GH_TOKEN: ${{ steps.app-token.outputs.token }}
       run: |
-        RELEASE_TAG="$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')"
+        RELEASE_TAG=$(gh api -X GET repos/leanprover/lean4-nightly/releases \
+          -f per_page=1 --jq '.[0].tag_name')
+        if [ -z "$RELEASE_TAG" ] || [ "$RELEASE_TAG" = "null" ]; then
+          echo "::error::Could not determine latest lean4-nightly release"
+          exit 1
+        fi
         echo "RELEASE_TAG=$RELEASE_TAG"
         echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}"
         echo "new=$RELEASE_TAG" >> "$GITHUB_OUTPUT"
@@ -88,6 +95,8 @@ jobs:
     - name: Clone lean4-nightly and get PRs
       id: get-prs
       if: steps.commit-bump.outputs.bumped == 'true'
+      env:
+        GH_TOKEN: ${{ steps.app-token.outputs.token }}
       run: |
         OLD="${{ steps.old-toolchain.outputs.old }}"
         NEW="${{ steps.get-latest-release.outputs.new }}"
@@ -121,9 +130,11 @@ jobs:
           echo "Checking commit $commit_sha for associated PRs..."
 
           # Query GitHub API for PRs associated with this commit
-          pr_numbers=$(curl -s -H "Accept: application/vnd.github.v3+json" \
-            "https://api.github.com/repos/leanprover/lean4/commits/$commit_sha/pulls" | \
-            jq -r '.[] | select(.merged_at != null) | .number | tostring' 2>/dev/null || echo "")
+          pr_numbers=$(gh api "repos/leanprover/lean4/commits/$commit_sha/pulls" \
+            --jq '[.[] | select(.merged_at != null) | .number] | .[] | tostring' 2>/dev/null) || {
+            echo "::warning::Failed to fetch PRs for commit $commit_sha, skipping"
+            continue
+          }
 
           # Add each PR number to our list (duplicates will be handled later)
           for pr_num in $pr_numbers; do
@@ -295,7 +306,7 @@ jobs:
           MESSAGE+=$'### Successfully merged branches into \'nightly-testing\':\n\n'
           for MERGE_INFO in $SUCCESSFUL_MERGES; do
             IFS='|' read -r PR_NUMBER GITHUB_DIFF _ <<< "$MERGE_INFO"
-            MESSAGE+=$(printf -- '- [lean-pr-testing-%s](%s) (adaptations for lean#%s)' "$PR_NUMBER" "$GITHUB_DIFF" "$PR_NUMBER")$'\n\n'
+            MESSAGE+="- [lean-pr-testing-${PR_NUMBER}](${GITHUB_DIFF}) (adaptations for lean#${PR_NUMBER})"$'\n\n'
           done
           MESSAGE+=$'\n'
         else
@@ -307,9 +318,9 @@ jobs:
           MESSAGE+=$'### Failed merges:\n\nThe following branches need to be merged manually into \'nightly-testing\':\n\n'
           for MERGE_INFO in $FAILED_MERGES; do
             IFS='|' read -r PR_NUMBER GITHUB_DIFF _ <<< "$MERGE_INFO"
-            MESSAGE+=$(printf '- [lean-pr-testing-%s](%s) (adaptations for lean#%s)' "$PR_NUMBER" "$GITHUB_DIFF" "$PR_NUMBER")$'\n\n'
+            MESSAGE+="- [lean-pr-testing-${PR_NUMBER}](${GITHUB_DIFF}) (adaptations for lean#${PR_NUMBER})"$'\n\n'
             MESSAGE+=$'```bash\n'
-            MESSAGE+=$(printf 'scripts/merge-lean-testing-pr.sh %s' "$PR_NUMBER")$'\n'
+            MESSAGE+="scripts/merge-lean-testing-pr.sh ${PR_NUMBER}"$'\n'
             MESSAGE+=$'```\n\n'
           done
         else

.github/workflows/release.yml

@@ -0,0 +1,21 @@
+name: Release
+
+on:
+  push:
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+      - "v[0-9]+.[0-9]+.[0-9]+-rc[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  release:
+    runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
+    steps:
+      - name: Create GitHub Release
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b # v2.5.0
+        with:
+          prerelease: ${{ contains(github.ref, 'rc') }}
+          make_latest: ${{ !contains(github.ref, 'rc') }}

.github/workflows/splice_bot.yaml

@@ -0,0 +1,15 @@
+name: splice-bot
+
+on:
+  pull_request_review_comment:
+    types: [created]
+
+permissions: {}
+
+jobs:
+  call-splice-bot:
+    if: ${{ contains(github.event.comment.body, 'splice-bot') }}
+    uses: leanprover-community/SpliceBot/.github/workflows/splice.yaml@fdb442693d6f613b25d2599ad64fd87cf019b9ce # master
+    with:
+      # Optional override; omit to use the reusable workflow's default "master"
+      base_ref: master

.github/workflows/splice_bot_wf_run.yaml

@@ -0,0 +1,29 @@
+name: splice-bot (workflow_run)
+
+on:
+  workflow_run:
+    workflows: ["splice-bot"]
+    types: [completed]
+
+permissions: {}
+
+jobs:
+  run-reusable:
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}
+    uses: leanprover-community/SpliceBot/.github/workflows/splice_wf_run.yaml@fdb442693d6f613b25d2599ad64fd87cf019b9ce # master
+    with:
+      source_workflow: ${{ github.event.workflow_run.name }}
+      push_to_fork: leanprover-community/mathlib4_copy
+      allow_pr_author: true
+      allowed_teams: |
+        leanprover-community/mathlib-reviewers
+        leanprover-community/mathlib-maintainers
+      # Installation owner used when minting token from app secrets below.
+      token_app_owner: leanprover-community
+    secrets:
+      token_app_id: ${{ secrets.MATHLIB_SPLICEBOT_APP_ID }}
+      token_app_private_key: ${{ secrets.MATHLIB_SPLICEBOT_PRIVATE_KEY }}
+      authz_token_app_id: ${{ secrets.LPC_TEAM_CHECK_APP_ID }}
+      authz_token_app_private_key: ${{ secrets.LPC_TEAM_CHECK_PRIVATE_KEY }}
+      branch_token_app_id: ${{ secrets.MATHLIB_COPY_SPLICEBOT_APP_ID }}
+      branch_token_app_private_key: ${{ secrets.MATHLIB_COPY_SPLICEBOT_PRIVATE_KEY }}