Skip to content

Commit ee51205

Browse files
mans0954mans0954
committed
Merge branch 'master' into mans0954/SesquilinearMaps1
2 parents 434f5d7 + b180173 commit ee51205

549 files changed

Lines changed: 9731 additions & 7926 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/bors.yml‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,19 @@ jobs:
161161
lean --version
162162
lake --version
163163
164+
- name: build cache
165+
run: |
166+
lake build cache
167+
168+
- name: prune ProofWidgets .lake
169+
run: |
170+
# The ProofWidgets release contains not just the `.js` (which we need in order to build)
171+
# but also `.oleans`, which may have been built with the wrong toolchain.
172+
# This removes them.
173+
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
174+
rm -rf .lake/packages/proofwidgets/.lake/build/lib
175+
rm -rf .lake/packages/proofwidgets/.lake/build/ir
176+
164177
- name: get cache
165178
run: |
166179
lake exe cache clean
@@ -194,6 +207,7 @@ jobs:
194207
lake exe cache put || (sleep 1; lake exe cache put) || true
195208
env:
196209
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
210+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
197211

198212
- name: check the cache
199213
run: |
@@ -221,6 +235,7 @@ jobs:
221235
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
222236
env:
223237
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
238+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
224239

225240
- name: build counterexamples
226241
run: |
@@ -229,6 +244,7 @@ jobs:
229244
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
230245
env:
231246
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
247+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
232248

233249
- name: check declarations in db files
234250
run: |

‎.github/workflows/build.yml‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -168,6 +168,19 @@ jobs:
168168
lean --version
169169
lake --version
170170
171+
- name: build cache
172+
run: |
173+
lake build cache
174+
175+
- name: prune ProofWidgets .lake
176+
run: |
177+
# The ProofWidgets release contains not just the `.js` (which we need in order to build)
178+
# but also `.oleans`, which may have been built with the wrong toolchain.
179+
# This removes them.
180+
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
181+
rm -rf .lake/packages/proofwidgets/.lake/build/lib
182+
rm -rf .lake/packages/proofwidgets/.lake/build/ir
183+
171184
- name: get cache
172185
run: |
173186
lake exe cache clean
@@ -201,6 +214,7 @@ jobs:
201214
lake exe cache put || (sleep 1; lake exe cache put) || true
202215
env:
203216
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
217+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
204218

205219
- name: check the cache
206220
run: |
@@ -228,6 +242,7 @@ jobs:
228242
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
229243
env:
230244
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
245+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
231246

232247
- name: build counterexamples
233248
run: |
@@ -236,6 +251,7 @@ jobs:
236251
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
237252
env:
238253
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
254+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
239255

240256
- name: check declarations in db files
241257
run: |

‎.github/workflows/build.yml.in‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -147,6 +147,19 @@ jobs:
147147
lean --version
148148
lake --version
149149

150+
- name: build cache
151+
run: |
152+
lake build cache
153+
154+
- name: prune ProofWidgets .lake
155+
run: |
156+
# The ProofWidgets release contains not just the `.js` (which we need in order to build)
157+
# but also `.oleans`, which may have been built with the wrong toolchain.
158+
# This removes them.
159+
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
160+
rm -rf .lake/packages/proofwidgets/.lake/build/lib
161+
rm -rf .lake/packages/proofwidgets/.lake/build/ir
162+
150163
- name: get cache
151164
run: |
152165
lake exe cache clean
@@ -180,6 +193,7 @@ jobs:
180193
lake exe cache put || (sleep 1; lake exe cache put) || true
181194
env:
182195
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
196+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
183197

184198
- name: check the cache
185199
run: |
@@ -207,6 +221,7 @@ jobs:
207221
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
208222
env:
209223
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
224+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
210225

211226
- name: build counterexamples
212227
run: |
@@ -215,6 +230,7 @@ jobs:
215230
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
216231
env:
217232
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
233+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
218234

219235
- name: check declarations in db files
220236
run: |

