Merge branch 'master' into fewer-expr-copies

.github/workflows/ci.yml

@@ -298,8 +298,8 @@ jobs:
         uses: msys2/setup-msys2@v2
         with:
           msystem: clang64
-          # `:p` means prefix with appropriate msystem prefix
-          pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
+          # `:` means do not prefix with msystem
+          pacboy: "make: python: cmake clang ccache gmp git: zip: unzip: diffutils: binutils: tree: zstd tar:"
         if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
@@ -426,7 +426,7 @@ jobs:
         if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
-          make -C build -j$NPROC stage3
+          make -C build -j$NPROC check-stage3
         if: matrix.test-speedcenter
       - name: Test Speedcenter Benchmarks
         run: |
@@ -455,12 +455,24 @@ jobs:
     # mark as merely cancelled not failed if builds are cancelled
     if: ${{ !cancelled() }}
     steps:
+    - if: ${{ contains(needs.*.result, 'failure') && github.repository == 'leanprover/lean4' && github.ref_name == 'master' }}
+      uses: zulip/github-actions-zulip/send-message@v1
+      with:
+        api-key: ${{ secrets.ZULIP_BOT_KEY }}
+        email: "[email protected]"
+        organization-url: "https://lean-fro.zulipchat.com"
+        to: "infrastructure"
+        topic: "Github actions"
+        type: "stream"
+        content: |
+          A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
     - if: contains(needs.*.result, 'failure')
       uses: actions/github-script@v7
       with:
         script: |
             core.setFailed('Some jobs failed')
 
+
   # This job creates releases from tags
   # (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
   # We do not attempt to automatically construct a changelog here:
@@ -533,3 +545,8 @@ jobs:
           gh workflow -R leanprover/release-index run update-index.yml
         env:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
+      - name: Update toolchain on mathlib4's nightly-testing branch
+        run: |
+          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
+        env:
+          GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/jira.yml

@@ -0,0 +1,34 @@
+name: Jira sync
+
+on:
+  issues:
+    types: [closed]
+
+jobs:
+  jira-sync:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Move Jira issue to Done
+        env:
+          JIRA_API_TOKEN: ${{ secrets.JIRA_API_TOKEN }}
+          JIRA_USERNAME: ${{ secrets.JIRA_USERNAME }}
+          JIRA_BASE_URL: ${{ secrets.JIRA_BASE_URL }}
+        run: |
+          issue_number=${{ github.event.issue.number }}
+
+          jira_issue_key=$(curl -s -u "${JIRA_USERNAME}:${JIRA_API_TOKEN}" \
+            -X GET -H "Content-Type: application/json" \
+            "${JIRA_BASE_URL}/rest/api/2/search?jql=summary~\"${issue_number}\"" | \
+            jq -r '.issues[0].key')
+
+          if [ -z "$jira_issue_key" ]; then
+            exit
+          fi
+
+          curl -s -u "${JIRA_USERNAME}:${JIRA_API_TOKEN}" \
+            -X POST -H "Content-Type: application/json" \
+            --data "{\"transition\": {\"id\": \"41\"}}" \
+            "${JIRA_BASE_URL}/rest/api/2/issue/${jira_issue_key}/transitions"
+
+          echo "Moved Jira issue ${jira_issue_key} to Done"

.github/workflows/nix-ci.yml

@@ -103,7 +103,7 @@ jobs:
         continue-on-error: true
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
           # https://github.com/netlify/cli/issues/1809
           cp -r --dereference ./result ./dist
@@ -146,5 +146,3 @@ jobs:
       - name: Fixup CCache Cache
         run: |
           sudo chown -R $USER /nix/var/cache
-      - name: CCache stats
-        run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s

CONTRIBUTING.md

@@ -63,6 +63,20 @@ Because the change will be squashed, there is no need to polish the commit messa
 Reviews and Feedback:
 ----
 
+The lean4 repo is managed by the Lean FRO's *triage team* that aims to provide initial feedback on new bug reports, PRs, and RFCs weekly.
+This feedback generally consists of prioritizing the ticket using one of the following categories:
+* label `P-high`: We will work on this issue
+* label `P-medium`: We may work on this issue if we find the time
+* label `P-low`: We are not planning to work on this issue
+* *closed*: This issue is already fixed, it is not an issue, or is not sufficiently compatible with our roadmap for the project and we will not work on it nor accept external contributions on it
+
+For *bug reports*, the listed priority reflects our commitment to fixing the issue.
+It is generally indicative but not necessarily identical to the priority an external contribution addressing this bug would receive.
+For *PRs* and *RFCs*, the priority reflects our commitment to reviewing them and getting them to an acceptable state.
+Accepted RFCs are marked with the label `RFC accepted` and afterwards assigned a new "implementation" priority as with bug reports.
+
+General guidelines for interacting with reviews and feedback:
+
 **Be Patient**: Given the limited number of full-time maintainers and the volume of PRs, reviews may take some time.
 
 **Engage Constructively**: Always approach feedback positively and constructively. Remember, reviews are about ensuring the best quality for the project, not personal criticism.