Merge branch 'joachim/rfl-errors' into joachim/iff-rfl-attrib

.github/ISSUE_TEMPLATE/bug_report.md

@@ -9,9 +9,15 @@ assignees: ''
 
 ### Prerequisites
 
-* [ ] Put an X between the brackets on this line if you have done all of the following:
-    * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
-    * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
+Please put an X between the brackets as you perform the following steps:
+
+* [ ] Check that your issue is not already filed:
+      https://github.com/leanprover/lean4/issues
+* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
+      Avoid dependencies to Mathlib or Batteries.
+* [ ] Test your test case against the latest nightly release, for example on
+      https://live.lean-lang.org/#project=lean-nightly
+      (You can also use the settings there to switch to “Lean nightly”)
 
 ### Description
 
@@ -33,8 +39,8 @@ assignees: ''
 
 ### Versions
 
-[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
-[OS version]
+[Output of `#eval Lean.versionString`]
+[OS version, if not using live.lean-lang.org.]
 
 ### Additional Information
 

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
     - name: actionlint
       uses: raven-actions/actionlint@v1
       with:

.github/workflows/check-stage0.yml

@@ -0,0 +1,57 @@
+name: Check for stage0 changes
+
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-stage0-on-queue:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
+        fetch-depth: 0
+
+    - name: Find base commit
+      if: github.event_name == 'pull_request'
+      run: echo "BASE=$(git merge-base origin/${{ github.base_ref }} HEAD)" >> "$GITHUB_ENV"
+
+    - name: Identify stage0 changes
+      run: |
+        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0 |
+          grep -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in' \
+          > "$RUNNER_TEMP/stage0" || true
+        if test -s "$RUNNER_TEMP/stage0"
+        then
+          echo "CHANGES=yes" >> "$GITHUB_ENV"
+        else
+          echo "CHANGES=no" >> "$GITHUB_ENV"
+        fi
+      shell: bash
+
+    - if: github.event_name == 'pull_request'
+      name: Set label
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const { owner, repo, number: issue_number  } = context.issue;
+          if (process.env.CHANGES == 'yes') {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['changes-stage0'] }).catch(() => {});
+          } else {
+            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'changes-stage0' }).catch(() => {});
+          }
+
+    - if: env.CHANGES == 'yes'
+      name: Report changes
+      run: |
+        echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
+        # shellcheck disable=SC2129
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+        cat  "$RUNNER_TEMP/stage0"  >> "$GITHUB_STEP_SUMMARY"
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+
+    - if: github.event_name == 'merge_group' && env.CHANGES == 'yes'
+      name: Fail when on the merge queue
+      run: exit 1

.github/workflows/copyright-header.yml

@@ -10,7 +10,7 @@ jobs:
 
     - name: Verify .lean files start with a copyright header.
       run: |
-        FILES=$(find . -type d \( -path "./tests" -o -path "./doc" -o -path "./src/lake/examples" -o -path "./src/lake/tests" -o -path "./build" -o -path "./nix" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
+        FILES=$(find ./src -type d \( -path "./src/lake/examples" -o -path "./src/lake/tests" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
         if [ -n "$FILES" ]; then
           echo "Found .lean files which do not have a copyright header:"
           echo "$FILES"

.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

@@ -6,45 +6,63 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
+  # see ci.yml
+  configure:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.result }}
+    steps:
+      - name: Configure build matrix
+        id: set-matrix
+        uses: actions/github-script@v7
+        with:
+          script: |
+            let large = ${{ github.repository == 'leanprover/lean4' }};
+            let matrix = [
+              {
+                "name": "Nix Linux",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x8" : "ubuntu-latest",
+              }
+            ];
+            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
+            return matrix;
+
   Build:
+    needs: [configure]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
         shell: nix run .#ciShell -- bash -euxo pipefail {0}
     strategy:
       matrix:
-        include:
-          - name: Nix Linux
-            os: ubuntu-latest
-          #- name: Nix macOS
-          #  os: macos-latest
+        include: ${{fromJson(needs.configure.outputs.matrix)}}
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
     env:
       NIX_BUILD_ARGS: --print-build-logs --fallback
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
       - name: Set Up Nix Cache
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: nix-store-cache
           key: ${{ matrix.name }}-nix-store-cache-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-nix-store-cache
+          save-always: true
       - name: Further Set Up Nix Cache
         shell: bash -euxo pipefail {0}
         run: |
@@ -61,13 +79,14 @@ jobs:
           sudo mkdir -m0770 -p /nix/var/cache/ccache
           sudo chown -R $USER /nix/var/cache/ccache
       - name: Setup CCache Cache
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: /nix/var/cache/ccache
           key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-nix-ccache
+          save-always: true
       - name: Further Set Up CCache Cache
         run: |
           sudo chown -R root:nixbld /nix/var/cache
@@ -77,10 +96,16 @@ jobs:
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build $NIX_BUILD_ARGS .#test -o push-test
+          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
+      - name: Test Summary
+        uses: test-summary/action@v2
+        with:
+          paths: push-test/test-results.xml
+        if: always()
+        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
@@ -123,5 +148,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

.github/workflows/pr-release.yml

@@ -126,11 +126,11 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
             MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
-            if [[ -n "$STD_REMOTE_TAGS" ]]; then
-              echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+            if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
+              echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE=""
 
               if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
@@ -140,16 +140,18 @@ jobs:
                 MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
               fi
             else
-              echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
+              echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
             fi
 
           else
             echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_SHA\`."
+            git -C lean4.git fetch origin nightly-with-mathlib 
+            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
+            MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
           fi
 
           if [[ -n "$MESSAGE" ]]; then
@@ -161,7 +163,8 @@ jobs:
             # so keep in sync
 
             # Use GitHub API to check if a comment already exists
-            existing_comment="$(curl -L -s -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
+            existing_comment="$(curl --retry 3 --location --silent \
+                                    -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
                                     | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')"
@@ -221,35 +224,35 @@ jobs:
               description: description,
             });
 
-      # We next automatically create a Std branch using this toolchain.
-      # Std doesn't itself have a mechanism to report results of CI from this branch back to Lean
-      # Instead this is taken care of by Mathlib CI, which will fail if Std fails.
+      # We next automatically create a Batteries branch using this toolchain.
+      # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
+      # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
           sudo rm -rf ./*
 
-      # Checkout the Std repository with all branches
-      - name: Checkout Std repository
+      # Checkout the Batteries repository with all branches
+      - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
-          repository: leanprover/std4
+          repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_std_tag
+        id: check_batteries_tag
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
 
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'."
+            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -266,7 +269,7 @@ jobs:
           else
             echo "Branch already exists, pushing an empty commit."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
+            # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
@@ -289,13 +292,20 @@ jobs:
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: leanprover-community/mathlib4
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
 
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         id: check_mathlib_tag
@@ -319,8 +329,9 @@ jobs:
             git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
             git add lean-toolchain
-            sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
-            git add lakefile.lean
+            sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "nightly-testing-'"${MOST_RECENT_NIGHTLY}"'",' lakefile.lean
+            lake update batteries
+            git add lakefile.lean lake-manifest.json
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
             echo "Branch already exists, pushing an empty commit."