Merge branch 'main' into union-darray

.github/workflows/build.yml

@@ -54,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,46 @@
+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:
+          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,62 @@
+# 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:
+        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:
+        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:
+        labels: awaiting-review

.github/workflows/test_mathlib.yml

@@ -12,53 +12,44 @@ jobs:
     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: Retrieve information about the original workflow
-        uses: potiuk/get-workflow-origin@v1_1
-        id: workflow-info
+      - name: Checkout PR
+        uses: actions/checkout@v4
         with:
-          token: ${{ secrets.GITHUB_TOKEN }}
-          sourceRunId: ${{ github.event.workflow_run.id }}
+          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.workflow-info.outputs.pullRequestNumber != ''
+        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
+      - 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: Retrieve PR information
-        if: steps.workflow-info.outputs.pullRequestNumber != ''
-        id: pr-info
-        uses: actions/github-script@v6
-        env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-        with:
-          script: |
-            const prNumber = process.env.PR_NUMBER;
-            const { data: pr } = await github.rest.pulls.get({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              pull_number: prNumber
-            });
-            core.exportVariable('HEAD_REPO', pr.head.repo.full_name);
-            core.exportVariable('HEAD_BRANCH', pr.head.ref);
-
       - name: Check if tag exists
-        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
         id: check_mathlib_tag
         env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-          HEAD_REPO: ${{ env.HEAD_REPO }}
-          HEAD_BRANCH: ${{ env.HEAD_BRANCH }}
+          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]"
@@ -74,7 +65,7 @@ jobs:
             echo "Branch does not exist, creating it."
             git switch -c batteries-pr-testing-$PR_NUMBER "$BASE"
 
-            # Use the fork and branch name to modify the lakefile.lean
+            # 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
@@ -90,8 +81,8 @@ jobs:
           fi
 
       - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != ''
+        if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
         env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
         run: |
           git push origin batteries-pr-testing-$PR_NUMBER

Batteries.lean

@@ -32,23 +32,22 @@ 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
@@ -62,6 +61,7 @@ import Batteries.Lean.NameMapAttribute
 import Batteries.Lean.PersistentHashMap
 import Batteries.Lean.PersistentHashSet
 import Batteries.Lean.Position
+import Batteries.Lean.SatisfiesM
 import Batteries.Lean.Syntax
 import Batteries.Lean.System.IO
 import Batteries.Lean.TagAttribute
@@ -70,13 +70,12 @@ 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
@@ -94,12 +93,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.ExtendedBinder
 import Batteries.Util.LibraryNote
+import Batteries.Util.Panic
 import Batteries.Util.Pickle
 import Batteries.Util.ProofWanted
 import Batteries.WF