feat: lazy initialization of closed terms

[hargoniX]

• v1
• feat: lazy initialization of closed terms

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 426b416 against d8fb702 are in! @hargoniX

Large changes (3✅, 13🟥)

• 🟥 Std.Data.DHashMap.Internal.RawLemmas//instructions: +3.5G (+1.3%)
• 🟥 big_beq_rec//instructions: +629.1M (+3.1%)
• 🟥 big_do//instructions: +132.9M (+0.5%)
• 🟥 big_omega.lean MT//instructions: +445.9M (+1.7%)
• 🟥 big_omega.lean//instructions: +451.8M (+1.8%)
• 🟥 binarytrees.st//instructions: +54.8M (+0.1%)
• 🟥 bv_decide_mul//instructions: +1.7G (+3.5%)
• 🟥 charactersIn//instructions: +471.3M (+1.2%)
• 🟥 deriv//instructions: +512.7M (+6.8%)
• ✅ lake startup//instructions: -24.9M (-9.6%)
• ✅ rbmap_library//instructions: -25.6M (-0.2%)
• 🟥 size/install//bytes: +65MiB (+2.7%)
• 🟥 size/libleanshared.so//bytes: +25MiB (+12.4%)
• 🟥 tests/compiler//sum binary sizes: +154.0M (+12.6%)
• ✅ unionfind//instructions: -20.3M (-0.1%)
• 🟥 workspaceSymbols//instructions: +480.0M (+1.8%)

