Trigger CI for leanprover/lean4#4061

.docker/gitpod/Dockerfile

@@ -1,4 +1,4 @@
-# This is the Dockerfile for leanprover/std4
+# This is the Dockerfile for leanprover-community/batteries
 # This file is mostly copied from [mathlib4](https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile)
 
 # gitpod doesn't support multiple FROM statements, (or rather, you can't copy from one to another)
@@ -23,8 +23,8 @@ RUN { echo && echo "PS1='\[\033[01;32m\]\u\[\033[00m\] \[\033[01;34m\]\w\[\033[0
 # install elan
 RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
 
-# install whichever toolchain std4 is currently using
-RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover/std4/main/lean-toolchain)
+# install whichever toolchain batteries is currently using
+RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/batteries/main/lean-toolchain)
 
 # install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
 RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvim

.github/workflows/build.yml

@@ -23,15 +23,15 @@ jobs:
 
       - uses: actions/checkout@v4
 
-      - name: build std
+      - name: build batteries
         id: build
         run: lake build -Kwerror
 
-      - name: test std
+      - name: test batteries
         if: steps.build.outcome == 'success'
         run: make test
 
-      - name: lint std
+      - name: lint batteries
         if: steps.build.outcome == 'success'
         run: make lint
 
@@ -57,7 +57,7 @@ jobs:
       - name: Check for long lines
         if: always()
         run: |
-          ! (find Std -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+          ! (find Batteries -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
 
       - name: Check for trailing whitespace
         if: always()

.github/workflows/merge_conflicts.yml

@@ -6,7 +6,7 @@ on:
 
 jobs:
   main:
-    if: github.repository_owner == 'leanprover'
+    if: github.repository_owner == 'leanprover-community'
     runs-on: ubuntu-latest
     steps:
       - name: check if prs are dirty

.github/workflows/nightly_bump_toolchain.yml

@@ -8,7 +8,7 @@ on:
 
 jobs:
   update-toolchain:
-    if: github.repository_owner == 'leanprover'
+    if: github.repository_owner == 'leanprover-community'
     runs-on: ubuntu-latest
 
     steps:

.github/workflows/nightly_detect_failure.yml

@@ -22,12 +22,12 @@ jobs:
         organization-url: 'https://leanprover.zulipchat.com'
         to: 'nightly-testing'
         type: 'stream'
-        topic: 'Std status updates'
+        topic: 'Batteries status updates'
         content: |
-          ❌ The latest CI for Std's [`nightly-testing`](https://github.com/leanprover/std4/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 Std on that nightly release.
+  # push it to `nightly-testing-YYYY-MM-DD` so we have a known good version of Batteries on that nightly release.
   handle_success:
     if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
     runs-on: ubuntu-latest
@@ -72,18 +72,18 @@ jobs:
           'anchor': 'newest',
           'num_before': 1,
           'num_after': 0,
-          'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Std status updates'}],
+          'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Batteries status updates'}],
           'apply_markdown': False
         }
         response = client.get_messages(request)
         messages = response['messages']
-        if not messages or messages[0]['content'] != "✅ The latest CI for Std's [`nightly-testing`](https://github.com/leanprover/std4/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': 'Std status updates',
-                'content': "✅ The latest CI for Std's [`nightly-testing`](https://github.com/leanprover/std4/tree/nightly-testing) branch has succeeded!"
+                'topic': 'Batteries status updates',
+                '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/nightly_merge_master.yml

@@ -9,7 +9,7 @@ on:
 
 jobs:
   merge-to-nightly:
-    if: github.repository_owner == 'leanprover'
+    if: github.repository_owner == 'leanprover-community'
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository

.vscode/copyright.code-snippets

