Trigger CI for leanprover/lean4#4717

.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'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean

Batteries.lean

@@ -35,7 +35,6 @@ import Batteries.Data.Range
 import Batteries.Data.Rat
 import Batteries.Data.String
 import Batteries.Data.Sum
-import Batteries.Data.Thunk
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
 import Batteries.Lean.AttributeExtra

Batteries/Data/Array/Lemmas.lean

@@ -11,6 +11,11 @@ import Batteries.Util.ProofWanted
 
 namespace Array
 
+theorem get_modify {arr : Array α} {x i} (h : i < arr.size) :
+    (arr.modify x f).get ⟨i, by simp [h]⟩ =
+    if x = i then f (arr.get ⟨i, h⟩) else arr.get ⟨i, h⟩ := by
+  simp [getElem_modify h]
+
 theorem forIn_eq_data_forIn [Monad m]
     (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn as b f = forIn as.data b f := by

Batteries/Data/HashMap/WF.lean

@@ -224,7 +224,7 @@ private theorem pairwise_replaceF [BEq α] [PartialEquivBEq α]
   | cons a l ih =>
     simp only [List.pairwise_cons, List.replaceF] at H ⊢
     generalize e : cond .. = z; unfold cond at e; revert e
-    split <;> (intro h; subst h; simp)
+    split <;> (intro h; subst h; simp only [List.pairwise_cons])
     · next e => exact ⟨(H.1 · · ∘ PartialEquivBEq.trans e), H.2⟩
     · next e =>
       refine ⟨fun a h => ?_, ih H.2⟩

Batteries/Data/LazyList.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Simon Hudon
 -/
-import Batteries.Data.Thunk
+
 /-!
 # Lazy lists
 

Batteries/Data/UnionFind/Basic.lean

@@ -307,7 +307,8 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     rw [findAux_s]; split <;> [rfl; skip]
     have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
     have := lt_of_parentD (by rwa [parentD_eq])
-    rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify (by rwa [FindAux.size_eq])]
+    rw [rankD_eq' (by simp [FindAux.size_eq, h])]
+    rw [Array.get_modify (by rwa [FindAux.size_eq])]
     split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩), -Array.get_eq_getElem]
   else
     simp only [rankD, Array.data_length, Array.get_eq_getElem, rank]

Batteries/Lean/AttributeExtra.lean

@@ -4,10 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Batteries.Lean.TagAttribute
+import Std.Data.HashMap.Basic
+
 open Lean
 
 namespace Lean
 
+open Std
+
 /--
 `TagAttributeExtra` works around a limitation of `TagAttribute`, which is that definitions
 must be tagged in the same file that declares the definition.
@@ -73,7 +77,7 @@ structure ParametricAttributeExtra (α : Type) where
   /-- The underlying `ParametricAttribute`. -/
   attr : ParametricAttribute α
   /-- A list of pre-tagged declarations with their values. -/
-  base : HashMap Name α
+  base : Std.HashMap Name α
   deriving Inhabited
 
 /--
@@ -94,7 +98,7 @@ or `none` if `decl` is not tagged.
 -/
 def getParam? [Inhabited α] (attr : ParametricAttributeExtra α)
     (env : Environment) (decl : Name) : Option α :=
-  attr.attr.getParam? env decl <|> attr.base.find? decl
+  attr.attr.getParam? env decl <|> attr.base[decl]?
 
 /-- Applies attribute `attr` to declaration `decl`, given a value for the parameter. -/
 def setParam (attr : ParametricAttributeExtra α)

Batteries/Lean/HashMap.lean

@@ -4,22 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Lean.Data.HashMap
-
-namespace Lean.HashMap
+import Std.Data.HashMap.Basic
+namespace Std.HashMap
 
 variable [BEq α] [Hashable α]
 
-instance : ForIn m (HashMap α β) (α × β) where
-  forIn m init f := do
-    let mut acc := init
-    for buckets in m.val.buckets.val do
-      for d in buckets do
-        match ← f d acc with
-        | .done b => return b
-        | .yield b => acc := b
-    return acc
-
 /--
 `O(|other|)` amortized. Merge two `HashMap`s.
 The values of keys which appear in both maps are combined using the monadic function `f`.
