draft: decl check

[datokrat]

No description provided.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for cf12c6b against cdc3486 are in. No significant results found. @datokrat

• 🟥 build//instructions: +596.6M (+0.01%)

Small changes (3🟥)

• 🟥 build/module/Lean.AddDecl//instructions: +923.7M (+15.18%) (reduced significance based on *//lines)
• 🟥 build/module/LeanChecker//instructions: +17.4M (+0.74%)
• 🟥 mvcgen/sym/AddSubCancelDeep/700/kernel//wall-clock: +16ms (+5.00%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-06-18 09:05:41)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-14101 build failed against this PR. (2026-06-18 09:11:23) View Log

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 9817d0f against cdc3486 are in. There are significant results. @datokrat

• 🟥 build//instructions: +113.2G (+1.00%)
• 🟥 other exited with code 1

Large changes (2🟥)

• 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +5.7G (+2.98%)
• 🟥 build/profile/type checking//wall-clock: +29s (+24.94%)

Medium changes (25🟥)

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

Small changes (482🟥)

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

[datokrat]

!radar

[leanprover-radar]

Benchmark results for e565a03 against cdc3486 are in. There are significant results. @datokrat

• 🟥 build//instructions: +64.7G (+0.57%)

Large changes (1🟥)

• 🟥 build/profile/type checking//wall-clock: +18s (+15.73%)

Medium changes (17🟥)

• 🟥 build/module/Std.Data.DHashMap.Lemmas//instructions: +1.3G (+2.53%)
• 🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.4G (+1.04%)
• 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +3.2G (+1.69%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.DTreeMap.Lemmas//instructions: +1.6G (+2.83%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: +1.6G (+2.35%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.ExtDHashMap.Lemmas//instructions: +1.3G (+2.65%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.ExtDTreeMap.Lemmas//instructions: +1.4G (+2.91%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.ExtTreeMap.Lemmas//instructions: +1.1G (+3.79%)
• 🟥 build/module/Std.Data.HashMap.Lemmas//instructions: +1.0G (+3.24%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.Internal.List.Associative//instructions: +1.5G (+1.91%)
• 🟥 build/module/Std.Data.TreeMap.Lemmas//instructions: +1.2G (+3.88%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.TreeMap.Raw.Lemmas//instructions: +1.2G (+3.06%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Do.Triple.SpecLemmas//instructions: +1.7G (+6.35%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Internal.Do.Triple.SpecLemmas//instructions: +1.4G (+8.48%) (reduced significance based on absolute threshold)
• 🟥 elab/simp_congr//instructions: +236.7M (+2.50%)
• 🟥 misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: +1.9G (+0.84%)
• 🟥 misc/import Std.Data.Internal.List.Associative//instructions: +1.6G (+2.25%)

Small changes (324🟥)

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

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 24db27d against 659e8bb are in. There are significant results. @datokrat

• 🟥 build//instructions: +81.9G (+0.73%)

Large changes (40✅, 16🟥)

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

Medium changes (10✅, 19🟥)

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

Small changes (244✅, 406🟥)

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

[datokrat]

!radar

[leanprover-radar]

Benchmark results for 24db27d against 7559185 are in. There are significant results. @datokrat

• 🟥 build//instructions: +59.4G (+0.52%)

Large changes (1🟥)

• 🟥 build/profile/type checking//wall-clock: +15s (+13.38%)

Medium changes (15🟥)

• 🟥 build/module/Std.Data.DHashMap.Lemmas//instructions: +1.3G (+2.57%)
• 🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.4G (+1.04%)
• 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +3.2G (+1.68%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.DTreeMap.Lemmas//instructions: +1.6G (+2.81%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: +1.6G (+2.40%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.ExtDHashMap.Lemmas//instructions: +1.3G (+2.65%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.ExtDTreeMap.Lemmas//instructions: +1.4G (+2.94%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.ExtTreeMap.Lemmas//instructions: +1.1G (+3.84%)
• 🟥 build/module/Std.Data.HashMap.Lemmas//instructions: +1.0G (+3.24%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.Internal.List.Associative//instructions: +1.5G (+1.98%)
• 🟥 build/module/Std.Data.TreeMap.Lemmas//instructions: +1.2G (+3.94%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Data.TreeMap.Raw.Lemmas//instructions: +1.2G (+3.08%) (reduced significance based on absolute threshold)
• 🟥 elab/simp_congr//instructions: +227.3M (+2.41%)
• 🟥 misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: +1.9G (+0.84%)
• 🟥 misc/import Std.Data.Internal.List.Associative//instructions: +1.6G (+2.30%)

Small changes (2✅, 294🟥)

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