Skip to content

Commit b216e5c

Browse files
JulianJulian
committed
Bump the Lean versions in CI.
1 parent 32fb8aa commit b216e5c

13 files changed

Lines changed: 90 additions & 67 deletions

‎demos/project/lake-manifest.json‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "d9874e4268b90436f38b811922d5aff6af138197",
8+
"rev": "d3716e6d2ea114ae7d9f994e5ebf3c064d80c8a7",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": null,
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "leanprover-community",
18-
"rev": "293af9b2a383eed4d04d66b898d608d0a44b750f",
18+
"rev": "f3c7bd5061bd81b4480295c524d4f245c8b7e4e2",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
38+
"rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
3939
"name": "importGraph",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",
@@ -45,50 +45,50 @@
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
48+
"rev": "e4952ae2afde0dd2868b313356d1ce00da677bd9",
4949
"name": "proofwidgets",
5050
"manifestFile": "lake-manifest.json",
51-
"inputRev": "v0.0.98",
51+
"inputRev": "main",
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": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
58+
"rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
5959
"name": "aesop",
6060
"manifestFile": "lake-manifest.json",
61-
"inputRev": "v4.30.0-rc2",
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": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
68+
"rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
6969
"name": "Qq",
7070
"manifestFile": "lake-manifest.json",
71-
"inputRev": "v4.30.0-rc2",
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": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
78+
"rev": "9c6e03c0a86237b199ebe6b1fbac18078a767ade",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
81-
"inputRev": "v4.30.0-rc2",
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": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
88+
"rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
8989
"name": "Cli",
9090
"manifestFile": "lake-manifest.json",
91-
"inputRev": "v4.30.0-rc2",
91+
"inputRev": "v4.32.0-rc1",
9292
"inherited": true,
9393
"configFile": "lakefile.toml"}],
9494
"name": "NeovimLoves",

‎demos/project/lean-toolchain‎

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

‎justfile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -118,4 +118,4 @@ _clone-test-dependencies: _clone-dependencies
118118
# Rebuild some test fixtures used in the test suite.
119119
_rebuild-test-fixtures:
120120
cd "{{ fixture_projects}}/Example/" && lake build
121-
cd "{{ fixture_projects }}/WithWidgets/" && lake build && lake build ProofWidgets.Demos ImportGraph.Tools Mathlib.Tactic.Widget.Conv Mathlib.Tactic.Widget.InteractiveUnfold
121+
cd "{{ fixture_projects }}/WithWidgets/" && lake build && lake build ProofWidgets.Demos ImportGraph.Tools Mathlib.Tactic.Widget.Conv Mathlib.Tactic.ClickSuggestions

