[algebraic-dev]

This PR aims to fix some dead locks and memory leaks in Task Manager finalization that affects LibUV finalization.

The task manager currently refuses to schedule more work when finalizing, which is good because otherwise it could cause some weird effects, like Task.get and IO.wait waiting on something that can never finish if they're inside an already running task. Also, if some dedicated task tries to use IO.asTask, it can cause something to be added to m_queues, and when delete g_task_manager frees the buffer, it does not free the tasks or their closures.

[algebraic-dev]

!bench

[leanprover-radar]

Benchmark results for 373723f against 136fe94 are in. There are significant results. @algebraic-dev

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Runner for run build has different system configurations between commits.
• Runner for run other has different system configurations between commits.

• ✅ build//instructions: -8.4G (-0.08%)

Large changes (127✅, 1🟥)

• ✅ build//wall-clock: -2m 15s (-100.00%)
• ✅ compiled/binarytrees.st//wall-clock: -2s (-100.00%)
• ✅ compiled/binarytrees//wall-clock: -392ms (-100.00%)
• ✅ compiled/const_fold//wall-clock: -938ms (-100.00%)
• ✅ compiled/deriv//wall-clock: -501ms (-100.00%)
• ✅ compiled/hashmap//wall-clock: -164ms (-100.00%)
• ✅ compiled/http_server_tcp//wall-clock: -11s (-100.00%)
• ✅ compiled/ilean_roundtrip//wall-clock: -1s (-100.00%)
• ✅ compiled/incr_header_load//wall-clock: -66ms (-100.00%)
• ✅ compiled/incr_header_save//wall-clock: -1s (-100.00%)
• ✅ compiled/io_compute//wall-clock: -2s (-100.00%)
• ✅ compiled/iterators//wall-clock: -17ms (-100.00%)
• ✅ compiled/liasolver//wall-clock: -164ms (-100.00%)
• ✅ compiled/nat_repr//wall-clock: -1s (-100.00%)
• ✅ compiled/parser//wall-clock: -2s (-100.00%)
• ✅ compiled/phashmap//wall-clock: -421ms (-100.00%)
• ✅ compiled/qsort//wall-clock: -1s (-100.00%)
• ✅ compiled/rbmap//wall-clock: -338ms (-100.00%)
• ✅ compiled/rbmap_checkpoint//wall-clock: -1s (-100.00%)
• ✅ compiled/rbmap_checkpoint2//wall-clock: -556ms (-100.00%)
• and 108 more

Medium changes (2🟥)

• 🟥 compiled/liasolver//instructions: +182.8k (+0.01%)
• 🟥 size/all/.cpp//lines: +140.0 (+0.54%)

Small changes (9✅)

• ✅ build/module/Init.Data.String.Slice.Pattern//instructions: -83.6M (-0.89%)
• ✅ build/module/Lean.Meta.Inductive//instructions: -2.6M (-0.36%)
• ✅ compiled/channel//wall-clock: -3s (-100.00%)
• ✅ compiled/hashmap//maxrss: -930kiB (-5.10%)
• ✅ compiled/nat_repr//maxrss: -930kiB (-5.10%)
• ✅ compiled/qsort//maxrss: -953kiB (-5.23%)
• ✅ compiled/select//maxrss: -918kiB (-5.04%)
• ✅ compiled/sigmaIterator//maxrss: -934kiB (-5.12%)
• ✅ lake/inundation/precompileModules/no-op//wall-clock: -368ms (-100.00%)

[algebraic-dev]

!bench

[leanprover-radar]

Benchmark results for 1e6819f against f37a027 are in. There are significant results. @algebraic-dev

• ✅ build//instructions: -315.6M (-0.00%)

Large changes (1🟥)

• 🟥 size/compile/.out//bytes: +24MiB (+0.72%)

Medium changes (1🟥)

• 🟥 size/all/.cpp//lines: +140.0 (+0.54%)

Small changes (2🟥)

• 🟥 compiled/rbmap_checkpoint2//task-clock: +46ms (+8.26%)
• 🟥 compiled/rbmap_checkpoint2//wall-clock: +46ms (+8.19%)