Merge branch 'main' into binaryRec

.github/workflows/build.yml

@@ -18,10 +18,9 @@ jobs:
 
       - id: lean-action
         name: build, test, and lint batteries
-        uses: leanprover/lean-action@v1-beta
+        uses: leanprover/lean-action@v1
         with:
-          build-args: '-Kwerror'
-          lint-module: 'Batteries'
+          build-args: '--wfail'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean
@@ -55,4 +54,4 @@ jobs:
       - name: Don't 'import Lean', use precise imports
         if: always()
         run: |
-          ! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+          ! (find . -name "*.lean" ! -path "./BatteriesTest/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')

.github/workflows/docs-deploy.yml

@@ -0,0 +1,38 @@
+name: Deploy Docs
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 10 * * *' # daily (UTC 10:00)
+
+permissions:
+  contents: write
+
+jobs:
+  deploy-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build -q Batteries:docs
+
+      - name: Deploy Docs
+        run: |
+          git config user.name "leanprover-community-batteries-bot"
+          git config user.email "[email protected]"
+          git checkout -b docs
+          git add docs/doc docs/doc-data
+          git commit -m "chore: generate docs"
+          git push origin docs --force

.github/workflows/docs-release.yml

@@ -0,0 +1,48 @@
+name: Release Docs
+
+on:
+  push:
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+      - "v[0-9]+.[0-9]+.[0-9]+-rc[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  build-docs:
+    runs-on: ubuntu-latest
+    if: github.repository_owner == 'leanprover-community'
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Docs
+        working-directory: docs
+        run: lake build -q Batteries:docs
+
+      - name: Compress Docs
+        working-directory: docs
+        env:
+          TAG_NAME: ${{ github.ref_name }}
+        run: |
+          tar -czf docs-${TAG_NAME}.tar.gz doc doc-data
+          zip -rq docs-${TAG_NAME}.zip doc doc-data
+
+      - 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
+          fail_on_unmatched_files: true

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

@@ -0,0 +1,65 @@
+# This workflow assigns `awaiting-review` or `WIP` labels to new PRs, and it removes
+# `awaiting-review`, `awaiting-author`, or `WIP` label from closed PRs.
+# It does not modify labels for open PRs that already have one of the `awaiting-review`,
+# `awaiting-author`, or `WIP` labels.
+
+name: Label PR from status change
+
+permissions:
+  contents: read
+  pull-requests: write
+
+on:
+  pull_request:
+    types:
+      - closed
+      - opened
+      - reopened
+      - converted_to_draft
+      - ready_for_review
+    branches:
+      - main
+
+jobs:
+  auto-label:
+    if: github.repository_owner == 'leanprover-community'
+    runs-on: ubuntu-latest
+    steps:
+
+    - uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+
+    - name: Unlabel closed PR
+      if: github.event.pull_request.state == 'closed'
+      uses: actions-ecosystem/action-remove-labels@v1
+      with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+        labels: |
+          WIP
+          awaiting-author
+          awaiting-review
+
+    - name: Label unlabeled draft PR as WIP
+      if: |
+        github.event.pull_request.state == 'open' &&
+        github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! 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
+      if: |
+        github.event.pull_request.state == 'open' &&
+        ! github.event.pull_request.draft &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-author') &&
+        ! contains(github.event.pull_request.labels.*.name, 'awaiting-review') &&
+        ! 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

@@ -24,7 +24,7 @@ jobs:
         type: 'stream'
         topic: 'Batteries status updates'
         content: |
-          ❌ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
+          ❌️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
 
   # Whenever `nightly-testing` passes CI,
   # push it to `nightly-testing-YYYY-MM-DD` so we have a known good version of Batteries on that nightly release.
@@ -77,13 +77,13 @@ jobs:
         }
         response = client.get_messages(request)
         messages = response['messages']
-        if not messages or messages[0]['content'] != "✅ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!":
+        if not messages or messages[0]['content'] != "✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!":
             # Post the success message
             request = {
                 'type': 'stream',
                 'to': 'nightly-testing',
                 'topic': 'Batteries status updates',
-                'content': "✅ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!"
+                'content': "✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!"
             }
             result = client.send_message(request)
             print(result)

.github/workflows/test_mathlib.yml

