From 2fae043a593358032a516184fddaacc3b03437f9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 8 Aug 2024 21:50:30 +1000 Subject: [PATCH] chore: adaptations for nightly-2024-08-08 (#910) Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: Wojciech Nawrocki Co-authored-by: L Co-authored-by: Joachim Breitner Co-authored-by: Kyle Miller --- Batteries/Data/Array/Lemmas.lean | 5 +++++ Batteries/Data/HashMap/WF.lean | 2 +- Batteries/Data/UnionFind/Basic.lean | 3 ++- Batteries/Lean/AttributeExtra.lean | 4 +++- Batteries/Lean/HashSet.lean | 11 ++--------- Batteries/Lean/Meta/Inaccessible.lean | 2 +- Batteries/Linter/UnnecessarySeqFocus.lean | 4 ++-- Batteries/Linter/UnreachableTactic.lean | 2 +- Batteries/Tactic/Lint/Frontend.lean | 6 +++--- Batteries/Tactic/Lint/Misc.lean | 4 ++-- lean-toolchain | 2 +- scripts/check_imports.lean | 2 +- test/where.lean | 1 + 13 files changed, 25 insertions(+), 23 deletions(-) diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean index 753cbb4955..10102cb3cc 100644 --- a/Batteries/Data/Array/Lemmas.lean +++ b/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 diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean index e83e32e567..427e2a4537 100644 --- a/Batteries/Data/HashMap/WF.lean +++ b/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⟩ diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean index 292f4285eb..10b37105a3 100644 --- a/Batteries/Data/UnionFind/Basic.lean +++ b/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] diff --git a/Batteries/Lean/AttributeExtra.lean b/Batteries/Lean/AttributeExtra.lean index aeac0267c5..adb6c0ef1f 100644 --- a/Batteries/Lean/AttributeExtra.lean +++ b/Batteries/Lean/AttributeExtra.lean @@ -8,6 +8,8 @@ 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. @@ -94,7 +96,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 α) diff --git a/Batteries/Lean/HashSet.lean b/Batteries/Lean/HashSet.lean index 0dedb7cd4f..7882358c40 100644 --- a/Batteries/Lean/HashSet.lean +++ b/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 diff --git a/Batteries/Lean/Meta/Inaccessible.lean b/Batteries/Lean/Meta/Inaccessible.lean index e308364616..fbc50a363e 100644 --- a/Batteries/Lean/Meta/Inaccessible.lean +++ b/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 diff --git a/Batteries/Linter/UnnecessarySeqFocus.lean b/Batteries/Linter/UnnecessarySeqFocus.lean index 566da1d490..f53fd05f51 100644 --- a/Batteries/Linter/UnnecessarySeqFocus.lean +++ b/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 @@ -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 diff --git a/Batteries/Linter/UnreachableTactic.lean b/Batteries/Linter/UnreachableTactic.lean index a4bedbe10c..cd73649969 100644 --- a/Batteries/Linter/UnreachableTactic.lean +++ b/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. diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean index 841c696af8..27ff3bf3b2 100644 --- a/Batteries/Tactic/Lint/Frontend.lean +++ b/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 diff --git a/Batteries/Tactic/Lint/Misc.lean b/Batteries/Tactic/Lint/Misc.lean index 3f0e69f648..a0aa8bc884 100644 --- a/Batteries/Tactic/Lint/Misc.lean +++ b/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 diff --git a/lean-toolchain b/lean-toolchain index 64981ae5f5..9f6eaf7908 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.11.0-rc1 +leanprover/lean4:nightly-2024-08-08 diff --git a/scripts/check_imports.lean b/scripts/check_imports.lean index 94e778369f..55bf0e8342 100644 --- a/scripts/check_imports.lean +++ b/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 diff --git a/test/where.lean b/test/where.lean index 6fd098ce53..5f7a4bcfa3 100644 --- a/test/where.lean +++ b/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