feat: new snapshot architecture on the cmdline

[Kha]

This is #3014 with cad5cce reverted for testing.

[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)

[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 https://github.com/leanprover/lean4/pull/3106#discussion_r1435177802:

     // 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 https://github.com/leanprover/lean4/pull/3106#pullrequestreview-1794662949, 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 ff000038b3b479adb703d7ca80140505aeb7cb44.Found no runs to compare against.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 3345a74ad16149dfa57320ca041b1582e095b1ae. There were significant changes against commit 66777670e882edde86379fef6914b2938e93b51f:

  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 a08eebd14b5e772fdad4f4d8494e09af73bf1123. There were significant changes against commit 66777670e882edde86379fef6914b2938e93b51f:

  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 68f2d58823efdc429859ed6e1e74e143665d2973. There were significant changes against commit ce73bbe277140201cdb3ad3015c13d01948704b2:

  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 cc2630de3aed0ca65424578e6b161c2be455c623. There were significant changes against commit 6a4159c4a792ed2e74f20aecf73974dc3e314e2c:

  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