Medium changes (3✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (525✅, 512🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 237d190 against d8fb702 are in! @hargoniX

Large changes (3✅, 13🟥)

• 🟥 Std.Data.DHashMap.Internal.RawLemmas//instructions: +3.5G (+1.3%)
• 🟥 big_beq_rec//instructions: +628.9M (+3.1%)
• 🟥 big_do//instructions: +133.1M (+0.5%)
• 🟥 big_omega.lean MT//instructions: +449.2M (+1.8%)
• 🟥 big_omega.lean//instructions: +450.4M (+1.8%)
• 🟥 binarytrees.st//instructions: +56.3M (+0.1%)
• 🟥 bv_decide_mul//instructions: +1.6G (+3.5%)
• 🟥 charactersIn//instructions: +471.4M (+1.2%)
• 🟥 deriv//instructions: +512.8M (+6.8%)
• ✅ lake startup//instructions: -25.0M (-9.6%)
• ✅ rbmap_library//instructions: -25.9M (-0.2%)
• 🟥 size/install//bytes: +65MiB (+2.7%)
• 🟥 size/libleanshared.so//bytes: +25MiB (+12.4%)
• 🟥 tests/compiler//sum binary sizes: +154.0M (+12.6%)
• ✅ unionfind//instructions: -20.4M (-0.1%)
• 🟥 workspaceSymbols//instructions: +481.7M (+1.9%)

Medium changes (3✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (528✅, 518🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for cd7c706 against d8fb702 are in! @hargoniX

Large changes (4✅, 7🟥)

• 🟥 Std.Data.DHashMap.Internal.RawLemmas//instructions: +4.2G (+1.6%)
• 🟥 big_do//instructions: +115.6M (+0.4%)
• 🟥 binarytrees.st//instructions: +52.8M (+0.1%)
• 🟥 deriv//instructions: +89.6M (+1.2%)
• ✅ lake startup//instructions: -35.4M (-13.7%)
• ✅ language server startup//instructions: -68.4M (-14.7%)
• ✅ rbmap_library//instructions: -36.5M (-0.3%)
• 🟥 size/install//bytes: +68MiB (+2.8%)
• 🟥 size/libleanshared.so//bytes: +21MiB (+10.7%)
• 🟥 tests/compiler//sum binary sizes: +115.8M (+9.4%)
• ✅ unionfind//instructions: -22.8M (-0.1%)

Medium changes (5✅, 16🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (994✅, 352🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 15f5f7d against d8fb702 are in! @hargoniX

Large changes (4✅, 5🟥)

• 🟥 binarytrees.st//instructions: +52.2M (+0.1%)
• 🟥 deriv//instructions: +89.0M (+1.2%)
• ✅ lake startup//instructions: -36.1M (-13.9%)
• ✅ language server startup//instructions: -69.4M (-14.9%)
• ✅ rbmap_library//instructions: -37.3M (-0.3%)
• 🟥 size/install//bytes: +68MiB (+2.8%)
• 🟥 size/libleanshared.so//bytes: +21MiB (+10.8%)
• 🟥 tests/compiler//sum binary sizes: +118.9M (+9.7%)
• ✅ unionfind//instructions: -22.7M (-0.1%)

Medium changes (13✅)

• ✅ Init.Prelude async//instructions: -63.3M (-0.5%)
• ✅ big_do//instructions: -46.6M (-0.2%)
• ✅ grind_ring_5.lean//instructions: -35.4M (-0.4%)
• ✅ hashmap.lean//instructions: -7.1M (-0.2%)
• ✅ iterators (elab)//instructions: -29.8M (-1.0%)
• ✅ iterators (interpreted)//instructions: -27.7M (-0.1%)
• ✅ lake build clean//instructions: -43.9G (-2.0%)
• ✅ lake config tree//instructions: -64.4M (-4.1%)
• ✅ liasolver//instructions: -31.6M (-0.8%)
• ✅ nat_repr//instructions: -732.9M (-17.3%)
• ✅ parser//instructions: -79.8M (-0.2%)
• ✅ workspaceSymbols with new ranges//instructions: -40.6M (-5.2%)
• ✅ workspaceSymbols//instructions: -214.9M (-0.8%)

Small changes (1805✅, 17🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 50bbfe8 against d8fb702 are in! @hargoniX

• 🟥 build exited with code 2
• 🟥 other exited with code 2

No significant changes detected.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 8949017 against d8fb702 are in! @hargoniX

• ✅ build//instructions: -64.4G (-0.5%)

Large changes (4✅, 5🟥)

• 🟥 binarytrees.st//instructions: +133.9M (+0.2%)
• 🟥 deriv//instructions: +88.4M (+1.2%)
• ✅ lake startup//instructions: -37.6M (-14.5%)
• ✅ language server startup//instructions: -72.9M (-15.6%)
• ✅ rbmap_library//instructions: -39.1M (-0.3%)
• 🟥 size/install//bytes: +62MiB (+2.6%)
• 🟥 size/libleanshared.so//bytes: +20MiB (+10.2%)
• 🟥 tests/compiler//sum binary sizes: +98.4M (+8.0%)
• ✅ unionfind//instructions: -23.0M (-0.1%)

Medium changes (15✅)

• ✅ Init.Prelude async//instructions: -66.6M (-0.5%)
• ✅ big_do//instructions: -49.0M (-0.2%)
• ✅ grind_ring_5.lean//instructions: -35.9M (-0.4%)
• ✅ hashmap.lean//instructions: -8.9M (-0.2%)
• ✅ iterators (compiled)//instructions: -2.0M (-0.4%)
• ✅ iterators (elab)//instructions: -32.0M (-1.1%)
• ✅ iterators (interpreted)//instructions: -29.9M (-0.1%)
• ✅ lake build clean//instructions: -47.1G (-2.2%)
• ✅ lake config tree//instructions: -68.3M (-4.3%)
• ✅ liasolver//instructions: -32.6M (-0.8%)
• ✅ nat_repr//instructions: -740.7M (-17.5%)
• ✅ parser//instructions: -83.7M (-0.2%)
• ✅ phashmap.lean//instructions: -70.6M (-0.7%)
• ✅ workspaceSymbols with new ranges//instructions: -29.4M (-3.7%)
• ✅ workspaceSymbols//instructions: -214.4M (-0.8%)

Small changes (1837✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 8c336a9 against 69b058d are in! @hargoniX

• ✅ build//instructions: -75.5G (-0.6%)

Large changes (5✅, 5🟥)

• 🟥 binarytrees.st//instructions: +108.6M (+0.2%)
• 🟥 deriv//instructions: +88.0M (+1.2%)
• ✅ lake startup//instructions: -43.3M (-16.7%)
• ✅ language server startup//instructions: -81.9M (-17.5%)
• ✅ liasolver//instructions: -36.8M (-0.9%)
• ✅ rbmap_library//instructions: -43.1M (-0.3%)
• 🟥 size/install//bytes: +62MiB (+2.6%)
• 🟥 size/libleanshared.so//bytes: +20MiB (+10.1%)
• 🟥 tests/compiler//sum binary sizes: +97.6M (+8.0%)
• ✅ unionfind//instructions: -24.3M (-0.1%)

Medium changes (18✅)

• ✅ Init.Prelude async//instructions: -70.1M (-0.6%)
• ✅ big_do//instructions: -53.9M (-0.2%)
• ✅ bv_decide_rewriter.lean//instructions: -105.4M (-0.9%)
• ✅ grind_ring_5.lean//instructions: -39.4M (-0.4%)
• ✅ hashmap.lean//instructions: -9.3M (-0.2%)
• ✅ identifier auto-completion//instructions: -442.8M (-0.5%)
• ✅ ilean roundtrip//instructions: -82.6M (-0.3%)
• ✅ import Lean//instructions: -26.9M (-1.4%)
• ✅ iterators (compiled)//instructions: -2.3M (-0.5%)
• ✅ iterators (elab)//instructions: -37.1M (-1.2%)
• ✅ iterators (interpreted)//instructions: -34.9M (-0.1%)
• ✅ lake build clean//instructions: -57.7G (-2.7%)
• ✅ lake config tree//instructions: -42.2M (-2.7%)
• ✅ parser//instructions: -85.8M (-0.2%)
• ✅ phashmap.lean//instructions: -109.4M (-1.1%)
• ✅ treemap.lean//instructions: -8.8M (-0.0%)
• ✅ workspaceSymbols with new ranges//instructions: -46.4M (-5.9%)
• ✅ workspaceSymbols//instructions: -214.0M (-0.8%)

Small changes (1919✅, 17🟥)

Too many entries to display here. View the full report on radar instead.