@@ -28,7 +17,7 @@ The values of keys which appear in both maps are combined using the monadic func
 def mergeWithM {m α β} [BEq α] [Hashable α] [Monad m] (f : α → β → β → m β)
     (self other : HashMap α β) : m (HashMap α β) :=
   other.foldM (init := self) fun map k v₂ =>
-    match map.find? k with
+    match map[k]? with
     | none => return map.insert k v₂
     | some v₁ => return map.insert k (← f k v₁ v₂)
 
@@ -41,6 +30,6 @@ def mergeWith (f : α → β → β → β) (self other : HashMap α β) : HashM
   -- Implementing this function directly, rather than via `mergeWithM`, gives
   -- us less constrained universes.
   other.fold (init := self) fun map k v₂ =>
-    match map.find? k with
+    match map[k]? with
     | none => map.insert k v₂
     | some v₁ => map.insert k <| f k v₁ v₂

Batteries/Lean/HashSet.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Lean.Data.HashSet
+import Std.Data.HashSet
 
-namespace Lean.HashSet
+namespace Std.HashSet
 
 variable [BEq α] [Hashable α]
 
@@ -66,10 +66,3 @@ def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
 @[inline]
 protected def ofArray [BEq α] [Hashable α] (as : Array α) : HashSet α :=
   HashSet.empty.insertMany as
-
-/--
-`O(n)`. Obtain a `HashSet` from a list.
--/
-@[inline]
-protected def ofList [BEq α] [Hashable α] (as : List α) : HashSet α :=
-  HashSet.empty.insertMany as

Batteries/Lean/Meta/Inaccessible.lean

@@ -5,7 +5,7 @@ Authors: Jannis Limperg
 -/
 import Lean.Meta.InferType
 
-open Lean Lean.Meta
+open Lean Lean.Meta Std
 
 /--
 Obtain the inaccessible fvars from the given local context. An fvar is
@@ -15,7 +15,7 @@ later fvar with the same user name.
 def Lean.LocalContext.inaccessibleFVars (lctx : LocalContext) :
     Array LocalDecl :=
   let (result, _) :=
-    lctx.foldr (β := Array LocalDecl × HashSet Name)
+    lctx.foldr (β := Array LocalDecl × Std.HashSet Name)
       (init := (Array.mkEmpty lctx.numIndices, {}))
       fun ldecl (result, seen) =>
         if ldecl.isImplementationDetail then

Batteries/Linter/UnnecessarySeqFocus.lean

@@ -8,7 +8,7 @@ import Lean.Linter.Util
 import Batteries.Lean.AttributeExtra
 
 namespace Batteries.Linter
-open Lean Elab Command Linter
+open Lean Elab Command Linter Std
 
 /--
 Enables the 'unnecessary `<;>`' linter. This will warn whenever the `<;>` tactic combinator
@@ -83,7 +83,7 @@ structure Entry where
   used : Bool
 
 /-- The monad for collecting used tactic syntaxes. -/
-abbrev M (ω) := StateRefT (HashMap String.Range Entry) (ST ω)
+abbrev M (ω) := StateRefT (Std.HashMap String.Range Entry) (ST ω)
 
 /-- True if this is a `<;>` node in either `tactic` or `conv` classes. -/
 @[inline] def isSeqFocus (k : SyntaxNodeKind) : Bool :=
@@ -120,7 +120,7 @@ partial def markUsedTactics : InfoTree → M ω Unit
   | .node i c => do
     if let .ofTacticInfo i := i then
       if let some r := i.stx.getRange? true then
-      if let some entry := (← get).find? r then
+      if let some entry := (← get)[r]? then
       if i.stx.getKind == ``Parser.Tactic.«tactic_<;>_» then
         let isBad := do
           unless i.goalsBefore.length == 1 || !multigoalAttr.hasTag env i.stx[0].getKind do

Batteries/Linter/UnreachableTactic.lean

@@ -8,7 +8,7 @@ import Lean.Linter.Util
 import Batteries.Tactic.Unreachable
 
 namespace Batteries.Linter
-open Lean Elab Command Linter
+open Lean Elab Command Linter Std
 
 /--
 Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed.
@@ -29,14 +29,14 @@ namespace UnreachableTactic
 def getLinterUnreachableTactic (o : Options) : Bool := getLinterValue linter.unreachableTactic o
 
 /-- The monad for collecting used tactic syntaxes. -/
