feat: new snapshot architecture on the cmdline

[Kha]

No description provided.

[leanprover-community-mathlib4-bot]

• ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-23 14:26:33)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 66777670e882edde86379fef6914b2938e93b51f --onto fe17b82096bf4825d83a36f220d79a6dadebf5c8. (2024-05-27 08:28:51)
• ✅ Mathlib branch lean-pr-testing-3106 has successfully built against this PR. (2024-06-22 11:55:22) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6a4159c4a792ed2e74f20aecf73974dc3e314e2c --onto 8acdafd5b3957382c02779ada451c14da44e2aca. (2024-08-01 13:15:02)
• ✅ Mathlib branch lean-pr-testing-3106 has successfully built against this PR. (2024-08-01 15:15:10) View Log
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-08-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-08-05 15:59:37)

[Kha]

@abentkamp I verified that even on master, the wasm lean gets stuck on this line on task-spawning files such as task_test.lean. No idea why except for general wonkiness of pthread emulation but at least it's not a bug in the new snapshots.

[abentkamp]

There are a couple of restrictions of emscripten pthreads listed here, which might cause this: https://emscripten.org/docs/porting/pthreads.html Unfortunately, I dont think I will have the time to look into this in the near future. Sebastian Ullrich ***@***.***> schrieb am Sa., 23. Dez. 2023, 5:06 PM:

…

***@***.**** commented on this pull request. ------------------------------ In src/runtime/object.cpp <#3106 (comment)>: > // wait for all workers to finish m_worker_finished_cv.wait(lock, [&]() { return m_num_std_workers + m_num_dedicated_workers == 0; }); + // never seems to terminate under Emscripten @abentkamp <https://github.com/abentkamp> I verified that even on master, the wasm lean gets stuck on this line on task-spawning files such as task_test.lean. No idea why except for general wonkiness of pthread emulation but at least it's not a bug in the new snapshots. — Reply to this email directly, view it on GitHub <#3106 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAYFUCOH2XDRYQUHPFJQZZLYK36PHAVCNFSM6AAAAABA6T4S52VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTOOJUGY3DEOJUHE> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit ff00003.Found no runs to compare against.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 3345a74.
There were significant changes against commit 6677767:

  Benchmark                  Metric                  Change
  ====================================================================
- import Lean                branches                  1.0%   (14.3 σ)
- import Lean                instructions              1.1%   (15.6 σ)
- import Lean                maxrss                    1.3%   (23.8 σ)
- lake build clean           instructions              3.2%   (32.6 σ)
- lake build clean           task-clock               17.0%   (16.4 σ)
- language server startup    branch-misses             5.5%   (12.2 σ)
- language server startup    maxrss                   18.6%  (936.2 σ)
- reduceMatch                instructions              2.3%  (334.6 σ)
- reduceMatch                maxrss                   11.5%   (31.3 σ)
- stdlib                     attribute application    10.1%   (82.0 σ)
- stdlib                     dsimp                    20.6%   (61.8 σ)
- stdlib                     instructions              3.9%  (155.1 σ)
- stdlib                     maxrss                   11.2% (1742.1 σ)
- stdlib                     tactic execution         18.9%   (69.5 σ)
- stdlib                     task-clock               17.9%   (17.5 σ)
- stdlib                     type checking             9.8%   (21.8 σ)
- stdlib                     wall-clock               10.7%   (73.8 σ)
- tests/bench/ interpreted   instructions              1.8%  (212.4 σ)
- tests/bench/ interpreted   maxrss                    7.3%   (97.8 σ)
+ tests/bench/ interpreted   task-clock              -21.3%  (-14.9 σ)
- workspaceSymbols           maxrss                    6.6%   (18.2 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit a08eebd.
There were significant changes against commit 6677767:

  Benchmark                  Metric             Change
  ===============================================================
- import Lean                branches             1.0%   (13.5 σ)
- import Lean                instructions         1.1%   (13.8 σ)
- import Lean                maxrss               1.3%   (33.4 σ)
- lake build clean           instructions         3.1%   (27.4 σ)
- lake build clean           task-clock          17.8%   (14.2 σ)
- language server startup    maxrss              18.5%  (627.1 σ)
- language server startup    task-clock          16.3%   (12.0 σ)
- language server startup    wall-clock           7.8%   (10.4 σ)
- reduceMatch                maxrss              11.5%   (31.2 σ)
- stdlib                     dsimp               11.4%   (21.2 σ)
- stdlib                     instructions         2.6%  (163.7 σ)
- stdlib                     maxrss              12.0%  (474.7 σ)
- stdlib                     tactic execution    14.4%  (125.6 σ)
- stdlib                     task-clock          14.9%  (176.8 σ)
- stdlib                     type checking        6.1% (1777.9 σ)
- stdlib                     wall-clock           7.6%   (34.6 σ)
- tests/bench/ interpreted   maxrss               7.2%  (624.7 σ)
+ tests/bench/ interpreted   task-clock         -37.5% (-480.9 σ)
+ tests/bench/ interpreted   wall-clock          -8.8%  (-48.0 σ)
- workspaceSymbols           maxrss               7.3%   (13.0 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 68f2d58.
There were significant changes against commit ce73bbe:

  Benchmark                  Metric             Change
  ===============================================================
- import Lean                branches             1.1%   (14.1 σ)
- import Lean                instructions         1.1%   (14.4 σ)
- import Lean                maxrss               1.3%   (27.9 σ)
- lake build clean           instructions         3.2%   (36.7 σ)
- lake build clean           task-clock          18.2%   (12.9 σ)
- language server startup    maxrss               6.7%  (309.5 σ)
- reduceMatch                instructions         1.1%  (212.4 σ)
- reduceMatch                maxrss               2.1%  (258.8 σ)
- stdlib                     maxrss               2.3% (4277.3 σ)
- tests/bench/ interpreted   maxrss               3.3%  (385.6 σ)
+ tests/bench/ interpreted   task-clock         -36.8%  (-93.5 σ)
+ tests/bench/ interpreted   wall-clock         -10.0%  (-18.3 σ)
- tests/compiler             sum binary sizes    50.1%
- workspaceSymbols           maxrss               2.3%  (323.9 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit cc2630d.
There were significant changes against commit 6a4159c:

  Benchmark                  Metric             Change
  ===============================================================
- import Lean                branches             1.1%   (24.1 σ)
- import Lean                instructions         1.1%   (23.6 σ)
- lake build clean           instructions         2.9%   (15.2 σ)
- lake build clean           task-clock          18.6%   (14.1 σ)
- lake config elab           instructions         1.7%  (132.0 σ)
- lake config elab           maxrss               1.3%   (41.2 σ)
- language server startup    maxrss               6.3%  (366.0 σ)
- reduceMatch                instructions         5.6%  (512.9 σ)
- reduceMatch                maxrss               2.1%  (292.0 σ)
- stdlib                     fix level params     2.5%   (13.5 σ)
- stdlib                     maxrss               2.1%  (244.8 σ)
- tests/bench/ interpreted   instructions         1.8% (2590.9 σ)
- tests/bench/ interpreted   maxrss               3.4%  (389.5 σ)
+ tests/bench/ interpreted   task-clock         -15.5%  (-13.7 σ)
- workspaceSymbols           maxrss               2.3%  (240.6 σ)

[Kha]

Mathlib run is clear http://speed.lean-fro.org/mathlib4/run-detail/0a0c0354-f960-438b-8fa5-117e6e4f15c7

[Kha]

processCommand and the whole FrontendM are not used by Lean itself anymore now but I think it's fine to leave them around as they have some external uses. They just will not benefit from parallelism etc. going forward.