‎spec/filter_hypothesis_custom_spec.lua‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ describe(
2121
function()
2222
it('filters hypotheses', function()
2323
assert.infoview_contents_at('eft').are [[
24-
case h
2524
⊢ n = n
2625
c : 4 = 4
2726
b : 3 = 3

‎spec/fixtures/projects/Example/Example.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,5 +19,5 @@ theorem has_multiple_goals (n : Nat) : n = n := by
1919

2020
def has_multibyte_character {𝔽 : Type} : 𝔽 = 𝔽 := rfl
2121

22-
def will_be_modified : 37 = 37 := by
22+
theorem will_be_modified : 37 = 37 := by
2323
exact rfl

‎spec/fixtures/projects/Example/lean-toolchain‎

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

‎spec/fixtures/projects/WithWidgets/lake-manifest.json‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "d9874e4268b90436f38b811922d5aff6af138197",
8+
"rev": "d3716e6d2ea114ae7d9f994e5ebf3c064d80c8a7",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "master",
@@ -15,7 +15,7 @@
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "leanprover-community",
18-
"rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
18+
"rev": "e4952ae2afde0dd2868b313356d1ce00da677bd9",
1919
"name": "proofwidgets",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "leanprover-community",
28-
"rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
28+
"rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
2929
"name": "importGraph",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "293af9b2a383eed4d04d66b898d608d0a44b750f",
38+
"rev": "f3c7bd5061bd81b4480295c524d4f245c8b7e4e2",
3939
"name": "plausible",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",
@@ -55,40 +55,40 @@
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
58+
"rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
5959
"name": "aesop",
6060
"manifestFile": "lake-manifest.json",
61-
"inputRev": "v4.30.0-rc2",
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": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
68+
"rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
6969
"name": "Qq",
7070
"manifestFile": "lake-manifest.json",
71-
"inputRev": "v4.30.0-rc2",
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": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
78+
"rev": "9c6e03c0a86237b199ebe6b1fbac18078a767ade",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
81-
"inputRev": "v4.30.0-rc2",
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": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
88+
"rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
8989
"name": "Cli",
9090
"manifestFile": "lake-manifest.json",
91-
"inputRev": "v4.30.0-rc2",
91+
"inputRev": "v4.32.0-rc1",
9292
"inherited": true,
9393
"configFile": "lakefile.toml"}],
9494
"name": "WithWidgets",

‎spec/infoview/auto_diff_pin_spec.lua‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ describe(
3131

3232
-- Two positions with known, distinct goal states.
3333
local pos_inl = { 4, 5 } -- `| inl h37 =>`: case inl goal + expected type
34-
local pos_inl_h = { 5, 5 } -- `apply Or.inr`: case inl.h, ⊢ p
34+
local pos_inl_h = { 5, 5 } -- `apply Or.inr`: case inl, ⊢ p
3535

3636
it('shows previous position in diff when cursor moves', function()
3737
lean_window = Window:current()
@@ -66,7 +66,7 @@ describe(
6666
-- Move to a new position with a different goal.
6767
helpers.move_cursor { to = pos_inl_h }
6868
assert.infoview_contents.are [[
69-
case inl.h
69+
case inl
7070
p q : Prop
7171
h37 : p
7272
⊢ p
@@ -98,7 +98,7 @@ describe(
9898
]]
9999

100100
assert.diff_contents.are [[
101-
case inl.h
101+
case inl
102102
p q : Prop
103103
h37 : p
104104
⊢ p
@@ -123,7 +123,7 @@ describe(
123123

124124
helpers.move_cursor { to = pos_inl_h }
125125
assert.infoview_contents.are [[
126-
case inl.h
126+
case inl
127127
p q : Prop
128128
h37 : p
129129
⊢ p
@@ -168,7 +168,7 @@ describe(
168168
-- Move to pos_inl_h: diff should update to pos_inl.
169169
helpers.move_cursor { to = pos_inl_h }
170170
assert.infoview_contents.are [[
171-
case inl.h
171+
case inl
172172
p q : Prop
173173
h37 : p
174174
⊢ p

‎spec/infoview/autoupdate_spec.lua‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -278,10 +278,14 @@ describe('infoview content (auto-)update', function()
278278
vim.cmd.edit { fixtures.project.child 'Example.lean', bang = true }
279279
helpers.move_cursor { to = { 23, 1 } }
280280
assert.infoview_contents.are [[
281+
Goals accomplished 🎉
282+
281283
⊢ 37 = 37
282284
]]
283-
vim.api.nvim_buf_set_lines(0, 21, 22, true, { 'def will_be_modified : 2 = 2 := by' })
285+
vim.api.nvim_buf_set_lines(0, 21, 22, true, { 'theorem will_be_modified : 2 = 2 := by' })
284286
assert.infoview_contents.are [[
287+
Goals accomplished 🎉
288+
285289
⊢ 2 = 2
286290
]]
287291
end)

‎spec/infoview/contents_spec.lua‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -207,22 +207,28 @@ describe('interactive infoview', function()
207207

208208
it(
209209
'shows goals with multibyte characters',
210-
helpers.clean_buffer([[def multibyte {𝔽 : Type} : 𝔽 = 𝔽 := rfl]], function()
211-
assert.infoview_contents_at({ 1, 48 }).are [[
212-
▼ expected type (1:40-1:43)
210+
helpers.clean_buffer(
211+
[[
212+
set_option linter.defProp false in
213+
def multibyte {𝔽 : Type} : 𝔽 = 𝔽 := rfl
214+
]],
215+
function()
216+
assert.infoview_contents_at({ 2, 48 }).are [[
217+
▼ expected type (2:40-2:43)
213218
𝔽 : Type
214219
⊢ 𝔽 = 𝔽
215220
]]
216221

217-
assert.infoview_contents_at({ 1, 44 }).are [[
222+
assert.infoview_contents_at({ 2, 44 }).are [[
218223
]]
219224

220-
assert.infoview_contents_at({ 1, 46 }).are [[
221-
▼ expected type (1:40-1:43)
225+
assert.infoview_contents_at({ 2, 46 }).are [[
226+
▼ expected type (2:40-2:43)
222227
𝔽 : Type
223228
⊢ 𝔽 = 𝔽
224229
]]
225-
end)
230+
end
231+
)
226232
)
227233

228234
it(

0 commit comments

Comments
 (0)