bump to 2023-02-10

Stream: mathlib4

[Gabriel Ebner]

There has been a merge of the 2003 PR. If anybody is overly motivated to work on the bump, feel free to start or steal from my branch.

[Johan Commelin]

@Reid Barton do you by chance have a branch somewhere that bumps (parts of) mathlib4?

[Johan Commelin]

@Gabriel Ebner Thanks for merging 2003! That's awesome!

[Reid Barton]

I think I didn't make much progress beyond Gabriel's bump2003

[Johan Commelin]

Ok, then I'll continue with bump2003

[Johan Commelin]

Ooh, we need to wait for the release of the nightly anyways

[Johan Commelin]

nightly released

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/pull/2188

[Johan Commelin]

Mathlib is building. There were a few regressions, but in total, I don't think it was bad at all.

[Sebastian Ullrich]

Cumulative profile (edit: ignore, see below instead)

'compilation': 40.622243
'compilation new': 35.967108
'dsimp': 0.163423
'elaboration': 131.949339
'import': 117.061900
'initialization': 14.360300
'interpretation': 97.187590
'linting': 6.368045
'norm_num': 0.000258
'parsing': 3.762523
'ring': 0.000012
'simp': 48.144701
'typeclass inference': 264.206892
    Command being timed: "bash -c lake env nix shell github:leanprover/lean4/pull/2097/merge -c zsh -c 'echo Mathlib/**/*.lean | xargs -n1 -P9 lean --profile -Dprofiler.threshold=100000' |& ~/lean/lean/tests/bench/accumulate_profile.py"
    User time (seconds): 1685.62
    System time (seconds): 102.73
    Percent of CPU this job got: 893%
    Elapsed (wall clock) time (h:mm:ss or m:ss): 3:20.22
    Average shared text size (kbytes): 0
    Average unshared data size (kbytes): 0
    Average stack size (kbytes): 0
    Average total size (kbytes): 0
    Maximum resident set size (kbytes): 1226536
    Average resident set size (kbytes): 0
    Major (requiring I/O) page faults: 11179
    Minor (reclaiming a frame) page faults: 42066277
    Voluntary context switches: 11573
    Involuntary context switches: 7521
    Swaps: 0
    File system inputs: 2728
    File system outputs: 328
    Socket messages sent: 0
    Socket messages received: 0
    Signals delivered: 0
    Page size (bytes): 4096
    Exit status: 0

[Sebastian Ullrich]

Compare with master:

'compilation': 173.588834
'compilation new': 86.642312
'dsimp': 5.008818
'elaboration': 1737.619387
'import': 264.284900
'initialization': 31.086600
'interpretation': 905.333030
'linting': 37.893245
'norm_num': 3.297573
'parsing': 19.672510
'ring': 9.192630
'simp': 434.506535
'typeclass inference': 1553.702595
    Command being timed: "bash -c lake env zsh -c 'echo Mathlib/**/*.lean | xargs -n1 -P9 lean --profile -Dprofiler.threshold=100000' |& ~/lean/lean/tests/bench/accumulate_profile.py"
    User time (seconds): 5186.98
    System time (seconds): 110.18
    Percent of CPU this job got: 872%
    Elapsed (wall clock) time (h:mm:ss or m:ss): 10:07.00
    Average shared text size (kbytes): 0
    Average unshared data size (kbytes): 0
    Average stack size (kbytes): 0
    Average total size (kbytes): 0
    Maximum resident set size (kbytes): 4110212
    Average resident set size (kbytes): 0
    Major (requiring I/O) page faults: 3442
    Minor (reclaiming a frame) page faults: 44354368
    Voluntary context switches: 283482
    Involuntary context switches: 23882
    Swaps: 0
    File system inputs: 53320
    File system outputs: 0
    Socket messages sent: 0
    Socket messages received: 0
    Signals delivered: 0
    Page size (bytes): 4096
    Exit status: 0

[Sebastian Ullrich]

(wait a minute, verifying these measures...)

[Eric Wieser]

File system outputs: 0 vs File system outputs: 328?

[Johan Commelin]

@Sebastian Ullrich shouldn't you profile mathlib4:master vs mathlib4:bump-2023-02-10 with their respective lean toolchains?

[Johan Commelin]

github:leanprover/lean4/pull/2097/merge looks a bit suspicious to me

[Sebastian Ullrich]

Yes, I also wanted to include the the fixes to the interpretation metric from that PR. I just verified that the numbers don't really change when using the correct nightly apart from that.

[Johan Commelin]

@Sebastian Ullrich But what about
Eric Wieser said:

File system outputs: 0 vs File system outputs: 328?

[Sebastian Ullrich]

So I don't really understand why everything got faster. But it's clear that many TC bottlenecks got eliminated.

[Sebastian Ullrich]

Note that this is not a dependency-ordered build but parallel check of all Lean files, so the wall clock time is a measure of ideal parallelism. I think I'll redo the numbers with lake build

[Johan Commelin]

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check @Finset.smul_finset_subset_smul_finset_iff₀ /- LINTER FAILED:
simplify fails on left-hand side:
tactic 'simp' failed, nested error:
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit) -/

[Johan Commelin]

variable [DecidableEq β] [GroupWithZero α] [MulAction α β] {s t : Finset β} {a : α} {b : β}

theorem test1.smul_finset_subset_smul_finset_iff₀ (ha : a ≠ 0) : a • s ⊆ a • t ↔ s ⊆ t :=
  by simp [ha] -- timeout, as reported by the linter

theorem test2.smul_finset_subset_smul_finset_iff₀ (ha : a ≠ 0) : a • s ⊆ a • t ↔ s ⊆ t :=
  by simp only [Finset.smul_finset_subset_smul_finset_iff₀ ha] -- instant win