‎.github/workflows/build_fork.yml‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,19 @@ jobs:
165165
lean --version
166166
lake --version
167167
168+
- name: build cache
169+
run: |
170+
lake build cache
171+
172+
- name: prune ProofWidgets .lake
173+
run: |
174+
# The ProofWidgets release contains not just the `.js` (which we need in order to build)
175+
# but also `.oleans`, which may have been built with the wrong toolchain.
176+
# This removes them.
177+
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
178+
rm -rf .lake/packages/proofwidgets/.lake/build/lib
179+
rm -rf .lake/packages/proofwidgets/.lake/build/ir
180+
168181
- name: get cache
169182
run: |
170183
lake exe cache clean
@@ -198,6 +211,7 @@ jobs:
198211
lake exe cache put || (sleep 1; lake exe cache put) || true
199212
env:
200213
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
214+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
201215

202216
- name: check the cache
203217
run: |
@@ -225,6 +239,7 @@ jobs:
225239
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
226240
env:
227241
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
242+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
228243

229244
- name: build counterexamples
230245
run: |
@@ -233,6 +248,7 @@ jobs:
233248
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
234249
env:
235250
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
251+
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
236252

237253
- name: check declarations in db files
238254
run: |

‎Archive/Arithcc.lean‎

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -303,23 +303,21 @@ theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
303303
304304
Unlike Theorem 1 in the paper, both `map` and the assumption on `t` are explicit.
305305
-/
306-
theorem compiler_correctness :
307-
∀ (map : Identifier → Register) (e : Expr) (ξ : Identifier → Word) (η : State) (t : Register),
308-
(∀ x, read (loc x map) η = ξ x) →
309-
(∀ x, loc x map < t) → outcome (compile map e t) η ≃[t] { η with ac := value e ξ } := by
310-
intro map e ξ η t hmap ht
311-
revert η t
312-
induction e <;> intro η t hmap ht
306+
theorem compiler_correctness
307+
(map : Identifier → Register) (e : Expr) (ξ : Identifier → Word) (η : State) (t : Register)
308+
(hmap : ∀ x, read (loc x map) η = ξ x) (ht : ∀ x, loc x map < t) :
309+
outcome (compile map e t) η ≃[t] { η with ac := value e ξ } := by
310+
induction e generalizing η t with
313311
-- 5.I
314-
case const => simp [StateEq, step]; rfl
312+
| const => simp [StateEq, step]; rfl
315313
-- 5.II
316-
case var =>
314+
| var =>
317315
simp [hmap, StateEq, step] -- Porting note: was `finish [hmap, StateEq, step]`
318316
constructor
319317
· simp_all only [read, loc]
320318
· rfl
321319
-- 5.III
322-
case sum =>
320+
| sum =>
323321
rename_i e_s₁ e_s₂ e_ih_s₁ e_ih_s₂
324322
simp
325323
generalize value e_s₁ ξ = ν₁ at e_ih_s₁ ⊢

‎Archive/Imo/Imo1962Q1.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -145,11 +145,11 @@ theorem satisfied_by_153846 : ProblemPredicate 153846 := by
145145
#align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
146146

147147
theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by
148-
cases' without_digits h1 with c h2
148+
have ⟨c, h2⟩ := without_digits h1
149149
have h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6 := by apply lt_or_ge
150-
cases' h3 with h3 h3
151-
case inr => exact case_more_digits h3 h2
152-
case inl =>
150+
cases h3 with
151+
| inr h3 => exact case_more_digits h3 h2
152+
| inl h3 =>
153153
interval_cases h : (digits 10 c).length
154154
· exfalso; exact case_0_digit h h2
155155
· exfalso; exact case_1_digit h h2

‎Archive/Imo/Imo1981Q3.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -207,5 +207,5 @@ theorem imo1981_q3 : IsGreatest (specifiedSet 1981) 3524578 := by
207207
apply this
208208
· decide
209209
· decide
210-
· norm_num [ProblemPredicate_iff]; decide
210+
· norm_num [problemPredicate_iff]; decide
211211
#align imo1981_q3 imo1981_q3

