feat: API to avoid deadlocks from dropped promises

[Kha]

This PR improves the Promise API by considering how dropped promises can lead to never-finished tasks.

[Kha]

@tydeu I regret introduction of this API, it makes it impossible to hide implementation details based on Task.map/bind. This should have been some IO.Ref in Lake itself. But I think we'll survive.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 31bdcea.
There were significant changes against commit 412389f:

  Benchmark                      Metric                  Change
  ========================================================================
- Init.Data.List.Sublist async   instructions              3.1%   (21.8 σ)
- Init.Data.List.Sublist async   maxrss                   42.4%   (12.4 σ)
- Init.Data.List.Sublist async   task-clock               10.6%   (16.1 σ)
- Init.Prelude async             branches                  2.2%   (10.9 σ)
- Init.Prelude async             instructions              4.7%   (21.6 σ)
- big_do                         maxrss                    9.0%  (258.6 σ)
- big_omega.lean                 instructions              1.0%  (114.6 σ)
- big_omega.lean                 maxrss                    7.6%   (73.5 σ)
- big_omega.lean                 task-clock                2.4%   (19.5 σ)
- big_omega.lean                 wall-clock                1.8%   (14.0 σ)
- big_omega.lean MT              instructions              1.2%   (12.2 σ)
- big_omega.lean MT              maxrss                    7.2%  (118.7 σ)
- binarytrees                    instructions              1.2%  (389.0 σ)
- binarytrees.st                 instructions              1.2% (1107.0 σ)
- bv_decide_inequality.lean      maxrss                    4.4%   (15.7 σ)
- bv_decide_mul                  instructions              1.3%  (185.8 σ)
- bv_decide_mul                  maxrss                    1.1%   (25.7 σ)
- bv_decide_realworld            maxrss                    1.5%   (27.5 σ)
- const_fold                     instructions              1.1%   (52.8 σ)
- deriv                          instructions              1.1%   (20.6 σ)
- identifier auto-completion     instructions              1.1%   (14.2 σ)
- ilean roundtrip                instructions              1.4%  (194.6 σ)
- lake build clean               instructions              5.4%   (32.6 σ)
- lake build clean               task-clock               23.4%   (10.6 σ)
- lake build clean               wall-clock               10.1%   (15.2 σ)
- language server startup        branches                  3.1%   (46.5 σ)
- language server startup        instructions              4.5%   (61.7 σ)
- language server startup        maxrss                    8.3%  (357.1 σ)
- language server startup        task-clock                9.0%   (55.8 σ)
- language server startup        wall-clock                1.7%   (11.7 σ)
- parser                         instructions              1.1%  (303.9 σ)
- qsort                          instructions              1.0%  (310.9 σ)
- reduceMatch                    instructions              1.5%   (59.6 σ)
- reduceMatch                    maxrss                    7.0%   (85.2 σ)
- simp_arith1                    instructions              1.1%   (28.6 σ)
- stdlib                         attribute application     4.3%  (145.7 σ)
- stdlib                         instructions              2.5%  (521.7 σ)
- stdlib                         maxrss                    2.6%   (65.5 σ)
- stdlib                         task-clock               10.3%   (40.5 σ)
- stdlib                         wall-clock                3.0%   (72.4 σ)
- tests/bench/ interpreted       maxrss                    3.0%   (73.8 σ)
- unionfind                      instructions              3.3% (1023.0 σ)
- workspaceSymbols               instructions              1.7%  (739.7 σ)
- workspaceSymbols               maxrss                    3.0%   (53.9 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 084eabe.
There were no significant changes against commit 412389f.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 084eabe.
There were no significant changes against commit 412389f.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 36315ff.
There were significant changes against commit 412389f:

  Benchmark        Metric                  Change
  ========================================================
- big_omega.lean   task-clock                1.9% (12.2 σ)
- big_omega.lean   wall-clock                1.9% (12.1 σ)
- stdlib           attribute application     1.7% (12.1 σ)
- stdlib           tactic execution          2.0% (55.9 σ)
- stdlib           type checking             2.5% (90.1 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6958 has successfully built against this PR. (2025-02-05 19:02:18) View Log
• 🟡 Mathlib branch lean-pr-testing-6958 build against this PR was cancelled. (2025-02-05 19:39:17) View Log
• ✅ Mathlib branch lean-pr-testing-6958 has successfully built against this PR. (2025-02-05 20:21:38) View Log
• ✅ Mathlib branch lean-pr-testing-6958 has successfully built against this PR. (2025-02-06 09:49:51) View Log
• ✅ Mathlib branch lean-pr-testing-6958 has successfully built against this PR. (2025-02-06 12:01:20) View Log
• 🟡 Mathlib branch lean-pr-testing-6958 build this PR didn't complete normally. (2025-02-06 13:27:09) View Log
• ✅ Mathlib branch lean-pr-testing-6958 has successfully built against this PR. (2025-02-06 14:39:40) View Log
• ✅ Mathlib branch lean-pr-testing-6958 has successfully built against this PR. (2025-02-06 18:31:30) View Log
• ✅ Mathlib branch lean-pr-testing-6958 has successfully built against this PR. (2025-02-07 10:46:12) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1248a55d32f5fc64c7a26cd606fdf4c2908ce09c --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-07 12:53:44)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 36315ff.
There were significant changes against commit 412389f:

  Benchmark        Metric                  Change
  ========================================================
- big_omega.lean   task-clock                1.9% (12.2 σ)
- big_omega.lean   wall-clock                1.9% (12.1 σ)
- stdlib           attribute application     1.7% (12.1 σ)
- stdlib           tactic execution          2.0% (55.9 σ)
- stdlib           type checking             2.5% (90.1 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5109a6a.
There were significant changes against commit 412389f:

  Benchmark                 Metric       Change
  ========================================================
+ ilean roundtrip           parse         -7.5%  (-17.5 σ)
+ lake build no-op          task-clock    -2.7%  (-12.7 σ)
+ language server startup   wall-clock    -1.0% (-113.5 σ)
- stdlib                    wall-clock     1.1%  (288.4 σ)

[leanprover-bot]

Here are the benchmark results for commit 9acc17c.
There were significant changes against commit b01ca8e:

  Benchmark                      Metric                 Change
  =======================================================================
- Init.Data.List.Sublist async   instructions             1.4%  (158.5 σ)
- Init.Prelude async             instructions             1.9%  (134.4 σ)
- big_do                         task-clock               4.1%   (15.1 σ)
- big_do                         wall-clock               4.2%   (15.5 σ)
+ big_omega.lean MT              maxrss                  -1.3%  (-18.7 σ)
+ big_omega.lean MT              task-clock              -2.6%  (-71.2 σ)
+ big_omega.lean MT              wall-clock              -2.5%  (-63.7 σ)
- binarytrees                    instructions             1.2%  (678.6 σ)
- binarytrees.st                 instructions             1.2%  (585.7 σ)
- bv_decide_mul                  instructions             1.2%  (156.6 σ)
+ bv_decide_realworld            task-clock              -3.3%  (-10.3 σ)
+ bv_decide_realworld            wall-clock              -1.5%  (-42.0 σ)
- const_fold                     instructions             1.1%   (36.9 σ)
- deriv                          instructions             1.1%   (26.4 σ)
- identifier auto-completion     instructions             1.1%   (13.3 σ)
- ilean roundtrip                instructions             1.3%  (106.2 σ)
+ import Lean                    task-clock              -6.7%  (-47.3 σ)
+ import Lean                    wall-clock              -6.6%  (-54.5 σ)
- lake build clean               instructions             2.0%   (22.4 σ)
- lake build clean               maxrss                  15.5%   (22.3 σ)
+ lake build clean               task-clock             -10.2%  (-44.3 σ)
- lake config elab               instructions             1.2%   (45.1 σ)
+ language server startup        maxrss                  -1.4%  (-15.3 σ)
- parser                         instructions             1.1% (1832.2 σ)
+ parser                         task-clock              -3.3%  (-33.3 σ)
+ parser                         wall-clock              -3.3%  (-31.9 σ)
- qsort                          instructions             1.0%  (203.4 σ)
+ rbmap                          task-clock              -6.7%  (-11.0 σ)
+ rbmap                          wall-clock              -6.7%  (-10.6 σ)
+ stdlib                         instantiate metavars    -5.7% (-118.8 σ)
+ stdlib                         type checking           -1.0%  (-34.6 σ)
- unionfind                      instructions             3.3% (1259.1 σ)
- workspaceSymbols               instructions             1.3%  (408.9 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 59ab103.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit aedf808.
There were significant changes against commit b01ca8e:

  Benchmark                 Metric                 Change
  =================================================================
+ big_omega.lean MT         maxrss                  -1.3% (-22.3 σ)
+ lake build clean          task-clock             -10.4% (-16.2 σ)
+ language server startup   maxrss                  -1.6% (-57.5 σ)
+ stdlib                    instantiate metavars    -3.6% (-15.3 σ)

[Kha]

!bench

[Kha]

@digama0 This change may be relevant for lean4tar. Though it shouldn't break anything immediately as at least core is unlikely to store any promises in .oleans.

[leanprover-bot]

Here are the benchmark results for commit bb23bfb.
There were significant changes against commit 1248a55:

  Benchmark                      Metric             Change
  ==================================================================
- Init.Data.List.Sublist async   task-clock           1.1% (844.5 σ)
- Init.Prelude async             branches             1.0%  (96.6 σ)
- Init.Prelude async             instructions         1.1% (109.1 σ)
+ big_do                         task-clock          -7.9% (-17.9 σ)
+ big_do                         wall-clock          -7.9% (-18.0 σ)
- big_omega.lean MT              task-clock           5.5%  (21.1 σ)
- big_omega.lean MT              wall-clock           5.5%  (21.2 σ)
- ilean roundtrip                parse                4.8%  (10.3 σ)
- lake config elab               task-clock           3.3%  (11.5 σ)
- lake config elab               wall-clock           3.4%  (10.7 σ)
- liasolver                      task-clock           4.7%  (12.5 σ)
- liasolver                      wall-clock           4.8%  (11.4 σ)
- stdlib                         fix level params     1.4%  (11.7 σ)