From 008cfbcefc142be39203b362690cf8230f21a253 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 8 Jan 2025 16:43:25 +1100 Subject: [PATCH] chore: bump to v4.15.0-rc1 (#61) * chore: bump to v4.15.0-rc1 * fix InfoTree.lean (cf. https://github.com/leanprover/lean4/pull/5835) * fix: workaround for Meta.Context.config private (#64) --------- Co-authored-by: Bryan Gin-ge Chen Co-authored-by: L --- REPL/Lean/InfoTree.lean | 18 +++++++++++------- REPL/Snapshots.lean | 3 ++- lean-toolchain | 2 +- test/Mathlib/lake-manifest.json | 28 ++++++++++++++-------------- test/Mathlib/lakefile.toml | 2 +- test/Mathlib/lean-toolchain | 2 +- 6 files changed, 30 insertions(+), 25 deletions(-) diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index 7abf0b8..88ec289 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -53,6 +53,7 @@ namespace Lean.Elab.Info def kind : Info → String | .ofTacticInfo _ => "TacticInfo" | .ofTermInfo _ => "TermInfo" + | ofPartialTermInfo _ => "PartialTermInfo" | .ofCommandInfo _ => "CommmandInfo" | .ofMacroExpansionInfo _ => "MacroExpansionInfo" | .ofOptionInfo _ => "OptionInfo" @@ -63,11 +64,13 @@ def kind : Info → String | .ofFVarAliasInfo _ => "FVarAliasInfo" | .ofFieldRedeclInfo _ => "FieldRedeclInfo" | .ofOmissionInfo _ => "OmissionInfo" + | .ofChoiceInfo _ => "ChoiceInfo" /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/ def stx? : Info → Option Syntax | .ofTacticInfo info => info.stx | .ofTermInfo info => info.stx + | ofPartialTermInfo info => info.stx | .ofCommandInfo info => info.stx | .ofMacroExpansionInfo info => info.stx | .ofOptionInfo info => info.stx @@ -78,6 +81,7 @@ def stx? : Info → Option Syntax | .ofFVarAliasInfo _ => none | .ofFieldRedeclInfo info => info.stx | .ofOmissionInfo info => info.stx + | .ofChoiceInfo info => info.stx /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/ def isOriginal (i : Info) : Bool := @@ -214,13 +218,13 @@ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Posit def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position × Array Name) := -- HACK: creating a child ngen - t.findTacticNodes.map fun ⟨i, ctx⟩ => - let range := stxRange ctx.fileMap i.stx - ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, - i.stx, - i.goalsBefore, - range.fst, - range.snd, + t.findTacticNodes.map fun ⟨i, ctx⟩ => + let range := stxRange ctx.fileMap i.stx + ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, + i.stx, + i.goalsBefore, + range.fst, + range.snd, i.getUsedConstantsAsSet.toArray ) diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index 1114c24..7297700 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -259,13 +259,14 @@ When pickling the `Environment`, we do so relative to its imports. def pickle (p : ProofSnapshot) (path : FilePath) : IO Unit := do let env := p.coreState.env let p' := { p with coreState := { p.coreState with env := ← mkEmptyEnvironment }} + let (cfg, _) ← Lean.Meta.getConfig.toIO p'.coreContext p'.coreState p'.metaContext p'.metaState _root_.pickle path (env.header.imports, env.constants.map₂, ({ p'.coreState with } : CompactableCoreState), p'.coreContext, p'.metaState, - ({ p'.metaContext with } : CompactableMetaContext), + ({ p'.metaContext with config := cfg } : CompactableMetaContext), p'.termState, ({ p'.termContext with } : CompactableTermContext), p'.tacticState, diff --git a/lean-toolchain b/lean-toolchain index 1e70935..cf25a98 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.15.0-rc1 diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index f312e5a..60686a2 100644 --- a/test/Mathlib/lake-manifest.json +++ b/test/Mathlib/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4bbdccd9c5f862bf90ff12f0a9e2c8be032b9a84", + "rev": "41ff1f7899c971f91362710d4444e338b8acd644", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -35,47 +35,47 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "519e509a28864af5bed98033dd33b95cf08e9aa7", + "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "68280daef58803f68368eb2e53046dabcd270c9d", + "rev": "2b000e02d50394af68cfb4770a291113d94801b5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.47", + "inputRev": "v0.0.48", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030", + "rev": "8b6048aa0a4a4b6bcf83597802d8dee734e64b7e", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.14.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "v4.14.0", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml index 6ff9631..ce5ace7 100644 --- a/test/Mathlib/lakefile.toml +++ b/test/Mathlib/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "v4.14.0" +rev = "v4.15.0-rc1" [[lean_lib]] name = "ReplMathlibTests" diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index 401bc14..cf25a98 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 \ No newline at end of file +leanprover/lean4:v4.15.0-rc1