Trigger CI for leanprover/lean4#5145

.github/workflows/build.yml

@@ -9,6 +9,10 @@ on:
 
 name: ci
 
+concurrency:
+  group: build-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   build:
     name: Build

.github/workflows/docs-deploy.yml

@@ -26,7 +26,7 @@ jobs:
 
       - name: Build Docs
         working-directory: docs
-        run: lake build -q Batteries:docs
+        run: lake build --keep-toolchain -q Batteries:docs
 
       - name: Deploy Docs
         run: |

.github/workflows/docs-release.yml

@@ -27,7 +27,7 @@ jobs:
 
       - name: Build Docs
         working-directory: docs
-        run: lake build -q Batteries:docs
+        run: lake build --keep-toolchain -q Batteries:docs
 
       - name: Compress Docs
         working-directory: docs
@@ -40,6 +40,8 @@ jobs:
       - name: Release Docs
         uses: softprops/action-gh-release@v2
         with:
+          prerelease: ${{ contains(github.ref, 'rc') }}
+          make_latest: ${{ !contains(github.ref, 'rc') }}
           files: |
             docs/docs-${{ github.ref_name }}.tar.gz
             docs/docs-${{ github.ref_name }}.zip

.github/workflows/labels-from-status.yml

@@ -34,6 +34,7 @@ jobs:
       if: github.event.pull_request.state == 'closed'
       uses: actions-ecosystem/action-remove-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: |
           WIP
           awaiting-author
@@ -48,6 +49,7 @@ jobs:
         ! contains(github.event.pull_request.labels.*.name, 'WIP')
       uses: actions-ecosystem/action-add-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: WIP
 
     - name: Label unlabeled other PR as awaiting-review
@@ -59,4 +61,5 @@ jobs:
         ! contains(github.event.pull_request.labels.*.name, 'WIP')
       uses: actions-ecosystem/action-add-labels@v1
       with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
         labels: awaiting-review

.github/workflows/nightly_detect_failure.yml

@@ -88,3 +88,120 @@ jobs:
             result = client.send_message(request)
             print(result)
       shell: python
+
+    # Next, determine if we should remind the humans to create a new PR to the `bump/v4.X.0` branch.
+
+    - name: Check for matching bump/nightly-YYYY-MM-DD branch
+      id: check_branch
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const branchName = `bump/nightly-${process.env.NIGHTLY}`;
+          const branches = await github.rest.repos.listBranches({
+            owner: context.repo.owner,
+            repo: context.repo.repo
+          });
+          const exists = branches.data.some(branch => branch.name === branchName);
+          if (exists) {
+            console.log(`Branch ${branchName} exists.`);
+            return true;
+          } else {
+            console.log(`Branch ${branchName} does not exist.`);
+            return false;
+          }
+        result-encoding: string
+
+    - name: Exit if matching branch exists
+      if: steps.check_branch.outputs.result == 'true'
+      run: |
+        echo "Matching bump/nightly-YYYY-MM-DD branch found, no further action needed."
+        exit 0
+
+    - name: Fetch latest bump branch name
+      id: latest_bump_branch
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const branches = await github.paginate(github.rest.repos.listBranches, {
+            owner: context.repo.owner,
+            repo: context.repo.repo
+          });
+          const bumpBranches = branches
+            .map(branch => branch.name)
+            .filter(name => name.match(/^bump\/v4\.\d+\.0$/))
+            .sort((a, b) => b.localeCompare(a, undefined, {numeric: true, sensitivity: 'base'}));
+          if (!bumpBranches.length) {
+            throw new Exception("Did not find any bump/v4.x.0 branch")
+          }
+          const latestBranch = bumpBranches[0];
+          return latestBranch;
+
+    - name: Fetch lean-toolchain from latest bump branch
+      id: bump_version
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const response = await github.rest.repos.getContent({
+            owner: context.repo.owner,
+            repo: context.repo.repo,
+            path: 'lean-toolchain',
+            ref: ${{ steps.latest_bump_branch.outputs.result }}
+          });
+          const content = Buffer.from(response.data.content, 'base64').toString();
+          const version = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/)[1];
+          return version;
+
+    - name: Compare versions and post a reminder.
+      env:
+        BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
+        BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
+        SHA: ${{ env.SHA }}
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+      shell: python
+      run: |
+        import os
+        import zulip
+        client = zulip.Client(email='[email protected]', api_key=os.getenv('ZULIP_API_KEY'), site='https://leanprover.zulipchat.com')
+        current_version = os.getenv('NIGHTLY')
+        bump_version = os.getenv('BUMP_VERSION')
+        bump_branch = os.getenv('BUMP_BRANCH')
+        sha = os.getenv('SHA')
+        print(f'Current version: {current_version}, Bump version: {bump_version}, SHA: {sha}')
+        if current_version > bump_version:
+            print('Lean toolchain in `nightly-testing` is ahead of the bump branch.')
+            # Get the last message in the 'Batteries bump branch reminders' topic
+            request = {
+              'anchor': 'newest',
+              'num_before': 1,
+              'num_after': 0,
+              'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Batteries bump branch reminders'}],
+              'apply_markdown': False    # Otherwise the content test below fails.
+            }
+            response = client.get_messages(request)
+            messages = response['messages']
+            bump_branch_suffix = bump_branch.replace('bump/', '')
+            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
+            payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
+            payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
+            # Only post if the message is different
+            # We compare the first 160 characters, since that includes the date and bump version
+            if not messages or messages[0]['content'][:160] != payload[:160]:
+                # Log messages, because the bot seems to repeat itself...
+                if messages:
+                    print("###### Last message:")
+                    print(messages[0]['content'])
+                    print("###### Current message:")
+                    print(payload)
+                else:
+                    print('The strings match!')
+                # Post the reminder message
+                request = {
+                    'type': 'stream',
+                    'to': 'nightly-testing',
+                    'topic': 'Batteries bump branch reminders',
+                    'content': payload
+                }
+                result = client.send_message(request)
+                print(result)
+        else:
+            print('No action needed.')

