experiment: normalize instances in `inferInstanceAs` by Kha · Pull Request #12895 · leanprover/lean4

Kha · 2026-03-12T11:29:21Z

Experiment based on leanprover-community/mathlib4#36420

Kha · 2026-03-12T11:29:28Z

!bench

leanprover-radar · 2026-03-12T11:29:35Z

Benchmark results for 19f2533 against e804829 are in. Significant changes detected! @Kha

🟥 build//instructions: +3.2T (+24.99%)

Large changes (151🟥)

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

Medium changes (2✅, 243🟥)

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

Small changes (13✅, 471🟥)

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

leanprover-bot · 2026-03-12T12:27:38Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-09 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-03-12 12:27:37)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-17 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-03-17 10:13:50)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-18 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-03-19 05:10:55)

mathlib-lean-pr-testing · 2026-03-12T12:31:44Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12895 build failed against this PR. (2026-03-12 12:31:42) View Log
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-17 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. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-17 10:13:49)

Kha · 2026-03-12T14:02:41Z

!bench

leanprover-radar · 2026-03-12T14:03:49Z

Benchmark results for ed712ff against e804829 are in. There are no significant changes. @Kha

🟥 build//instructions: +3.5G (+0.03%)

Small changes (11✅, 3🟥)

✅ build/module/Init.Control.Lawful.MonadAttach.Instances//instructions: -17.4M (-1.32%)
✅ build/module/Init.Control.StateRef//instructions: -10.3M (-1.56%)
✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap//instructions: -154.1M (-0.33%)
✅ build/module/Init.Data.List.MinMaxOn//instructions: -103.5M (-1.32%)
✅ build/module/Init.Data.Order.MinMaxOn//instructions: -25.5M (-1.24%)
✅ build/module/Init.Data.Order.Ord//instructions: -25.3M (-0.62%)
✅ build/module/Lake.Build.Data//instructions: -29.7M (-0.76%)
🟥 build/module/Lean.Elab.BuiltinTerm//instructions: +207.9M (+1.85%) (reduced significance based on *//lines)
🟥 build/module/Lean.Parser.Term//instructions: +122.5M (+0.71%)
✅ build/module/Lean.Util.MonadCache//instructions: -27.2M (-2.26%)
✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap//instructions: -93.6M (-1.73%) (reduced significance based on absolute threshold)
✅ build/module/Std.Time.Time.Unit.Hour//instructions: -10.7M (-1.39%)
✅ build/module/Std.Time.Time.Unit.Nanosecond//instructions: -14.7M (-1.58%)
🟥 compiled/workspaceSymbolsNewRanges//instructions: +2.8M (+0.38%)

mathlib-lean-pr-testing · 2026-03-12T15:10:37Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12895 build failed against this PR. (2026-03-12 15:10:35) View Log

JovanGerb · 2026-03-12T15:30:20Z

I think it would be a bad idea to replace all instances with their synthesized instance, because it would lead to very confusing behaviour. You would get the following:

instance inst1 : A := X
instance inst2 : A := Y
#print inst2 -- value is `inst1`

I'm not saying it is a good idea to write multiple instances of A, but it is a common thing to do when testing.

Kha · 2026-03-12T15:42:12Z

Yes I limited the normalization to inferInstanceAs for now though it would still be nice to remove the need for fast_instance% as well. I'm not actually sure we want to run trySynthInstance in the general case instead of doing some more restricted "is this already an instance" check but for inferInstanceAs specifically it does seem to be the right thing to do.

mathlib-lean-pr-testing · 2026-03-12T15:47:54Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12895 build failed against this PR. (2026-03-12 15:47:52) View Log

mathlib-lean-pr-testing · 2026-03-12T17:23:56Z

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-12895 built against this PR, but testing failed. (2026-03-12 17:23:54) View Log

Kha · 2026-03-15T12:46:23Z

!bench

leanprover-radar · 2026-03-15T12:46:29Z

Benchmark results for ed712ff against e804829 are in. There are no significant changes. @Kha

🟥 build//instructions: +3.5G (+0.03%)

Small changes (11✅, 3🟥)

✅ build/module/Init.Control.Lawful.MonadAttach.Instances//instructions: -17.4M (-1.32%)
✅ build/module/Init.Control.StateRef//instructions: -10.3M (-1.56%)
✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap//instructions: -154.1M (-0.33%)
✅ build/module/Init.Data.List.MinMaxOn//instructions: -103.5M (-1.32%)
✅ build/module/Init.Data.Order.MinMaxOn//instructions: -25.5M (-1.24%)
✅ build/module/Init.Data.Order.Ord//instructions: -25.3M (-0.62%)
✅ build/module/Lake.Build.Data//instructions: -29.7M (-0.76%)
🟥 build/module/Lean.Elab.BuiltinTerm//instructions: +207.9M (+1.85%) (reduced significance based on *//lines)
🟥 build/module/Lean.Parser.Term//instructions: +122.5M (+0.71%)
✅ build/module/Lean.Util.MonadCache//instructions: -27.2M (-2.26%)
✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap//instructions: -93.6M (-1.73%) (reduced significance based on absolute threshold)
✅ build/module/Std.Time.Time.Unit.Hour//instructions: -10.7M (-1.39%)
✅ build/module/Std.Time.Time.Unit.Nanosecond//instructions: -14.7M (-1.58%)
🟥 compiled/workspaceSymbolsNewRanges//instructions: +2.8M (+0.38%)

