chore: bump for lean4#3159 (#29)

* chore: bump for lean4#3159 * trying, and failing, to run 'lake update' in test/Mathlib * lake update * update to v4.6.0-rc1 * finish updating for 3159 --------- Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Feb 2, 2024 · 6413ae1 · 6413ae1
1 parent 2a102d0
commit 6413ae1
Show file tree

Hide file tree

Showing 6 changed files with 22 additions and 24 deletions.
diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean
@@ -62,6 +62,7 @@ def kind : Info → String
   | .ofCustomInfo         _ => "CustomInfo"
   | .ofFVarAliasInfo      _ => "FVarAliasInfo"
   | .ofFieldRedeclInfo    _ => "FieldRedeclInfo"
+  | .ofOmissionInfo       _ => "OmissionInfo"
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
 def stx? : Info → Option Syntax
@@ -76,6 +77,7 @@ def stx? : Info → Option Syntax
   | .ofCustomInfo         info => info.stx
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
+  | .ofOmissionInfo       info => info.stx
 
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 def isOriginal (i : Info) : Bool :=
@@ -142,11 +144,14 @@ partial def retainSubstantive (tree : InfoTree) : List InfoTree :=
   tree.filter fun | .ofTacticInfo i => i.isSubstantive | _ => true
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns all results. -/
-partial def findAllInfo (t : InfoTree) (ctx : Option ContextInfo) (p : Info → Bool) :
+partial def findAllInfo (t : InfoTree) (ctx? : Option ContextInfo) (p : Info → Bool) :
     List (Info × Option ContextInfo) :=
   match t with
-  | context ctx t => t.findAllInfo ctx p
-  | node i ts  => (if p i then [(i, ctx)] else []) ++ ts.toList.bind (fun t => t.findAllInfo ctx p)
+  | context ctx t => t.findAllInfo (ctx.mergeIntoOuter? ctx?) p
+  | node i ts  =>
+    let info := if p i then [(i, ctx?)] else []
+    let rest := ts.toList.bind (fun t => t.findAllInfo ctx? p)
+    info ++ rest
   | _ => []
 
 /-- Return all `TacticInfo` nodes in an `InfoTree` with "original" syntax,

diff --git a/REPL/Lean/InfoTree/ToJson.lean b/REPL/Lean/InfoTree/ToJson.lean
@@ -96,7 +96,7 @@ deriving ToJson
 
 partial def InfoTree.toJson (t : InfoTree) (ctx? : Option ContextInfo) : IO Json := do
   match t with
-  | .context i t => t.toJson i
+  | .context ctx t => t.toJson (ctx.mergeIntoOuter? ctx?)
   | .node info children =>
     if let some ctx := ctx? then
       let node : Option Json ← match info with

diff --git a/REPL/Main.lean b/REPL/Main.lean
@@ -131,19 +131,12 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   let messages ← messages.mapM fun m => Message.of m
   let traces ← proofState.newTraces old?
   let trees := proofState.newInfoTrees old?
-  let trees := match old? with
-  | some old =>
-    -- FIXME: I think this should be using `ContextInfo.save`
-    let ctx : ContextInfo :=
-    { env := old.coreState.env
-      ngen := old.coreState.ngen
-      fileMap := old.coreContext.fileMap
-      options := old.coreContext.options
-      currNamespace := old.coreContext.currNamespace
-      openDecls := old.coreContext.openDecls
-      mctx := old.metaState.mctx }
-    trees.map fun t => InfoTree.context ctx t
-  | none => trees
+  let trees ← match old? with
+  | some old => do
+    let (ctx, _) ← old.runMetaM do return { ← CommandContextInfo.save with }
+    let ctx := PartialContextInfo.commandCtx ctx
+    pure <| trees.map fun t => InfoTree.context ctx t
+  | none => pure trees
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
   let sorries ← sorries trees

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.0-rc1
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520",
+   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.27",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "aa20ff6f3effa95af3be5043c93d35a712cd79c4",
+   "rev": "490d2d4820d3ed2dea34f47f3cdfe9d72b8fbc80",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.5.0
		leanprover/lean4:v4.6.0-rc1