-abbrev M := StateRefT (HashMap String.Range Syntax) IO
+abbrev M := StateRefT (Std.HashMap String.Range Syntax) IO
 
 /--
 A list of blacklisted syntax kinds, which are expected to have subterms that contain
 unevaluated tactics.
 -/
 initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
-  IO.mkRef <| HashSet.empty
+  IO.mkRef <| Std.HashSet.empty
     |>.insert ``Parser.Term.binderTactic
     |>.insert ``Lean.Parser.Term.dynamicQuot
     |>.insert ``Lean.Parser.Tactic.quotSeq

Batteries/Tactic/Lint/Frontend.lean

@@ -126,7 +126,7 @@ def sortResults (results : HashMap Name α) : CoreM <| Array (Name × α) := do
   for (n, _) in results.toArray do
     if let some range ← findDeclarationRanges? n then
       key := key.insert n <| range.range.pos.line
-  pure $ results.toArray.qsort fun (a, _) (b, _) => key.findD a 0 < key.findD b 0
+  pure $ results.toArray.qsort fun (a, _) (b, _) => key.getD a 0 < key.getD b 0
 
 /-- Formats a linter warning as `#check` command with comment. -/
 def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Bool := false)
@@ -158,7 +158,7 @@ def groupedByFilename (results : HashMap Name MessageData) (useErrorFormat : Boo
       let mod ← findModuleOf? declName
       let mod := mod.getD (← getEnv).mainModule
       grouped.insert mod <$>
-        match grouped.find? mod with
+        match grouped[mod]? with
         | some (fp, msgs) => pure (fp, msgs.insert declName msg)
         | none => do
           let fp ← if useErrorFormat then
@@ -217,7 +217,7 @@ def getDeclsInPackage (pkg : Name) : CoreM (Array Name) := do
   let mut decls ← getDeclsInCurrModule
   let modules := env.header.moduleNames.map (pkg.isPrefixOf ·)
   return env.constants.map₁.fold (init := decls) fun decls declName _ =>
-    if modules[env.const2ModIdx[declName].get! (α := Nat)]! then
+    if modules[env.const2ModIdx[declName]?.get! (α := Nat)]! then
       decls.push declName
     else decls
 

Batteries/Tactic/Lint/Misc.lean

@@ -12,7 +12,7 @@ import Lean.Util.Recognizers
 import Lean.DocString
 import Batteries.Tactic.Lint.Basic
 
-open Lean Meta
+open Lean Meta Std
 
 namespace Std.Tactic.Lint
 
@@ -143,7 +143,7 @@ In pseudo-mathematical form, this returns `{{p : parameter | p ∈ u} | (u : lev
 FIXME: We use `Array Name` instead of `HashSet Name`, since `HashSet` does not have an equality
 instance. It will ignore `nm₀.proof_i` declarations.
 -/
-private def univParamsGrouped (e : Expr) (nm₀ : Name) : Lean.HashSet (Array Name) :=
+private def univParamsGrouped (e : Expr) (nm₀ : Name) : HashSet (Array Name) :=
   runST fun σ => do
     let res ← ST.mkRef (σ := σ) {}
     e.forEach fun

lakefile.lean

@@ -13,7 +13,7 @@ package batteries where
 @[default_target]
 lean_lib Batteries
 
-@[default_target]
+@[default_target, lint_driver]
 lean_exe runLinter where
   srcDir := "scripts"
   supportInterpreter := true

scripts/check_imports.lean

@@ -70,7 +70,7 @@ def writeImportModule (path : FilePath) (imports : Array Name) : IO Unit := do
 /-- Check for imports and return true if warnings issued. -/
 def checkMissingImports (modName : Name) (modData : ModuleData) (reqImports : Array Name) :
     LogIO Bool := do
-  let names : HashSet Name := HashSet.ofArray (modData.imports.map (·.module))
+  let names : Std.HashSet Name := Std.HashSet.ofArray (modData.imports.map (·.module))
   let mut warned := false
   for req in reqImports do
     if !names.contains req then

test/where.lean

@@ -2,6 +2,7 @@ import Batteries.Tactic.Where
 
 -- Return to pristine state
 set_option linter.missingDocs false
+set_option internal.minimalSnapshots false
 
 /-- info: -- In root namespace with initial scope -/
 #guard_msgs in #where