Skip to content

Commit 6756b62

Browse files
pandaman64pandaman64
authored
v4.27.0 (#155)
1 parent b98df20 commit 6756b62

8 files changed

Lines changed: 38 additions & 32 deletions

File tree

‎correctness/RegexCorrectness/Backtracker/Basic.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,28 +15,34 @@ variable {s : String} {σ : Strategy s} {nfa : NFA} {wf : nfa.WellFormed}
1515

1616
theorem done (hn : nfa[state] = .done) : pushNext σ nfa wf startPos stack update state pos = stack := by
1717
rw! [pushNext, hn]
18+
rfl
1819

1920
theorem fail (hn : nfa[state] = .fail) : pushNext σ nfa wf startPos stack update state pos = stack := by
2021
rw! [pushNext, hn]
22+
rfl
2123

2224
theorem epsilon {state' : Nat} (hn : nfa[state] = .epsilon state') :
2325
haveI isLt : state' < nfa.nodes.size := wf.inBounds' state hn
2426
pushNext σ nfa wf startPos stack update state pos = ⟨update, ⟨state', isLt⟩, pos⟩ :: stack := by
2527
rw! [pushNext, hn]
28+
rfl
2629

2730
theorem split {state₁ state₂ : Nat} (hn : nfa[state] = .split state₁ state₂) :
2831
haveI isLt : state₁ < nfa.nodes.size ∧ state₂ < nfa.nodes.size := wf.inBounds' state hn
2932
pushNext σ nfa wf startPos stack update state pos = ⟨update, ⟨state₁, isLt.1⟩, pos⟩ :: ⟨update, ⟨state₂, isLt.2⟩, pos⟩ :: stack := by
3033
rw! [pushNext, hn]
34+
rfl
3135

3236
theorem saveFin {offset : Nat} {state' : Fin nfa.nodes.size} (hn : nfa[state] = .save offset state') :
3337
pushNext σ nfa wf startPos stack update state pos = ⟨σ.write update offset pos.current, state', pos⟩ :: stack := by
3438
rw! [pushNext, hn]
39+
rfl
3540

3641
theorem save {offset state' : Nat} (hn : nfa[state] = .save offset state') :
3742
haveI isLt : state' < nfa.nodes.size := wf.inBounds' state hn
3843
pushNext σ nfa wf startPos stack update state pos = ⟨σ.write update offset pos.current, ⟨state', isLt⟩, pos⟩ :: stack := by
3944
rw! [pushNext, hn]
45+
rfl
4046

4147
theorem anchor_pos {a : Data.Anchor} {state' : Nat} (hn : nfa[state] = .anchor a state') (h : Data.Anchor.test pos.current a) :
4248
haveI isLt : state' < nfa.nodes.size := wf.inBounds' state hn

‎correctness/lake-manifest.json‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,17 +12,17 @@
1212
"type": "git",
1313
"subDir": null,
1414
"scope": "leanprover-community",
15-
"rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
15+
"rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
1616
"name": "mathlib",
1717
"manifestFile": "lake-manifest.json",
18-
"inputRev": "v4.27.0-rc1",
18+
"inputRev": "v4.27.0",
1919
"inherited": false,
2020
"configFile": "lakefile.lean"},
2121
{"url": "https://github.com/leanprover-community/plausible",
2222
"type": "git",
2323
"subDir": null,
2424
"scope": "leanprover-community",
25-
"rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
25+
"rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
2626
"name": "plausible",
2727
"manifestFile": "lake-manifest.json",
2828
"inputRev": "main",
@@ -32,7 +32,7 @@
3232
"type": "git",
3333
"subDir": null,
3434
"scope": "leanprover-community",
35-
"rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
35+
"rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
3636
"name": "LeanSearchClient",
3737
"manifestFile": "lake-manifest.json",
3838
"inputRev": "main",
@@ -42,7 +42,7 @@
4242
"type": "git",
4343
"subDir": null,
4444
"scope": "leanprover-community",
45-
"rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
45+
"rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
4646
"name": "importGraph",
4747
"manifestFile": "lake-manifest.json",
4848
"inputRev": "main",
@@ -52,17 +52,17 @@
5252
"type": "git",
5353
"subDir": null,
5454
"scope": "leanprover-community",
55-
"rev": "ef8377f31b5535430b6753a974d685b0019d0681",
55+
"rev": "c04225ee7c0585effbd933662b3151f01b600e40",
5656
"name": "proofwidgets",
5757
"manifestFile": "lake-manifest.json",
58-
"inputRev": "v0.0.84",
58+
"inputRev": "v0.0.85",
5959
"inherited": true,
6060
"configFile": "lakefile.lean"},
6161
{"url": "https://github.com/leanprover-community/aesop",
6262
"type": "git",
6363
"subDir": null,
6464
"scope": "leanprover-community",
65-
"rev": "fb12f5535c80e40119286d9575c9393562252d21",
65+
"rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
6666
"name": "aesop",
6767
"manifestFile": "lake-manifest.json",
6868
"inputRev": "master",
@@ -72,7 +72,7 @@
7272
"type": "git",
7373
"subDir": null,
7474
"scope": "leanprover-community",
75-
"rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
75+
"rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
7676
"name": "Qq",
7777
"manifestFile": "lake-manifest.json",
7878
"inputRev": "master",
@@ -82,7 +82,7 @@
8282
"type": "git",
8383
"subDir": null,
8484
"scope": "leanprover-community",
85-
"rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
85+
"rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
8686
"name": "batteries",
8787
"manifestFile": "lake-manifest.json",
8888
"inputRev": "main",
@@ -92,10 +92,10 @@
9292
"type": "git",
9393
"subDir": null,
9494
"scope": "leanprover",
95-
"rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
95+
"rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
9696
"name": "Cli",
9797
"manifestFile": "lake-manifest.json",
98-
"inputRev": "v4.27.0-rc1",
98+
"inputRev": "v4.27.0",
9999
"inherited": true,
100100
"configFile": "lakefile.toml"}],
101101
"name": "RegexCorrectness",

