Skip to content

Commit 7972b55

Browse files
mfornetmfornet
authored
Upgrade Lean to 4.32.2 (#164)
1 parent aa52510 commit 7972b55

21 files changed

Lines changed: 58 additions & 67 deletions

File tree

‎codelib/CodeLib/RustStd/U64/AbsDiff.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -359,7 +359,6 @@ theorem absDiffGlobals_pointsTo [WasmGlobalGS] :
359359
unfold absDiffGlobals
360360
rw [(BI.BigSepM.bigSepM_insert (get?_empty 0)).to_eq,
361361
BI.BigSepM.bigSepM_empty.to_eq, BI.sep_emp.to_eq]
362-
exact .rfl
363362

364363
theorem absDiffBodyHeap_agrees
365364
(runtimeModule : Module) (initial : Store Unit)

‎codelib/CodeLib/SepLogic/SmallStepAdequacy.lean‎

Lines changed: 5 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -294,7 +294,7 @@ theorem wasm_smallStep_runtime_adequacy
294294
imod (iOwn_alloc (E := runtimeElem)
295295
(runtimeValue • runtimeValue) (fun n =>
296296
CMRA.valid_iff_validN.mp
297-
(Agree.toAgree_op_valid_iff_equiv.mpr .rfl) n)) with
297+
(toAgree_op_valid_iff_eq.mpr rfl) n)) with
298298
⟨%runtimeName, Hruntime⟩
299299
letI runtimeGS : WasmRuntimeModuleGS :=
300300
{ runtimeElem
@@ -530,7 +530,7 @@ theorem wasm_smallStep_heap_globals_runtime_adequacy
530530
imod (iOwn_alloc (E := runtimeElem)
531531
(runtimeValue • runtimeValue) (fun n =>
532532
CMRA.valid_iff_validN.mp
533-
(Agree.toAgree_op_valid_iff_equiv.mpr .rfl) n)) with
533+
(toAgree_op_valid_iff_eq.mpr rfl) n)) with
534534
⟨%runtimeName, Hruntime⟩
535535
letI runtimeGS : WasmRuntimeModuleGS :=
536536
{ runtimeElem
@@ -656,7 +656,7 @@ theorem wasm_smallStep_heap_globals_runtime_store_adequacy
656656
imod (iOwn_alloc (E := runtimeElem)
657657
(runtimeValue • runtimeValue) (fun n =>
658658
CMRA.valid_iff_validN.mp
659-
(Agree.toAgree_op_valid_iff_equiv.mpr .rfl) n)) with
659+
(toAgree_op_valid_iff_eq.mpr rfl) n)) with
660660
⟨%runtimeName, Hruntime⟩
661661
letI runtimeGS : WasmRuntimeModuleGS :=
662662
{ runtimeElem
@@ -814,7 +814,7 @@ theorem wasm_smallStep_heap_globals_segments_runtime_store_adequacy
814814
imod (iOwn_alloc (E := runtimeElem)
815815
(runtimeValue • runtimeValue) (fun n =>
816816
CMRA.valid_iff_validN.mp
817-
(Agree.toAgree_op_valid_iff_equiv.mpr .rfl) n)) with
817+
(toAgree_op_valid_iff_eq.mpr rfl) n)) with
818818
⟨%runtimeName, Hruntime⟩
819819
letI runtimeGS : WasmRuntimeModuleGS :=
820820
{ runtimeElem
@@ -993,7 +993,7 @@ theorem wasm_smallStep_heap_globals_segments_tables_runtime_store_adequacy
993993
imod (iOwn_alloc (E := runtimeElem)
994994
(runtimeValue • runtimeValue) (fun n =>
995995
CMRA.valid_iff_validN.mp
996-
(Agree.toAgree_op_valid_iff_equiv.mpr .rfl) n)) with
996+
(toAgree_op_valid_iff_eq.mpr rfl) n)) with
997997
⟨%runtimeName, Hruntime⟩
998998
letI runtimeGS : WasmRuntimeModuleGS :=
999999
{ runtimeElem
@@ -1227,7 +1227,6 @@ private theorem global0Heap_pointsTo [WasmGlobalGS] :
12271227
unfold global0Heap
12281228
rw [(BI.BigSepM.bigSepM_insert (get?_empty 0)).to_eq,
12291229
BI.BigSepM.bigSepM_empty.to_eq, BI.sep_emp.to_eq]
1230-
exact .rfl
12311230

12321231
/-- A concrete adequacy witness for authoritative globals: the WP may derive
12331232
the result of `global.get 0` only from ownership allocated for the matching
@@ -2538,8 +2537,6 @@ private theorem memoryInitDropSegments_pointsTo [WasmDataSegmentGS] :
25382537
unfold memoryInitDropSegments
25392538
rw [(BI.BigSepM.bigSepM_insert (get?_empty 0)).to_eq,
25402539
BI.BigSepM.bigSepM_empty.to_eq, BI.sep_emp.to_eq]
2541-
iintro Hsegment
2542-
iexact Hsegment
25432540

25442541
def memoryInitDropAdequacyModule : Module :=
25452542
{ funcs :=
@@ -2644,8 +2641,6 @@ private theorem tableSetGetMap_pointsTo [WasmTableGS] :
26442641
unfold tableSetGetMap
26452642
rw [(BI.BigSepM.bigSepM_insert (get?_empty 0)).to_eq,
26462643
BI.BigSepM.bigSepM_empty.to_eq, BI.sep_emp.to_eq]
2647-
iintro Htable
2648-
iexact Htable
26492644

26502645
def tableSetGetAdequacyModule : Module :=
26512646
{ funcs :=
@@ -2997,8 +2992,6 @@ private theorem tableCopyOverlapMap_pointsTo [WasmTableGS] :
29972992
unfold tableCopyOverlapMap
29982993
rw [(BI.BigSepM.bigSepM_insert (get?_empty 0)).to_eq,
29992994
BI.BigSepM.bigSepM_empty.to_eq, BI.sep_emp.to_eq]
3000-
iintro Htable
3001-
iexact Htable
30022995

30032996
def tableCopyOverlapAdequacyModule : Module :=
30042997
{ funcs := [{ body := [] }, { body := [] }, { body := [] }]
@@ -3344,8 +3337,6 @@ private theorem tableInitDropTableMap_pointsTo [WasmTableGS] :
33443337
unfold tableInitDropTableMap
33453338
rw [(BI.BigSepM.bigSepM_insert (get?_empty 0)).to_eq,
33463339
BI.BigSepM.bigSepM_empty.to_eq, BI.sep_emp.to_eq]
3347-
iintro Htable
3348-
iexact Htable
33493340

33503341
private theorem tableInitDropElementMap_pointsTo [WasmElementSegmentGS] :
33513342
([∗map] index ↦ value ∈ tableInitDropElementMap,
@@ -3354,8 +3345,6 @@ private theorem tableInitDropElementMap_pointsTo [WasmElementSegmentGS] :
33543345
unfold tableInitDropElementMap
33553346
rw [(BI.BigSepM.bigSepM_insert (get?_empty 0)).to_eq,
33563347
BI.BigSepM.bigSepM_empty.to_eq, BI.sep_emp.to_eq]
3357-
iintro Hsegment
3358-
iexact Hsegment
33593348

33603349
def tableInitDropAdequacyModule : Module :=
33613350
{ funcs := [{ body := [] }]

‎codelib/lake-manifest.json‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": "Iris",
77
"scope": "",
8-
"rev": "c2485783af2626575d171398c86cea8b3a6e79ad",
8+
"rev": "a1c07545e3354645bbbb20045607e2f71462a1e7",
99
"name": "iris",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": null,
@@ -42,10 +42,10 @@
4242
"type": "git",
4343
"subDir": null,
4444
"scope": "leanprover-community",
45-
"rev": "81a5d257c8e410db227a6665ed08f64fea08e997",
45+
"rev": "905b95818eb32af7874a58b427f50c1711a5e96c",
4646
"name": "mathlib",
4747
"manifestFile": "lake-manifest.json",
48-
"inputRev": "v4.32.0",
48+
"inputRev": "v4.32.2",
4949
"inherited": true,
5050
"configFile": "lakefile.lean"},
5151
{"url": "https://github.com/leanprover-community/plausible",

‎codelib/lean-toolchain‎

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

‎docbuild/lake-manifest.json‎

Lines changed: 34 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@
1212
"type": "git",
1313
"subDir": null,
1414
"scope": "leanprover",
15-
"rev": "092d6318789e7bb9160ade1e85bdbcc0abfd7f6e",
15+
"rev": "1d0643dd819f8ca71b1dd82cba6e3e3050f0a255",
1616
"name": "«doc-gen4»",
1717
"manifestFile": "lake-manifest.json",
18-
"inputRev": "092d6318789e7bb9160ade1e85bdbcc0abfd7f6e",
18+
"inputRev": "v4.32.2",
1919
"inherited": false,
2020
"configFile": "lakefile.lean"},
2121
{"type": "path",
@@ -75,21 +75,51 @@
7575
"inputRev": "main",
7676
"inherited": true,
7777
"configFile": "lakefile.lean"},
78+
{"url": "https://github.com/leanprover-community/iris-lean.git",
79+
"type": "git",
80+
"subDir": "Iris",
81+
"scope": "",
82+
"rev": "a1c07545e3354645bbbb20045607e2f71462a1e7",
83+
"name": "iris",
84+
"manifestFile": "lake-manifest.json",
85+
"inputRev": null,
86+
"inherited": true,
87+
"configFile": "lakefile.toml"},
7888
{"type": "path",
7989
"scope": "",
8090
"name": "WasmInterpreterLean",
8191
"manifestFile": "lake-manifest.json",
8292
"inherited": true,
8393
"dir": "../programs/lean/../../codelib/../interpreter",
8494
"configFile": "lakefile.toml"},
95+
{"url": "https://github.com/leanprover-community/batteries",
96+
"type": "git",
97+
"subDir": null,
98+
"scope": "leanprover-community",
99+
"rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
100+
"name": "batteries",
101+
"manifestFile": "lake-manifest.json",
102+
"inputRev": "v4.32.0",
103+
"inherited": true,
104+
"configFile": "lakefile.toml"},
105+
{"url": "https://github.com/leanprover-community/quote4",
106+
"type": "git",
107+
"subDir": null,
108+
"scope": "leanprover-community",
109+
"rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
110+
"name": "Qq",
111+
"manifestFile": "lake-manifest.json",
112+
"inputRev": "v4.32.0",
113+
"inherited": true,
114+
"configFile": "lakefile.toml"},
85115
{"url": "https://github.com/leanprover-community/mathlib4",
86116
"type": "git",
87117
"subDir": null,
88118
"scope": "leanprover-community",
89-
"rev": "81a5d257c8e410db227a6665ed08f64fea08e997",
119+
"rev": "905b95818eb32af7874a58b427f50c1711a5e96c",
90120
"name": "mathlib",
91121
"manifestFile": "lake-manifest.json",
92-
"inputRev": "v4.32.0",
122+
"inputRev": "v4.32.2",
93123
"inherited": true,
94124
"configFile": "lakefile.lean"},
95125
{"url": "https://github.com/leanprover-community/plausible",
@@ -141,26 +171,6 @@
141171
"manifestFile": "lake-manifest.json",
142172
"inputRev": "master",
143173
"inherited": true,
144-
"configFile": "lakefile.toml"},
145-
{"url": "https://github.com/leanprover-community/quote4",
146-
"type": "git",
147-
"subDir": null,
148-
"scope": "leanprover-community",
149-
"rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
150-
"name": "Qq",
151-
"manifestFile": "lake-manifest.json",
152-
"inputRev": "master",
153-
"inherited": true,
154-
"configFile": "lakefile.toml"},
155-
{"url": "https://github.com/leanprover-community/batteries",
156-
"type": "git",
157-
"subDir": null,
158-
"scope": "leanprover-community",
159-
"rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
160-
"name": "batteries",
161-
"manifestFile": "lake-manifest.json",
162-
"inputRev": "main",
163-
"inherited": true,
164174
"configFile": "lakefile.toml"}],
165175
"name": "docbuild",
166176
"lakeDir": ".lake",

‎docbuild/lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ packagesDir = "../.lake/packages"
66
[[require]]
77
scope = "leanprover"
88
name = "«doc-gen4»"
9-
rev = "092d6318789e7bb9160ade1e85bdbcc0abfd7f6e"
9+
rev = "v4.32.2"
1010

1111
[[require]]
1212
name = "Project"

‎docbuild/lean-toolchain‎

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

‎interpreter/lake-manifest.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "81a5d257c8e410db227a6665ed08f64fea08e997",
8+
"rev": "905b95818eb32af7874a58b427f50c1711a5e96c",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "v4.32.0",
11+
"inputRev": "v4.32.2",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"url": "https://github.com/leanprover-community/plausible",

‎interpreter/lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ packagesDir = "../.lake/packages"
66
[[require]]
77
name = "mathlib"
88
scope = "leanprover-community"
9-
rev = "v4.32.0"
9+
rev = "v4.32.2"
1010

1111
[[lean_lib]]
1212
name = "Interpreter"

‎interpreter/lean-toolchain‎

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

0 commit comments

Comments
 (0)