‎Cache/IO.lean‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -286,7 +286,7 @@ def allExist (paths : List (FilePath × Bool)) : IO Bool := do
286286
pure true
287287

288288
/-- Compresses build files into the local cache and returns an array with the compressed files -/
289-
def packCache (hashMap : HashMap) (overwrite : Bool) (comment : Option String := none) :
289+
def packCache (hashMap : HashMap) (overwrite verbose : Bool) (comment : Option String := none) :
290290
IO $ Array String := do
291291
mkDir CACHEDIR
292292
IO.println "Compressing cache"
@@ -305,10 +305,14 @@ def packCache (hashMap : HashMap) (overwrite : Bool) (comment : Option String :=
305305
| unreachable!
306306
runCmd (← getLeanTar) $ #[zipPath.toString, trace] ++
307307
(if let some c := comment then #["-c", s!"git=mathlib4@{c}"] else #[]) ++ args
308-
acc := acc.push zip
308+
acc := acc.push (path, zip)
309309
for task in tasks do
310310
_ ← IO.ofExcept task.get
311-
return acc
311+
acc := acc.qsort (·.1.1 < ·.1.1)
312+
if verbose then
313+
for (path, zip) in acc do
314+
println! "packing {path} as {zip}"
315+
return acc.map (·.2)
312316

313317
/-- Gets the set of all cached files -/
314318
def getLocalCacheSet : IO $ Lean.RBTree String compare := do
@@ -347,12 +351,6 @@ def unpackCache (hashMap : HashMap) (force : Bool) : IO Unit := do
347351
IO.println s!"unpacked in {(← IO.monoMsNow) - now} ms"
348352
else IO.println "No cache files to decompress"
349353

350-
/-- Retrieves the azure token from the environment -/
351-
def getToken : IO String := do
352-
let some token ← IO.getEnv "MATHLIB_CACHE_SAS"
353-
| throw $ IO.userError "environment variable MATHLIB_CACHE_SAS must be set to upload caches"
354-
return token
355-
356354
instance : Ord FilePath where
357355
compare x y := compare x.toString y.toString
358356

‎Cache/Main.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -86,16 +86,16 @@ def main (args : List String) : IO Unit := do
8686
getFiles (← hashMemo.filterByFilePaths (toPaths args)) true true goodCurl true
8787
| "get-" :: args =>
8888
getFiles (← hashMemo.filterByFilePaths (toPaths args)) false false goodCurl false
89-
| ["pack"] => discard $ packCache hashMap false (← getGitCommitHash)
90-
| ["pack!"] => discard $ packCache hashMap true (← getGitCommitHash)
89+
| ["pack"] => discard $ packCache hashMap false false (← getGitCommitHash)
90+
| ["pack!"] => discard $ packCache hashMap true false (← getGitCommitHash)
9191
| ["unpack"] => unpackCache hashMap false
9292
| ["unpack!"] => unpackCache hashMap true
9393
| ["clean"] =>
9494
cleanCache $ hashMap.fold (fun acc _ hash => acc.insert $ CACHEDIR / hash.asLTar) .empty
9595
| ["clean!"] => cleanCache
9696
-- We allow arguments for `put` and `put!` so they can be added to the `roots`.
97-
| "put" :: _ => putFiles (← packCache hashMap false (← getGitCommitHash)) false (← getToken)
98-
| "put!" :: _ => putFiles (← packCache hashMap false (← getGitCommitHash)) true (← getToken)
97+
| "put" :: _ => putFiles (← packCache hashMap false true (← getGitCommitHash)) false (← getToken)
98+
| "put!" :: _ => putFiles (← packCache hashMap false true (← getGitCommitHash)) true (← getToken)
9999
| ["commit"] =>
100100
if !(← isGitStatusClean) then IO.println "Please commit your changes first" return else
101101
commit hashMap false (← getToken)

0 commit comments

Comments
 (0)