Skip to content

Commit 8e951c4

Browse files
kim-emkim-em
authored
chore: bump toolchain to v4.23.0-rc2 (#127)
* chore: bump toolchain to v4.23.0-rc2 * adaptations * update test output
1 parent 4d1b3e1 commit 8e951c4

12 files changed

+33
-32
lines changed

‎REPL/Lean/InfoTree.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -122,9 +122,9 @@ def getUsedConstantsAsSet (t : TacticInfo) : NameSet := go t.goalsBefore.toArray
122122
where go (mvars : Array MVarId) (mctx : MetavarContext) (acc : NameSet) : NameSet := Id.run do
123123
let assignments := mvars.filterMap mctx.getExprAssignmentCore?
124124
if assignments.isEmpty then return acc else
125-
let usedCs : NameSet := assignments.map Expr.getUsedConstantsAsSet |>.foldl .union {}
125+
let usedCs : NameSet := assignments.map Expr.getUsedConstantsAsSet |>.foldl .merge {}
126126
let childMVars := assignments.map fun expr => (expr.collectMVars {}).result
127-
return go childMVars.flatten mctx <| acc.union usedCs
127+
return go childMVars.flatten mctx <| acc.merge usedCs
128128

129129
end Lean.Elab.TacticInfo
130130

‎REPL/Main.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -141,10 +141,10 @@ def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment
141141

142142
private def collectFVarsAux : Expr → NameSet
143143
| .fvar fvarId => NameSet.empty.insert fvarId.name
144-
| .app fm arg => (collectFVarsAux fm).union $ collectFVarsAux arg
145-
| .lam _ binderType body _ => (collectFVarsAux binderType).union $ collectFVarsAux body
146-
| .forallE _ binderType body _ => (collectFVarsAux binderType).union $ collectFVarsAux body
147-
| .letE _ type value body _ => ((collectFVarsAux type).union $ collectFVarsAux value).union $ collectFVarsAux body
144+
| .app fm arg => (collectFVarsAux fm).merge $ collectFVarsAux arg
145+
| .lam _ binderType body _ => (collectFVarsAux binderType).merge $ collectFVarsAux body
146+
| .forallE _ binderType body _ => (collectFVarsAux binderType).merge $ collectFVarsAux body
147+
| .letE _ type value body _ => ((collectFVarsAux type).merge $ collectFVarsAux value).merge $ collectFVarsAux body
148148
| .mdata _ expr => collectFVarsAux expr
149149
| .proj _ _ struct => collectFVarsAux struct
150150
| _ => NameSet.empty

‎lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.22.0
1+
leanprover/lean4:v4.23.0-rc2

‎test/Mathlib/lake-manifest.json‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -5,20 +5,20 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
8+
"rev": "90c0e186fd333cbdddbe0e5148aa3cd2d24dcf9a",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "v4.22.0",
11+
"inputRev": "v4.23.0-rc2",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"url": "https://github.com/leanprover-community/plausible",
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "leanprover-community",
18-
"rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
18+
"rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
21-
"inputRev": "v4.22.0",
21+
"inputRev": "main",
2222
"inherited": true,
2323
"configFile": "lakefile.toml"},
2424
{"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,57 +35,57 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "eb164a46de87078f27640ee71e6c3841defc2484",
38+
"rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
3939
"name": "importGraph",
4040
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v4.22.0",
41+
"inputRev": "main",
4242
"inherited": true,
4343
"configFile": "lakefile.toml"},
4444
{"url": "https://github.com/leanprover-community/ProofWidgets4",
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
48+
"rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
4949
"name": "proofwidgets",
5050
"manifestFile": "lake-manifest.json",
51-
"inputRev": "v0.0.68",
51+
"inputRev": "v0.0.71",
5252
"inherited": true,
5353
"configFile": "lakefile.lean"},
5454
{"url": "https://github.com/leanprover-community/aesop",
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
58+
"rev": "523c8ee53f7057447fc62ec14e506fda4cf63dfa",
5959
"name": "aesop",
6060
"manifestFile": "lake-manifest.json",
61-
"inputRev": "v4.22.0",
61+
"inputRev": "master",
6262
"inherited": true,
6363
"configFile": "lakefile.toml"},
6464
{"url": "https://github.com/leanprover-community/quote4",
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
68+
"rev": "f85ad59c9b60647ef736719c23edd4578f723806",
6969
"name": "Qq",
7070
"manifestFile": "lake-manifest.json",
71-
"inputRev": "v4.22.0",
71+
"inputRev": "master",
7272
"inherited": true,
7373
"configFile": "lakefile.toml"},
7474
{"url": "https://github.com/leanprover-community/batteries",
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover-community",
78-
"rev": "240676e9568c254a69be94801889d4b13f3b249f",
78+
"rev": "6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
81-
"inputRev": "v4.22.0",
81+
"inputRev": "main",
8282
"inherited": true,
8383
"configFile": "lakefile.toml"},
8484
{"url": "https://github.com/leanprover/lean4-cli",
8585
"type": "git",
8686
"subDir": null,
8787
"scope": "leanprover",
88-
"rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
88+
"rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
8989
"name": "Cli",
9090
"manifestFile": "lake-manifest.json",
9191
"inputRev": "main",

‎test/Mathlib/lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
44
[[require]]
55
name = "mathlib"
66
git = "https://github.com/leanprover-community/mathlib4"
7-
rev = "v4.22.0"
7+
rev = "v4.23.0-rc2"
88

99
[[lean_lib]]
1010
name = "ReplMathlibTests"

‎test/Mathlib/lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.22.0
1+
leanprover/lean4:v4.23.0-rc2

‎test/app_type_mismatch2.expected.out‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,5 +37,5 @@
3737
"goals": ["case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0"]}
3838

3939
{"message":
40-
"Lean error:\ntactic 'apply' failed, could not unify the type of `?succ`\n n✝ + 1 = 0\nwith the goal\n true = true\nn✝ : Nat\n⊢ true = true"}
40+
"Lean error:\nTactic `apply` failed: could not unify the type of `?succ`\n n✝ + 1 = 0\nwith the goal\n true = true\n\nn✝ : Nat\n⊢ true = true"}
4141

‎test/dup_msg.expected.out‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,6 @@
1111
[{"severity": "error",
1212
"pos": {"line": 1, "column": 7},
1313
"endPos": {"line": 1, "column": 8},
14-
"data": "unknown identifier 'g'"}],
14+
"data": "Unknown identifier `g`"}],
1515
"env": 2}
1616

‎test/invalid_line_break.expected.out‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,13 @@
22
[{"severity": "error",
33
"pos": {"line": 1, "column": 23},
44
"endPos": {"line": 1, "column": 30},
5-
"data": "unknown identifier 'bysorry'"}],
5+
"data": "Unknown identifier `bysorry`"}],
66
"env": 0}
77

88
{"messages":
99
[{"severity": "error",
1010
"pos": {"line": 1, "column": 23},
1111
"endPos": {"line": 1, "column": 28},
12-
"data": "unknown identifier 'byrfl'"}],
12+
"data": "Unknown identifier `byrfl`"}],
1313
"env": 1}
1414

‎test/invalid_tactic.expected.out‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,6 @@
1616
[{"severity": "error",
1717
"pos": {"line": 0, "column": 0},
1818
"endPos": {"line": 0, "column": 0},
19-
"data": "unknown identifier 'my_fake_premise'"}],
19+
"data": "Unknown identifier `my_fake_premise`"}],
2020
"goals": []}
2121

0 commit comments

Comments
 (0)