chore: bump to v4.16.0-rc2 (#67)

* chore: bump to v4.16.0-rc2 * fix * fix: filter out term sorries that come from tactic sorries (#68) * fix: filter out term sorries that come from tactic sorries tactic sorry now has a child `exact sorry` in the infotree * bump test * fix mathlib test --------- Co-authored-by: L <[email protected]>
leanprover-community · Jan 15, 2025 · 4d7e572 · 4d7e572
1 parent 2196679
commit 4d7e572
Show file tree

Hide file tree

Showing 8 changed files with 50 additions and 27 deletions.
diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean
@@ -63,8 +63,8 @@ def kind : Info → String
   | .ofCustomInfo         _ => "CustomInfo"
   | .ofFVarAliasInfo      _ => "FVarAliasInfo"
   | .ofFieldRedeclInfo    _ => "FieldRedeclInfo"
-  | .ofOmissionInfo       _ => "OmissionInfo"
   | .ofChoiceInfo         _ => "ChoiceInfo"
+  | .ofDelabTermInfo      _ => "DelabTermInfo"
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
 def stx? : Info → Option Syntax
@@ -80,8 +80,8 @@ def stx? : Info → Option Syntax
   | .ofCustomInfo         info => info.stx
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
-  | .ofOmissionInfo       info => info.stx
   | .ofChoiceInfo         info => info.stx
+  | .ofDelabTermInfo      info => info.stx
 
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 def isOriginal (i : Info) : Bool :=
@@ -154,13 +154,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)
+    (stop : Info → Bool := fun _ => false) :
     List (Info × Option ContextInfo) :=
   match t with
-  | context ctx t => t.findAllInfo (ctx.mergeIntoOuter? ctx?) p
+  | context ctx t => t.findAllInfo (ctx.mergeIntoOuter? ctx?) p stop
   | node i ts  =>
     let info := if p i then [(i, ctx?)] else []
-    let rest := ts.toList.flatMap (fun t => t.findAllInfo ctx? p)
+    let rest := if stop i then [] else ts.toList.flatMap (fun t => t.findAllInfo ctx? p stop)
     info ++ rest
   | _ => []
 
@@ -189,9 +190,9 @@ def findSorryTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo) :=
 corresponding to explicit `sorry` terms,
 each equipped with its relevant `ContextInfo`. -/
 def findSorryTermNodes (t : InfoTree) : List (TermInfo × ContextInfo) :=
-  let infos := t.findAllInfo none fun i => match i with
-  | .ofTermInfo i => i.stx.isSorryTerm
-  | _ => false
+  let infos := t.findAllInfo none
+    (fun i => match i with | .ofTermInfo i => i.stx.isSorryTerm | _ => false)
+    (fun i => match i with | .ofTacticInfo i => i.stx.isSorryTactic | _ => false)
   infos.filterMap fun p => match p with
   | (.ofTermInfo i, some ctx) => (i, ctx)
   | _ => none

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc2
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e9ae2a61ef5c99d6edac84f0d04f6324c5d97f67",
+   "rev": "15f16b1ec50f425147926be1aede7b4baa725380",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-patch1",
+   "inputRev": "v4.16.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,30 +35,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

diff --git 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.15.0-patch1"
+rev = "v4.16.0-rc2"
 
 [[lean_lib]]
 name = "ReplMathlibTests"

diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc2
diff --git a/test/Mathlib/test/H20231020.in b/test/Mathlib/test/H20231020.in
@@ -1,4 +1,4 @@
-{"cmd": "import Mathlib.Algebra.BigOperators.Group.Finset\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Complex.Basic\nimport Mathlib.Data.Nat.Log\nimport Mathlib.Data.Complex.Exponential\nimport Mathlib.NumberTheory.Divisors\nimport Mathlib.Data.ZMod.Defs\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.Topology.Basic\nimport Mathlib.Data.Nat.Digits\nimport Mathlib.Tactic.NormNum.GCD\nopen BigOperators\nopen Real\nopen Nat\nopen Topology"}
+{"cmd": "import Mathlib.Algebra.BigOperators.Group.Finset.Basic\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Complex.Basic\nimport Mathlib.Data.Nat.Log\nimport Mathlib.Data.Complex.Exponential\nimport Mathlib.NumberTheory.Divisors\nimport Mathlib.Data.ZMod.Defs\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.Topology.Basic\nimport Mathlib.Data.Nat.Digits\nimport Mathlib.Tactic.NormNum.GCD\nopen BigOperators\nopen Real\nopen Nat\nopen Topology"}
 
 {"cmd": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num", "env": 0}
 

diff --git a/test/Mathlib/test/H20231020.lean b/test/Mathlib/test/H20231020.lean
@@ -1,4 +1,4 @@
-import Mathlib.Algebra.BigOperators.Group.Finset
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Nat.Log

diff --git a/test/calc.expected.out b/test/calc.expected.out
@@ -3,8 +3,12 @@
    ["Trans.trans",
     "sorryAx",
     "instOfNatNat",
+    "Lean.Name.num",
+    "Lean.Name.str",
+    "Lean.Name.anonymous",
     "instTransEq",
     "Nat",
+    "Lean.Name",
     "OfNat.ofNat",
     "Bool.false",
     "Eq"],
@@ -20,14 +24,32 @@
    "goals": "no goals",
    "endPos": {"line": 3, "column": 19}},
   {"usedConstants":
-   ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
+   ["sorryAx",
+    "instOfNatNat",
+    "Lean.Name.num",
+    "Lean.Name.str",
+    "Lean.Name.anonymous",
+    "Nat",
+    "Lean.Name",
+    "OfNat.ofNat",
+    "Bool.false",
+    "Eq"],
    "tactic": "sorry",
    "proofState": 4,
    "pos": {"line": 2, "column": 14},
    "goals": "⊢ 3 = 4",
    "endPos": {"line": 2, "column": 19}},
   {"usedConstants":
-   ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
+   ["sorryAx",
+    "instOfNatNat",
+    "Lean.Name.num",
+    "Lean.Name.str",
+    "Lean.Name.anonymous",
+    "Nat",
+    "Lean.Name",
+    "OfNat.ofNat",
+    "Bool.false",
+    "Eq"],
    "tactic": "sorry",
    "proofState": 5,
    "pos": {"line": 3, "column": 14},
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.15.0
		leanprover/lean4:v4.16.0-rc2