Trigger CI for leanprover/lean4#5145

.github/workflows/build.yml

@@ -20,7 +20,7 @@ jobs:
         name: build, test, and lint batteries
         uses: leanprover/lean-action@v1
         with:
-          build-args: '-Kwerror'
+          build-args: '--wfail'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean

.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

@@ -16,20 +16,17 @@ 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
@@ -48,9 +45,7 @@ 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.Meta.Basic
-import Batteries.Lean.Meta.Clear
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.Meta.Expr
 import Batteries.Lean.Meta.Inaccessible
@@ -76,9 +71,9 @@ 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
@@ -96,12 +91,16 @@ 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.Test.Internal.DummyLibraryNote
+import Batteries.Test.Internal.DummyLibraryNote2
 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

Batteries/Classes/SatisfiesM.lean

@@ -52,7 +52,7 @@ protected theorem trivial [Applicative m] [LawfulApplicative m] {x : m α} :
 /-- The `SatisfiesM p x` predicate is monotonic in `p`. -/
 theorem imp [Functor m] [LawfulFunctor m] {x : m α}
     (h : SatisfiesM p x) (H : ∀ {a}, p a → q a) : SatisfiesM q x :=
-  let ⟨x, h⟩ := h; ⟨(fun ⟨a, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩
+  let ⟨x, h⟩ := h; ⟨(fun ⟨_, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩
 
 /-- `SatisfiesM` distributes over `<$>`, general version. -/
 protected theorem map [Functor m] [LawfulFunctor m] {x : m α}
@@ -171,12 +171,12 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
   · refine ⟨fun s => (fun ⟨⟨a, h⟩, s'⟩ => ⟨⟨a, s'⟩, h⟩) <$> f s, fun s => ?_⟩
     rw [← comp_map, map_eq_pure_bind]; rfl
   · refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
-    show _ >>= _ = _; simp [map_eq_pure_bind, ← h]
+    show _ >>= _ = _; simp [← h]
 
 @[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
     SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x := by
   refine ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, eq⟩ => eq ▸ ?_⟩
   · exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, nofun⟩) <$> f
     show _ = _ >>= _; rw [← comp_map, map_eq_pure_bind]; congr; funext a; cases a <;> rfl
   · exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)
-    show _ >>= _ = _; simp [← comp_map, map_eq_pure_bind]; congr; funext ⟨a, h⟩; cases a <;> rfl
+    show _ >>= _ = _; simp [← comp_map, ← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl

Batteries/CodeAction/Attr.lean

@@ -14,7 +14,7 @@ import Lean.Server.CodeActions.Basic
 * Attribute `@[tactic_code_action]` collects code actions which will be called
   on each occurrence of a tactic.
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Elab Server Lsp RequestM Snapshots
 

Batteries/CodeAction/Basic.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
 import Lean.Server.InfoUtils
+import Lean.Server.CodeActions.Provider
 import Batteries.CodeAction.Attr
 
 /-!
@@ -18,131 +19,9 @@ on each occurrence of a hole (`_`, `?_` or `sorry`).
 attempt to use this code action provider when browsing the `Batteries.CodeAction.Hole.Attr` file
 itself.)
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
-open Lean Elab Term Server RequestM
-
-/--
-The return value of `findTactic?`.
-This is the syntax for which code actions will be triggered.
--/
-inductive FindTacticResult
-  /-- The nearest enclosing tactic is a tactic, with the given syntax stack. -/
-  | tactic : Syntax.Stack → FindTacticResult
-  /-- The cursor is between tactics, and the nearest enclosing range is a tactic sequence.
-  Code actions will insert tactics at index `insertIdx` into the syntax
-  (which is a nullNode of `tactic;*` inside a `tacticSeqBracketed` or `tacticSeq1Indented`). -/
-  | tacticSeq : (preferred : Bool) → (insertIdx : Nat) → Syntax.Stack → FindTacticResult
-
-/--
-Find the syntax on which to trigger tactic code actions.
-This is a pure syntax pass, without regard to elaboration information.
-
-* `preferred : String.Pos → Bool`: used to select "preferred `tacticSeq`s" based on the cursor
-  column, when the cursor selection would otherwise be ambiguous. For example, in:
-  ```
-  · foo
-    · bar
-      baz
-    |
-  ```
-  where the cursor is at the `|`, we select the `tacticSeq` starting with `foo`, while if the
-  cursor was indented to align with `baz` then we would select the `bar; baz` sequence instead.
-
-* `range`: the cursor selection. We do not do much with range selections; if a range selection
-  covers more than one tactic then we abort.
-
-* `root`: the root syntax to process
-
-The return value is either a selected tactic, or a selected point in a tactic sequence.
--/
-partial def findTactic? (preferred : String.Pos → Bool) (range : String.Range)
-    (root : Syntax) : Option FindTacticResult := do _ ← visit root; ← go [] root
-where
-  /-- Returns `none` if we should not visit this syntax at all, and `some false` if we only
-  want to visit it in "extended" mode (where we include trailing characters). -/
-  visit (stx : Syntax) (prev? : Option String.Pos := none) : Option Bool := do
-    let left ← stx.getPos? true
-    guard <| prev?.getD left ≤ range.start
-    let .original (endPos := right) (trailing := trailing) .. := stx.getTailInfo | none
-    guard <| right.byteIdx + trailing.bsize ≥ range.stop.byteIdx
-    return left ≤ range.start && right ≥ range.stop
-
-  /-- Merges the results of two `FindTacticResult`s. This just prefers the second (inner) one,
-  unless the inner tactic is a dispreferred tactic sequence and the outer one is preferred.
-  This is used to implement whitespace-sensitive selection of tactic sequences. -/
-  merge : (r₁ : Option FindTacticResult) → (r₂ : FindTacticResult) → FindTacticResult
-  | some r₁@(.tacticSeq (preferred := true) ..), .tacticSeq (preferred := false) .. => r₁
-  | _, r₂ => r₂
-
-  /-- Main recursion for `findTactic?`. This takes a `stack` context and a root syntax `stx`,
-  and returns the best `FindTacticResult` it can find. It returns `none` (abort) if two or more
-  results are found, and `some none` (none yet) if no results are found. -/
-  go (stack : Syntax.Stack) (stx : Syntax) (prev? : Option String.Pos := none) :
-      Option (Option FindTacticResult) := do
-    if stx.getKind == ``Parser.Tactic.tacticSeq then
-      -- TODO: this implementation is a bit too strict about the beginning of tacticSeqs.
-      -- We would like to be able to parse
-      -- · |
-      --   foo
-      -- (where `|` is the cursor position) as an insertion into the sequence containing foo
-      -- at index 0, but we currently use the start of the tacticSeq, which is the foo token,
-      -- as the earliest possible location that will be associated to the sequence.
-      let bracket := stx[0].getKind == ``Parser.Tactic.tacticSeqBracketed
-      let argIdx := if bracket then 1 else 0
-      let (stack, stx) := ((stx[0], argIdx) :: (stx, 0) :: stack, stx[0][argIdx])
-      let mainRes := stx[0].getPos?.map fun pos =>
-        let i := Id.run do
-          for i in [0:stx.getNumArgs] do
-            if let some pos' := stx[2*i].getPos? then
-              if range.stop < pos' then
-                return i
-          (stx.getNumArgs + 1) / 2
-        .tacticSeq (bracket || preferred pos) i ((stx, 0) :: stack)
-      let mut childRes := none
-      for i in [0:stx.getNumArgs:2] do
-        if let some inner := visit stx[i] then
-          let stack := (stx, i) :: stack
-          if let some child := (← go stack stx[i]) <|>
-            (if inner then some (.tactic ((stx[i], 0) :: stack)) else none)
-          then
-            if childRes.isSome then failure
-            childRes := merge mainRes child
-      return childRes <|> mainRes
-    else
-      let mut childRes := none
-      let mut prev? := prev?
-      for i in [0:stx.getNumArgs] do
-        if let some _ := visit stx[i] prev? then
-          if let some child ← go ((stx, i) :: stack) stx[i] prev? then
-            if childRes.isSome then failure
-            childRes := child
-        prev? := stx[i].getTailPos? true <|> prev?
-      return childRes
-
-/--
-Returns the info tree corresponding to a syntax, using `kind` and `range` for identification.
-(This is not foolproof, but it is a fairly accurate proxy for `Syntax` equality and a lot cheaper
-than deep comparison.)
--/
-partial def findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range)
-  (ctx? : Option ContextInfo) (t : InfoTree)
-  (f : ContextInfo → Info → Bool) (canonicalOnly := false) :
-    Option (ContextInfo × InfoTree) :=
-  match t with
-  | .context ctx t => findInfoTree? kind tgtRange (ctx.mergeIntoOuter? ctx?) t f canonicalOnly
-  | node@(.node i ts) => do
-    if let some ctx := ctx? then
-      if let some range := i.stx.getRange? canonicalOnly then
-        -- FIXME: info tree needs to be organized better so that this works
-        -- guard <| range.includes tgtRange
-        if i.stx.getKind == kind && range == tgtRange && f ctx i then
-          return (ctx, node)
-    for t in ts do
-      if let some res := findInfoTree? kind tgtRange (i.updateContext? ctx?) t f canonicalOnly then
-        return res
-    none
-  | _ => none
+open Lean Elab Server RequestM CodeAction
 
 /-- A code action which calls `@[tactic_code_action]` code actions. -/
 @[code_action_provider] def tacticCodeActionProvider : CodeActionProvider := fun params snap => do

Batteries/CodeAction/Deprecated.lean

@@ -14,8 +14,10 @@ This is an opt-in mechanism for making machine-applicable `@[deprecated]` defini
 whenever the deprecation lint also fires, allowing the user to replace the usage of the deprecated
 constant.
 -/
-namespace Std
-open Lean Elab Server Lsp RequestM
+
+namespace Batteries
+
+open Lean Elab Server Lsp RequestM CodeAction
 
 /-- An environment extension for identifying `@[deprecated]` definitions which can be auto-fixed -/
 initialize machineApplicableDeprecated : TagDeclarationExtension ← mkTagDeclarationExtension

Batteries/CodeAction/Misc.lean

@@ -15,7 +15,7 @@ import Lean.Server.CodeActions.Provider
 
 This declares some basic tactic code actions, using the `@[tactic_code_action]` API.
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Meta Elab Server RequestM CodeAction
 

Batteries/Data/Array.lean

@@ -4,3 +4,5 @@ import Batteries.Data.Array.Lemmas
 import Batteries.Data.Array.Match
 import Batteries.Data.Array.Merge
 import Batteries.Data.Array.Monadic
+import Batteries.Data.Array.OfFn
+import Batteries.Data.Array.Pairwise