@@ -1,5 +1,5 @@
 {
-	"Copyright header for std": {
+	"Copyright header for batteries": {
 		"scope": "lean4",
 		"prefix": "copyright",
 		"body": [

Batteries.lean

@@ -0,0 +1,108 @@
+import Batteries.Classes.BEq
+import Batteries.Classes.Cast
+import Batteries.Classes.Order
+import Batteries.Classes.RatCast
+import Batteries.Classes.SatisfiesM
+import Batteries.CodeAction
+import Batteries.CodeAction.Attr
+import Batteries.CodeAction.Basic
+import Batteries.CodeAction.Deprecated
+import Batteries.CodeAction.Misc
+import Batteries.Control.ForInStep
+import Batteries.Control.ForInStep.Basic
+import Batteries.Control.ForInStep.Lemmas
+import Batteries.Control.Lemmas
+import Batteries.Control.Nondet.Basic
+import Batteries.Data.Array
+import Batteries.Data.AssocList
+import Batteries.Data.BinomialHeap
+import Batteries.Data.BitVec
+import Batteries.Data.Bool
+import Batteries.Data.ByteArray
+import Batteries.Data.Char
+import Batteries.Data.DList
+import Batteries.Data.Fin
+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.String
+import Batteries.Data.Sum
+import Batteries.Data.UInt
+import Batteries.Data.UnionFind
+import Batteries.Lean.AttributeExtra
+import Batteries.Lean.Delaborator
+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.Meta.Basic
+import Batteries.Lean.Meta.Clear
+import Batteries.Lean.Meta.DiscrTree
+import Batteries.Lean.Meta.Expr
+import Batteries.Lean.Meta.Inaccessible
+import Batteries.Lean.Meta.InstantiateMVars
+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.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.Init
+import Batteries.Tactic.Instances
+import Batteries.Tactic.Lint
+import Batteries.Tactic.Lint.Basic
+import Batteries.Tactic.Lint.Frontend
+import Batteries.Tactic.Lint.Misc
+import Batteries.Tactic.Lint.Simp
+import Batteries.Tactic.Lint.TypeClass
+import Batteries.Tactic.NoMatch
+import Batteries.Tactic.OpenPrivate
+import Batteries.Tactic.PermuteGoals
+import Batteries.Tactic.PrintDependents
+import Batteries.Tactic.PrintPrefix
+import Batteries.Tactic.SeqFocus
+import Batteries.Tactic.ShowUnused
+import Batteries.Tactic.SqueezeScope
+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.Pickle
+import Batteries.Util.ProofWanted
+import Batteries.WF

Std/Classes/Cast.lean → Batteries/Classes/Cast.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
-import Std.Util.LibraryNote
+import Batteries.Util.LibraryNote
 
 library_note "coercion into rings"
 /--

Std/Classes/Order.lean → Batteries/Classes/Order.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Std.Tactic.SeqFocus
+import Batteries.Tactic.SeqFocus
 
 /-! ## Ordering -/
 
@@ -28,7 +28,7 @@ theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt ↔ o₁ = gt 
 
 end Ordering
 
-namespace Std
+namespace Batteries
 
 /-- `TotalBLE le` asserts that `le` has a total order, that is, `le a b ∨ le b a`. -/
 class TotalBLE (le : α → α → Bool) : Prop where
@@ -134,7 +134,7 @@ class LECmp [LE α] (cmp : α → α → Ordering) extends OrientedCmp cmp : Pro
   /-- `cmp x y ≠ .gt` holds iff `x ≤ y` is true. -/
   cmp_iff_le : cmp x y ≠ .gt ↔ x ≤ y
 
-theorem LTCmp.cmp_iff_ge [LE α] [LECmp (α := α) cmp] : cmp x y ≠ .lt ↔ y ≤ x := by
+theorem LECmp.cmp_iff_ge [LE α] [LECmp (α := α) cmp] : cmp x y ≠ .lt ↔ y ≤ x := by
   rw [← OrientedCmp.cmp_ne_gt, LECmp.cmp_iff_le]
 
 /-- `LawfulCmp cmp` asserts that the `LE`, `LT`, `BEq` instances are all coherent with each other
@@ -354,11 +354,11 @@ instance : LawfulOrd Bool where
 instance : LawfulOrd Int := .compareOfLessAndEq
   Int.lt_irrefl Int.lt_trans Int.not_lt Int.le_antisymm
 
-end Std
+end Batteries
 
 namespace Ordering
 
-open Std
+open Batteries
 
 /-- Pull back a comparator by a function `f`, by applying the comparator to both arguments. -/
 @[inline] def byKey (f : α → β) (cmp : β → β → Ordering) (a b : α) : Ordering := cmp (f a) (f b)

Std/Classes/RatCast.lean → Batteries/Classes/RatCast.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro, Gabriel Ebner
 -/
-import Std.Data.Rat.Basic
+import Batteries.Data.Rat.Basic
 
 /-- Type class for the canonical homomorphism `Rat → K`. -/
 class RatCast (K : Type u) where

Std/Classes/SatisfiesM.lean → Batteries/Classes/SatisfiesM.lean

@@ -23,8 +23,8 @@ presumably requiring more syntactic support (and smarter `do` blocks) from Lean.
 Or it may be that such a solution will look different!
 This is an open research program, and for now one should not be overly ambitious using `SatisfiesM`.
 
-In particular lemmas about pure operations on data structures in `Std` except for `HashMap` should
-avoid `SatisfiesM` for now, so that it is easy to migrate to other approaches in future.
+In particular lemmas about pure operations on data structures in `batteries` except for `HashMap`
+should avoid `SatisfiesM` for now, so that it is easy to migrate to other approaches in future.
 -/
 
 /--

Batteries/CodeAction.lean

@@ -0,0 +1,3 @@
+import Batteries.CodeAction.Attr
+import Batteries.CodeAction.Basic
+import Batteries.CodeAction.Misc

Std/CodeAction/Basic.lean → Batteries/CodeAction/Basic.lean

@@ -6,16 +6,17 @@ Authors: Mario Carneiro
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
 import Lean.Server.InfoUtils
-import Std.CodeAction.Attr
+import Batteries.CodeAction.Attr
 
 /-!
 # Initial setup for code actions
 
 This declares a code action provider that calls all `@[hole_code_action]` definitions
 on each occurrence of a hole (`_`, `?_` or `sorry`).
 
-(This is in a separate file from `Std.CodeAction.Hole.Attr` so that the server does not attempt
-to use this code action provider when browsing the `Std.CodeAction.Hole.Attr` file itself.)
+(This is in a separate file from `Batteries.CodeAction.Hole.Attr` so that the server does not
+attempt to use this code action provider when browsing the `Batteries.CodeAction.Hole.Attr` file
+itself.)
 -/
 namespace Std.CodeAction
 

Std/CodeAction/Deprecated.lean → Batteries/CodeAction/Deprecated.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Lean.Server.CodeActions
-import Std.CodeAction.Basic
-import Std.Lean.Position
+import Batteries.CodeAction.Basic
+import Batteries.Lean.Position
 
 /-!
 # Code action for @[deprecated] replacements

Std/CodeAction/Misc.lean → Batteries/CodeAction/Misc.lean

@@ -5,9 +5,9 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
-import Std.Lean.Name
-import Std.Lean.Position
-import Std.CodeAction.Attr
+import Batteries.Lean.Name
+import Batteries.Lean.Position
+import Batteries.CodeAction.Attr
 import Lean.Meta.Tactic.TryThis
 import Lean.Server.CodeActions.Provider
 

Batteries/Control/ForInStep.lean

@@ -0,0 +1,2 @@
+import Batteries.Control.ForInStep.Basic
+import Batteries.Control.ForInStep.Lemmas

Std/Control/ForInStep/Lemmas.lean → Batteries/Control/ForInStep/Lemmas.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Std.Control.ForInStep.Basic
+import Batteries.Control.ForInStep.Basic
 
 /-! # Additional theorems on `ForInStep` -/
 

Std/Control/Nondet/Basic.lean → Batteries/Control/Nondet/Basic.lean

@@ -3,8 +3,8 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Tactic.Lint.Misc
-import Std.Data.MLList.Basic
+import Batteries.Tactic.Lint.Misc
+import Batteries.Data.MLList.Basic
 
 /-!
 # A nondeterminism monad.

Batteries/Data/Array.lean

@@ -0,0 +1,6 @@
+import Batteries.Data.Array.Basic
+import Batteries.Data.Array.Init.Lemmas
+import Batteries.Data.Array.Lemmas
+import Batteries.Data.Array.Match
+import Batteries.Data.Array.Merge
+import Batteries.Data.Array.Monadic

Std/Data/Array/Basic.lean → Batteries/Data/Array/Basic.lean

@@ -3,14 +3,14 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
 -/
-import Std.Data.List.Init.Attach
-import Std.Data.Array.Init.Lemmas
+import Batteries.Data.List.Init.Attach
+import Batteries.Data.Array.Init.Lemmas
 
 /-!
 ## Definitions on Arrays
 
 This file contains various definitions on `Array`. It does not contain
-proofs about these definitions, those are contained in other files in `Std.Data.Array`.
+proofs about these definitions, those are contained in other files in `Batteries.Data.Array`.
 -/
 
 namespace Array