mathlib-lean-pr-testing · 2026-03-17T08:42:51Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-12895 build this PR didn't complete normally. (2026-03-17 08:42:50) View Log

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Add three new options (all defaulting to false) for wrapping constructor fields in auxiliary definitions to fix their types: - instance.normalForm.wrapFields.proofs: wraps proof fields via mkAuxTheorem - instance.normalForm.wrapFields.instances: wraps instance fields via mkAuxDefinition marked implicit_reducible - instance.normalForm.wrapFields.data: wraps data fields via mkAuxDefinition Also wrap the normalizeInstance call in withNewMCtxDepth to prevent isDefEq side effects from leaking, matching the Mathlib fast_instance% pattern. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-03-19T05:30:36Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12895 build failed against this PR. (2026-03-19 05:30:35) View Log

mathlib-lean-pr-testing · 2026-03-19T07:30:07Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12895 build failed against this PR. (2026-03-19 07:30:05) View Log

… check

…alizeInstance This PR passes `compile := false` when creating auxiliary definitions inside `normalizeInstance` if the surrounding declaration is noncomputable or we are in a noncomputable section, preventing spurious "Failed to find LCNF signature" errors. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Auxiliary definitions created by normalizeInstance in inferInstanceAs now propagate sorry warnings from the instances they wrap. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-03-19T13:56:29Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12895 build failed against this PR. (2026-03-19 13:56:27) View Log

Kha · 2026-03-22T10:19:35Z

Superseded by #12897

Kha changed the base branch from master to nightly-with-mathlib March 12, 2026 11:29

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 12, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 12, 2026

Update lean-toolchain for testing leanprover/lean4#12895

1c1f045

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Mar 12, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 12, 2026

Update lean-toolchain for testing leanprover/lean4#12895

4e3f4d5

mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 12, 2026

Kha force-pushed the push-zpvupnppupvs branch from f7a410e to ed712ff Compare March 12, 2026 14:02

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 12, 2026

Update lean-toolchain for leanprover/lean4#12895

5e21ae6

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 12, 2026

Update lean-toolchain for leanprover/lean4#12895

9b0732e

Kha mentioned this pull request Mar 12, 2026

feat: adjust instances in inferInstanceAs and def ... deriving #12897

Merged

Kha changed the title ~~experiment: transform all instances into instance normal form~~ experiment: normalize instances in inferInstanceAs Mar 12, 2026

Kha mentioned this pull request Mar 12, 2026

experiment: normalize all instances #12899

Closed

Kha force-pushed the push-zpvupnppupvs branch from ed712ff to c1b6c35 Compare March 17, 2026 08:24

Kha force-pushed the push-zpvupnppupvs branch from c1b6c35 to cb766bd Compare March 17, 2026 09:24

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 17, 2026

Update lean-toolchain for leanprover/lean4#12895

706c654

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 17, 2026

Update lean-toolchain for leanprover/lean4#12895

e94d144

kim-em and others added 3 commits March 19, 2026 03:38

fix tests

b17ae6f

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

fix: remove exceptEmoji usage after refactor in 75cc1c5

33a6067

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

kim-em force-pushed the push-zpvupnppupvs branch from 84ed9ed to 5026406 Compare March 19, 2026 03:39

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2026

Update lean-toolchain for leanprover/lean4#12895

954d280

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 19, 2026

Update lean-toolchain for leanprover/lean4#12895

0a08d1d

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2026

Update lean-toolchain for leanprover/lean4#12895

547f1c0

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 19, 2026

Update lean-toolchain for leanprover/lean4#12895

43949af

Kha and others added 14 commits March 19, 2026 12:28

fix stage 2

fc64232

full steam ahead

3d00251

do everything at instance transparency

3047c66

oops

2c691eb

tighten instance normal form

6eb4e08

add initial actual test

8cb52a1

sometimes we just need to wrap the instance

b09df2f

enable realizations

9a3d455

replace fast_instance instance synth leftover with type compatibility…

6de865f

… check

clean up and clarify

5c5c551

changes to completionOption test output

289ce65

test: update structWithAlgTCSynth expected output for new sorry warnings

7974d0b

Auxiliary definitions created by normalizeInstance in inferInstanceAs now propagate sorry warnings from the instances they wrap. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

tentative fix for the instanceNormalFormExpose problem

eb7e509

Kha force-pushed the push-zpvupnppupvs branch from d055c1a to eb7e509 Compare March 19, 2026 12:47

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 19, 2026

Update lean-toolchain for leanprover/lean4#12895

4200e0a

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 19, 2026

Update lean-toolchain for leanprover/lean4#12895

6d0047b

Kha closed this Mar 22, 2026

Conversation

Kha commented Mar 12, 2026

Uh oh!

Kha commented Mar 12, 2026

Uh oh!

leanprover-radar commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Mar 12, 2026

Uh oh!

leanprover-radar commented Mar 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Mar 12, 2026

Uh oh!

JovanGerb commented Mar 12, 2026

Uh oh!

Kha commented Mar 12, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 12, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 12, 2026

Uh oh!

Kha commented Mar 15, 2026

Uh oh!

leanprover-radar commented Mar 15, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 17, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 19, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 19, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 19, 2026

Uh oh!

Kha commented Mar 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

leanprover-radar commented Mar 12, 2026 •

edited

Loading

leanprover-bot commented Mar 12, 2026 •

edited

Loading

mathlib-lean-pr-testing bot commented Mar 12, 2026 •

edited

Loading

leanprover-radar commented Mar 12, 2026 •

edited

Loading