Batteries.lean

@@ -26,9 +26,11 @@ import Batteries.Data.HashMap
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList
+import Batteries.Data.NameSet
 import Batteries.Data.Nat
 import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
+import Batteries.Data.Random
 import Batteries.Data.Range
 import Batteries.Data.Rat
 import Batteries.Data.Stream
@@ -87,13 +89,13 @@ import Batteries.Tactic.NoMatch
 import Batteries.Tactic.OpenPrivate
 import Batteries.Tactic.PermuteGoals
 import Batteries.Tactic.PrintDependents
+import Batteries.Tactic.PrintOpaques
 import Batteries.Tactic.PrintPrefix
 import Batteries.Tactic.SeqFocus
 import Batteries.Tactic.ShowUnused
 import Batteries.Tactic.SqueezeScope
 import Batteries.Tactic.Trans
 import Batteries.Tactic.Unreachable
-import Batteries.Tactic.Where
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote

Batteries/Data/Array/Basic.lean

@@ -137,43 +137,11 @@ This will perform the update destructively provided that `a` has a reference cou
 abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
   a.set i x
 
-/--
-`swapN a i j hi hj` swaps two `Nat` indexed entries in an `Array α`.
-Uses `get_elem_tactic` to supply a proof that the indices are in range.
-`hi` and `hj` are both given a default argument `by get_elem_tactic`.
-This will perform the update destructively provided that `a` has a reference count of 1 when called.
--/
-abbrev swapN (a : Array α) (i j : Nat)
-    (hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α :=
-  Array.swap a ⟨i,hi⟩ ⟨j, hj⟩
+@[deprecated (since := "2024-11-24")] alias swapN := swap
 
-/--
-`swapAtN a i h x` swaps the entry with index `i : Nat` in the vector for a new entry `x`.
-The old entry is returned alongwith the modified vector.
-Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible.
--/
-abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
-    α × Array α := swapAt a ⟨i,h⟩ x
+@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt
 
-/--
-`eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`.
-`h : i < a.size` has a default argument `by get_elem_tactic` which tries to supply a proof
-that the index is valid.
-This function takes worst case O(n) time because it has to backshift all elements at positions
-greater than i.
--/
-abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
-  a.feraseIdx ⟨i, h⟩
-
-/--
-Remove the element at a given index from an array, panics if index is out of bounds.
--/
-def eraseIdx! (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then
-    a.feraseIdx ⟨i, h⟩
-  else
-    have : Inhabited (Array α) := ⟨a⟩
-    panic! s!"index {i} out of bounds"
+@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx
 
 end Array