From 0449d86bfbbbefd837d9bc77dbc413fe0dff056e Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Thu, 6 Jun 2024 21:53:06 +0000 Subject: [PATCH] bump --- Leaff/Diff.lean | 52 +++++++++++++++++++++++----------------------- Leaff/Hash.lean | 2 +- Leaff/HashSet.lean | 4 ++-- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- lean-toolchain | 2 +- test/main.lean | 2 +- test2/main.lean | 2 +- 8 files changed, 36 insertions(+), 36 deletions(-) diff --git a/Leaff/Diff.lean b/Leaff/Diff.lean index b3637f3..a2e0b35 100644 --- a/Leaff/Diff.lean +++ b/Leaff/Diff.lean @@ -1,11 +1,11 @@ import Lean -import Std.Lean.PersistentHashSet -import Std.Lean.Name -import Std.Tactic.OpenPrivate +import Batteries.Lean.PersistentHashSet +import Batteries.Lean.Name +import Batteries.Tactic.OpenPrivate -- import Leaff.Deriving.Optics import Leaff.Hash import Leaff.HashSet --- import Std.Lean.HashMap +-- import Batteries.Lean.HashMap /-! @@ -239,7 +239,7 @@ def mod : Diff → Name | .attributeChanged _ _ m => m | .extensionEntriesModified _ => Name.anonymous -open Std +open Batteries def mkConstWithLevelParams' (constInfo : ConstantInfo) : Expr := mkConst constInfo.name (constInfo.levelParams.map mkLevelParam) @@ -250,7 +250,6 @@ mkConst constInfo.name (constInfo.levelParams.map mkLevelParam) -- links / messagedata in the infoview maybe extracted as links somehow -- especially for the diffs command -- could we even have some form of expr diff? -open ToFormat in def summarize (diffs : List Diff) : MessageData := Id.run do if diffs == [] then return "No differences found." let mut out : MessageData := "Found differences:" ++ Format.line @@ -336,7 +335,7 @@ open Lean Environment namespace Lean.Environment -open Std +open Batteries def importDiffs (old new : Environment) : List Diff := Id.run do let mut out : List Diff := [] @@ -365,7 +364,7 @@ def importDiffs (old new : Environment) : List Diff := Id.run do namespace Leaff.Lean.HashMap variable [BEq α] [Hashable α] -/-- copied from Std, we copy rather than importing to reduce the std dependency +/-- copied from Batteries, we copy rather than importing to reduce the std dependency and make changing the Lean version used by Leaff easier (hopefully) -/ instance : ForIn m (HashMap α β) (α × β) where forIn m init f := do @@ -441,23 +440,24 @@ def diffExtension (old new : Environment) continue if ! ns.contains (renames.findD a a) then out := .docRemoved (renames.findD a a) (moduleName new (renames.findD a a)) :: out - | ``Lean.reducibilityAttrs => do - let os := PersistentEnvExtension.getImportedState reducibilityAttrs.ext old - let ns := PersistentEnvExtension.getImportedState reducibilityAttrs.ext new - for (a, red) in ns do - if ignoreInternal && a.isInternalDetail then - continue - if ! os.contains (revRenames.findD a a) then - out := .attributeAdded (toString red) a (moduleName new a) :: out - else - if os.find! (revRenames.findD a a) != red then - -- TODO specify more - out := .attributeChanged (toString red) a (moduleName new a) :: out - for (a, red) in os do - if ignoreInternal && a.isInternalDetail then - continue - if ! ns.contains (renames.findD a a) then - out := .attributeRemoved (toString red) (renames.findD a a) (moduleName new (renames.findD a a)) :: out + -- TODO fix after https://github.com/leanprover/lean4/commit/47a34316fc03ce936fddd2d3dce44784c5bcdfa9 + -- | ``Lean.reducibilityAttrs => do + -- let os := PersistentEnvExtension.getImportedState reducibilityAttrs.ext old + -- let ns := PersistentEnvExtension.getImportedState reducibilityAttrs.ext new + -- for (a, red) in ns do + -- if ignoreInternal && a.isInternalDetail then + -- continue + -- if ! os.contains (revRenames.findD a a) then + -- out := .attributeAdded (toString red) a (moduleName new a) :: out + -- else + -- if os.find! (revRenames.findD a a) != red then + -- -- TODO specify more + -- out := .attributeChanged (toString red) a (moduleName new a) :: out + -- for (a, red) in os do + -- if ignoreInternal && a.isInternalDetail then + -- continue + -- if ! ns.contains (renames.findD a a) then + -- out := .attributeRemoved (toString red) (renames.findD a a) (moduleName new (renames.findD a a)) :: out | ``Lean.protectedExt => do let os := TagDeclarationExtension.getImportedState protectedExt old let ns := TagDeclarationExtension.getImportedState protectedExt new @@ -597,7 +597,7 @@ def extDiffs (old new : Environment) (renames : NameMap Name) (ignoreInternal : -- Lean.Meta.recursorAttribute -- Lean.Meta.simpExtension -- Lean.Meta.congrExtension --- Std.Tactic.Alias.aliasExt +-- Batteries.Tactic.Alias.aliasExt open Trait diff --git a/Leaff/Hash.lean b/Leaff/Hash.lean index 8b1bcde..80eb9a7 100644 --- a/Leaff/Hash.lean +++ b/Leaff/Hash.lean @@ -1,5 +1,5 @@ import Lean -open Lean Meta Elab Std +open Lean Meta Elab def Lean.ConstantInfo.hash (c : ConstantInfo) : UInt64 := mixHash c.type.hash c.value!.hash diff --git a/Leaff/HashSet.lean b/Leaff/HashSet.lean index 52f8db6..9484c55 100644 --- a/Leaff/HashSet.lean +++ b/Leaff/HashSet.lean @@ -1,7 +1,7 @@ import Lean.Data.HashSet -import Std.Data.List.Basic +import Batteries.Data.List.Basic ---TODO consider removing Std dep +--TODO consider removing Batteries dep namespace Array diff --git a/lake-manifest.json b/lake-manifest.json index 535341d..3466d2e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -10,11 +10,11 @@ "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/std4.git", + {"url": "https://github.com/leanprover-community/batteries.git", "type": "git", "subDir": null, - "rev": "d9822056f5ae3579acbd9af5c8d0ee5fd06c85dc", - "name": "std", + "rev": "3b1555252d9369be7b0f39a0e0a07daa864e5b5b", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, diff --git a/lakefile.lean b/lakefile.lean index 8004b6b..b465dae 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -3,7 +3,7 @@ import Lake open Lake DSL require Cli from git "https://github.com/leanprover/lean4-cli.git" @ "main" -require std from git "https://github.com/leanprover/std4.git" @ "main" +require batteries from git "https://github.com/leanprover-community/batteries.git" @ "main" meta if get_config? mathlib = some "on" then require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "30d39f9a058b13ec1786a90af4c051d650762951" meta if get_config? mathlib = some "on" then diff --git a/lean-toolchain b/lean-toolchain index 9ad3040..ef1f67e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.8.0 diff --git a/test/main.lean b/test/main.lean index 2468c24..6363424 100644 --- a/test/main.lean +++ b/test/main.lean @@ -6,7 +6,7 @@ open Lean def sp : SearchPath := ["."/".lake" /"build"/"lib","."/".lake" /"packages"/"std"/"build"/"lib","/home/alexanderbest/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib/lean"] -#eval summarizeDiffImports #[`Std.Classes.RatCast] #[`Std.Data.Rat] sp sp +#eval summarizeDiffImports #[`Batteries.Classes.RatCast] #[`Batteries.Data.Rat] sp sp -- #eval summarizeDiffImports #[`Mathlib] #[`Mathlib] sp₁ sp₂ #eval summarizeDiffImports #[`test.TestA] #[`test2.Test] sp sp diff --git a/test2/main.lean b/test2/main.lean index 6f23d25..89e9a1a 100644 --- a/test2/main.lean +++ b/test2/main.lean @@ -6,7 +6,7 @@ open Lean def sp : SearchPath := ["."/".lake" /"build"/"lib","."/".lake" /"packages"/"std"/"build"/"lib","/home/alexanderbest/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib/lean"] -#eval summarizeDiffImports #[`Std.Classes.RatCast] #[`Std.Data.Rat] sp sp +#eval summarizeDiffImports #[`Batteries.Classes.RatCast] #[`Batteries.Data.Rat] sp sp -- #eval summarizeDiffImports #[`Mathlib] #[`Mathlib] sp₁ sp₂ #eval summarizeDiffImports #[`test.TestA] #[`test.TestB] sp sp