theorem test3.smul_finset_subset_smul_finset_iff₀ (ha : a ≠ 0) : a • s ⊆ a • t ↔ s ⊆ t :=
  by simp only [Finset.smul_finset_subset_smul_finset_iff₀, ha] -- unsolved goals

[Sebastian Ullrich]

lake build on bump-2023-02-10:

'.olean serialization': 37.853540
'C code generation': 1.768435
'compilation': 205.754573
'compilation new': 100.213137
'dsimp': 4.580919
'elaboration': 782.889996
'import': 371.659000
'initialization': 36.916400
'interpretation': 1055.931650
'linting': 44.834213
'norm_num': 0.336515
'parsing': 22.813774
'ring': 0.969340
'simp': 369.390996
'typeclass inference': 1684.782010
    Command being timed: "bash -c lake build -v |& ~/lean/lean/tests/bench/accumulate_profile.py"
    User time (seconds): 4638.28
    System time (seconds): 157.13
    Percent of CPU this job got: 993%
    Elapsed (wall clock) time (h:mm:ss or m:ss): 8:02.85
    Average shared text size (kbytes): 0
    Average unshared data size (kbytes): 0
    Average stack size (kbytes): 0
    Average total size (kbytes): 0
    Maximum resident set size (kbytes): 4128128
    Average resident set size (kbytes): 0
    Major (requiring I/O) page faults: 4733
    Minor (reclaiming a frame) page faults: 48589057
    Voluntary context switches: 368530
    Involuntary context switches: 122021
    Swaps: 0
    File system inputs: 472
    File system outputs: 1624832
    Socket messages sent: 0
    Socket messages received: 0
    Signals delivered: 0
    Page size (bytes): 4096
    Exit status: 0

lake build on master:

'.olean serialization': 37.793700
'C code generation': 1.781041
'compilation': 207.986073
'compilation new': 99.645207
'dsimp': 5.195223
'elaboration': 2007.594839
'elaboration took': 156.000000
'import': 370.157500
'initialization': 37.668100
'interpretation': 1214.664330
'linting': 47.547507
'norm_num': 3.849844
'parsing': 23.782369
'ring': 11.871330
'simp': 544.161378
'typeclass inference': 1907.262770
    Command being timed: "bash -c lake build -v |& ~/lean/lean/tests/bench/accumulate_profile.py"
    User time (seconds): 6442.80
    System time (seconds): 160.61
    Percent of CPU this job got: 953%
    Elapsed (wall clock) time (h:mm:ss or m:ss): 11:32.31
    Average shared text size (kbytes): 0
    Average unshared data size (kbytes): 0
    Average stack size (kbytes): 0
    Average total size (kbytes): 0
    Maximum resident set size (kbytes): 4116644
    Average resident set size (kbytes): 0
    Major (requiring I/O) page faults: 2596
    Minor (reclaiming a frame) page faults: 48789824
    Voluntary context switches: 370295
    Involuntary context switches: 93514
    Swaps: 0
    File system inputs: 80
    File system outputs: 1624616
    Socket messages sent: 0
    Socket messages received: 0
    Signals delivered: 0
    Page size (bytes): 4096
    Exit status: 0

[Sebastian Ullrich]

That looks much more reasonable. I think I know what went wrong above.

[Johan Commelin]

Thanks! That is a slightly more sober but also more realistic report, I guess?

[Johan Commelin]

Still, it's a juicy speedup. Things like norm_num and ring seem 10x faster

[Floris van Doorn]

What is interpretation?

[Sebastian Ullrich]

It is time spent in the interpreter, except that's not true without https://github.com/leanprover/lean4/pull/2097. Profiling with that PR next.

[Sebastian Ullrich]

The accounting is a bit tricky, but I think I got it to work now. Here are two more runs, with and without the interpretation fix

'compilation': 164.714187
'compilation new': 87.103079
'dsimp': 4.474797
'elaboration': 847.785834
'import': 463.646400
'initialization': 30.652100
'interpretation': 684.955990
'linting': 61.308320
'norm_num': 0.293605
'parsing': 19.379258
'ring': 0.617584
'simp': 320.809063
'typeclass inference': 1478.708429

'compilation': 165.137222
'compilation new': 84.167392
'dsimp': 4.273111
'elaboration': 653.229938
'import': 263.245600
'initialization': 31.160300
'interpretation': 817.407900
'linting': 37.820219
'norm_num': 0.304183
'parsing': 19.365134
'ring': 0.769890
'simp': 302.897895
'typeclass inference': 1360.253054

It looks like a good part of elaboration, import (env extensions presumably) and linting was miscounted as interpretation, which makes sense. The increase in TC doesn't, but that may be a fluke.

[Sebastian Ullrich]

So it's probably better to first look at further optimizing TC inference before taking another stab at precompilation. Well, the potential wins with precompilation are likely higher, but how much additional overhead and caching work we would introduce are not clear to me yet.

[Johan Commelin]

Johan Commelin said:

https://github.com/leanprover-community/mathlib4/pull/2188

I don't really understand the regressions in this bump. @Gabriel Ebner the diff is ~38 lines. But it might point to some issues? They must be pretty specific corner cases though, otherwise I would expect to see a lot more problems.

[Floris van Doorn]

Here is a much less detailed overview of the build time of this bump, that clearly shows its impact.

After this bump, the build time of mathlib4 is 39m 44s.
Before this bump, the build time of mathlib4 is 58m43s (this is the average of two builds that make a relatively small change to to_additive, which is imported by almost all files in Mathlib)

[Yury G. Kudryashov]

Elan downloaded Lean 2023-02-10, and there is no bin/

[Yury G. Kudryashov]

(Linux NixOS)

[Yury G. Kudryashov]

Removed, downloaded again, now it works.