@@ -0,0 +1,88 @@
+# Test Mathlib against a Batteries PR
+
+name: Test Mathlib
+
+on:
+  workflow_run:
+    workflows: [ci]
+    types: [completed]
+
+jobs:
+  on-success:
+    runs-on: ubuntu-latest
+    if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover-community/batteries'
+    steps:
+      - name: Checkout PR
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Get PR info
+        id: pr-info
+        run: |
+          echo "pullRequestNumber=$(gh pr list --search $SHA --json number -q '.[0].number' || echo '')" >> $GITHUB_OUTPUT
+          echo "targetBranch=$(gh pr list --search $SHA --json baseRefName -q '.[0].baseRefName' || echo '')" >> $GITHUB_OUTPUT
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          SHA: ${{ github.event.workflow_run.head_sha }}
+
+      - name: Checkout mathlib4 repository
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
+        uses: actions/checkout@v4
+        with:
+          repository: leanprover-community/mathlib4
+          token: ${{ secrets.MATHLIB4_BOT }}
+          ref: master
+          fetch-depth: 0
+
+      - name: Install elan
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
+        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.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
+        id: check_mathlib_tag
+        env:
+          PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
+          HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+        run: |
+          git config user.name "leanprover-community-mathlib4-bot"
+          git config user.email "[email protected]"
+
+          echo "PR info: $HEAD_REPO $HEAD_BRANCH"
+
+          BASE=master
+          echo "Using base tag: $BASE"
+
+          EXISTS="$(git ls-remote --heads origin batteries-pr-testing-$PR_NUMBER | wc -l)"
+          echo "Branch exists: $EXISTS"
+          if [ "$EXISTS" = "0" ]; then
+            echo "Branch does not exist, creating it."
+            git switch -c batteries-pr-testing-$PR_NUMBER "$BASE"
+
+            # Modify the lakefile.lean with the fork and branch name
+            sed -i "s,require \"leanprover-community\" / \"batteries\" @ git \".\+\",require \"leanprover-community\" / \"batteries\" from git \"https://github.com/$HEAD_REPO\" @ \"$HEAD_BRANCH\",g" lakefile.lean
+
+            lake update batteries
+            git add lakefile.lean lake-manifest.json
+            git commit -m "Update Batteries branch for testing https://github.com/leanprover-community/batteries/pull/$PR_NUMBER"
+          else
+            echo "Branch already exists, merging $BASE and bumping Batteries."
+            git switch batteries-pr-testing-$PR_NUMBER
+            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
+            lake update batteries
+            git add lake-manifest.json
+            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover-community/batteries/pull/$PR_NUMBER"
+          fi
+
+      - name: Push changes
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
+        env:
+          PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
+        run: |
+          git push origin batteries-pr-testing-$PR_NUMBER

.gitpod.yml

@@ -4,3 +4,8 @@ image:
 vscode:
   extensions:
     - leanprover.lean4
+
+tasks:
+  - init: |
+      elan self update
+      lake build

Batteries.lean

@@ -1,4 +1,3 @@
-import Batteries.Classes.BEq
 import Batteries.Classes.Cast
 import Batteries.Classes.Order
 import Batteries.Classes.RatCast
@@ -15,40 +14,39 @@ import Batteries.Control.Lemmas
 import Batteries.Control.Nondet.Basic
 import Batteries.Data.Array
 import Batteries.Data.AssocList
+import Batteries.Data.BinaryHeap
 import Batteries.Data.BinomialHeap
-import Batteries.Data.BitVec
-import Batteries.Data.Bool
 import Batteries.Data.ByteArray
+import Batteries.Data.ByteSubarray
 import Batteries.Data.Char
 import Batteries.Data.DList
 import Batteries.Data.Fin
+import Batteries.Data.FloatArray
 import Batteries.Data.HashMap
-import Batteries.Data.Int
 import Batteries.Data.LazyList
 import Batteries.Data.List
 import Batteries.Data.MLList
 import Batteries.Data.Nat
-import Batteries.Data.Option
 import Batteries.Data.PairingHeap
 import Batteries.Data.RBMap
 import Batteries.Data.Range
 import Batteries.Data.Rat
+import Batteries.Data.Stream
 import Batteries.Data.String
-import Batteries.Data.Sum
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
+import Batteries.Data.Vector
 import Batteries.Lean.AttributeExtra
-import Batteries.Lean.Delaborator
+import Batteries.Lean.EStateM
 import Batteries.Lean.Except
 import Batteries.Lean.Expr
 import Batteries.Lean.Float
 import Batteries.Lean.HashMap
 import Batteries.Lean.HashSet
 import Batteries.Lean.IO.Process
 import Batteries.Lean.Json
-import Batteries.Lean.Meta.AssertHypotheses
+import Batteries.Lean.LawfulMonad
 import Batteries.Lean.Meta.Basic
-import Batteries.Lean.Meta.Clear
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.Meta.Expr
 import Batteries.Lean.Meta.Inaccessible
@@ -57,31 +55,29 @@ import Batteries.Lean.Meta.SavedState
 import Batteries.Lean.Meta.Simp
 import Batteries.Lean.Meta.UnusedNames
 import Batteries.Lean.MonadBacktrack
-import Batteries.Lean.Name
 import Batteries.Lean.NameMap
 import Batteries.Lean.NameMapAttribute
 import Batteries.Lean.PersistentHashMap
 import Batteries.Lean.PersistentHashSet
 import Batteries.Lean.Position
-import Batteries.Lean.SMap
+import Batteries.Lean.SatisfiesM
 import Batteries.Lean.Syntax
 import Batteries.Lean.System.IO
 import Batteries.Lean.TagAttribute
 import Batteries.Lean.Util.EnvSearch
-import Batteries.Lean.Util.Path
 import Batteries.Linter
 import Batteries.Linter.UnnecessarySeqFocus
 import Batteries.Linter.UnreachableTactic
 import Batteries.Logic
-import Batteries.StdDeprecations
 import Batteries.Tactic.Alias
 import Batteries.Tactic.Basic
 import Batteries.Tactic.Case
-import Batteries.Tactic.Classical
 import Batteries.Tactic.Congr
 import Batteries.Tactic.Exact
+import Batteries.Tactic.HelpCmd
 import Batteries.Tactic.Init
 import Batteries.Tactic.Instances
+import Batteries.Tactic.Lemma
 import Batteries.Tactic.Lint
 import Batteries.Tactic.Lint.Basic
 import Batteries.Tactic.Lint.Frontend
@@ -96,13 +92,13 @@ 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.Test.Internal.DummyLabelAttr
 import Batteries.Util.Cache
-import Batteries.Util.CheckTactic
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote
+import Batteries.Util.Panic
 import Batteries.Util.Pickle
 import Batteries.Util.ProofWanted
 import Batteries.WF