‎correctness/lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ defaultTargets = ["RegexCorrectness"]
99
[[require]]
1010
name = "mathlib"
1111
scope = "leanprover-community"
12-
rev = "v4.27.0-rc1"
12+
rev = "v4.27.0"
1313

1414
[[require]]
1515
name = "Regex"

‎correctness/lean-toolchain‎

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

‎docbuild/lake-manifest.json‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover",
8-
"rev": "05bb84181739ecc0897184a3e2906241267bcdfd",
8+
"rev": "01e143329f2f79abbb8559344e836c221ae84cfd",
99
"name": "«doc-gen4»",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "v4.27.0-rc1",
11+
"inputRev": "v4.27.0",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"type": "path",
@@ -22,7 +22,7 @@
2222
"type": "git",
2323
"subDir": null,
2424
"scope": "",
25-
"rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
25+
"rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
2626
"name": "Cli",
2727
"manifestFile": "lake-manifest.json",
2828
"inputRev": "main",
@@ -32,7 +32,7 @@
3232
"type": "git",
3333
"subDir": null,
3434
"scope": "",
35-
"rev": "cff8377dbe50aae42cbd04213d5b3dacf742c3ba",
35+
"rev": "b09d573cbacf5a8e767292e0edeec787a81689ce",
3636
"name": "UnicodeBasic",
3737
"manifestFile": "lake-manifest.json",
3838
"inputRev": "main",
@@ -42,7 +42,7 @@
4242
"type": "git",
4343
"subDir": null,
4444
"scope": "",
45-
"rev": "f3872ff0d82a43e2ab57595524df3934210f2bb9",
45+
"rev": "c8a6a4dae7c7f42949a1058427a75c20447e990f",
4646
"name": "BibtexQuery",
4747
"manifestFile": "lake-manifest.json",
4848
"inputRev": "master",
@@ -69,17 +69,17 @@
6969
"type": "git",
7070
"subDir": null,
7171
"scope": "leanprover-community",
72-
"rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
72+
"rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
7373
"name": "mathlib",
7474
"manifestFile": "lake-manifest.json",
75-
"inputRev": "v4.27.0-rc1",
75+
"inputRev": "v4.27.0",
7676
"inherited": true,
7777
"configFile": "lakefile.lean"},
7878
{"url": "https://github.com/leanprover-community/plausible",
7979
"type": "git",
8080
"subDir": null,
8181
"scope": "leanprover-community",
82-
"rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
82+
"rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
8383
"name": "plausible",
8484
"manifestFile": "lake-manifest.json",
8585
"inputRev": "main",
@@ -89,7 +89,7 @@
8989
"type": "git",
9090
"subDir": null,
9191
"scope": "leanprover-community",
92-
"rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
92+
"rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
9393
"name": "LeanSearchClient",
9494
"manifestFile": "lake-manifest.json",
9595
"inputRev": "main",
@@ -99,7 +99,7 @@
9999
"type": "git",
100100
"subDir": null,
101101
"scope": "leanprover-community",
102-
"rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
102+
"rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
103103
"name": "importGraph",
104104
"manifestFile": "lake-manifest.json",
105105
"inputRev": "main",
@@ -109,17 +109,17 @@
109109
"type": "git",
110110
"subDir": null,
111111
"scope": "leanprover-community",
112-
"rev": "ef8377f31b5535430b6753a974d685b0019d0681",
112+
"rev": "c04225ee7c0585effbd933662b3151f01b600e40",
113113
"name": "proofwidgets",
114114
"manifestFile": "lake-manifest.json",
115-
"inputRev": "v0.0.84",
115+
"inputRev": "v0.0.85",
116116
"inherited": true,
117117
"configFile": "lakefile.lean"},
118118
{"url": "https://github.com/leanprover-community/aesop",
119119
"type": "git",
120120
"subDir": null,
121121
"scope": "leanprover-community",
122-
"rev": "fb12f5535c80e40119286d9575c9393562252d21",
122+
"rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
123123
"name": "aesop",
124124
"manifestFile": "lake-manifest.json",
125125
"inputRev": "master",
@@ -129,7 +129,7 @@
129129
"type": "git",
130130
"subDir": null,
131131
"scope": "leanprover-community",
132-
"rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
132+
"rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
133133
"name": "Qq",
134134
"manifestFile": "lake-manifest.json",
135135
"inputRev": "master",
@@ -139,7 +139,7 @@
139139
"type": "git",
140140
"subDir": null,
141141
"scope": "leanprover-community",
142-
"rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
142+
"rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
143143
"name": "batteries",
144144
"manifestFile": "lake-manifest.json",
145145
"inputRev": "main",

‎docbuild/lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,4 +10,4 @@ path = "../correctness"
1010
[[require]]
1111
scope = "leanprover"
1212
name = "doc-gen4"
13-
rev = "v4.27.0-rc1"
13+
rev = "v4.27.0"

‎docbuild/lean-toolchain‎

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

‎regex/lean-toolchain‎

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

0 commit comments

Comments
 (0)