Skip to content

feat: @[instance_reducible] part 2#12263

Merged
kim-em merged 20 commits intomasterfrom
instance_reducible_2
Feb 3, 2026
Merged

feat: @[instance_reducible] part 2#12263
kim-em merged 20 commits intomasterfrom
instance_reducible_2

Conversation

@leodemoura
Copy link
Copy Markdown
Member

@leodemoura leodemoura commented Feb 1, 2026 •
edited
Loading

This PR implements the second part of #12247.

@leodemoura leodemoura requested a review from kim-em as a code owner February 1, 2026 05:46
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 1, 2026
@ghost
Copy link
Copy Markdown

ghost commented Feb 1, 2026 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ec60620534cc25d1e16612468a7d3ba80cf91938 --onto d1514f3cecc4139039962137fcf3a84c9459194a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-01 06:37:45)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7a9a4e18c2c1defa4261b852f38f6d67f18eb1c --onto d1514f3cecc4139039962137fcf3a84c9459194a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-01 17:59:52)
  • 💥 Mathlib branch lean-pr-testing-12263 build failed against this PR. (2026-02-02 00:03:54) View Log
  • 💥 Mathlib branch lean-pr-testing-12263 build failed against this PR. (2026-02-02 00:49:54) View Log
  • 💥 Mathlib branch lean-pr-testing-12263 build failed against this PR. (2026-02-02 01:05:03) View Log
  • 💥 Mathlib branch lean-pr-testing-12263 build failed against this PR. (2026-02-02 01:25:24) View Log
  • 💥 Mathlib branch lean-pr-testing-12263 build failed against this PR. (2026-02-02 12:20:49) View Log
  • 💥 Mathlib branch lean-pr-testing-12263 build failed against this PR. (2026-02-02 19:15:47) View Log
  • 🟡 Mathlib branch lean-pr-testing-12263 build this PR didn't complete normally. (2026-02-02 22:03:34) View Log
  • ❌ Mathlib branch lean-pr-testing-12263 built against this PR, but linting failed. (2026-02-02 22:59:13) View Log
  • ❌ Mathlib branch lean-pr-testing-12263 built against this PR, but linting failed. (2026-02-03 04:00:30) View Log

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Feb 1, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ec60620534cc25d1e16612468a7d3ba80cf91938 --onto 42a0e9245300da6b3d971fa0033d726bb8e11cc3. You can force reference manual CI using the force-manual-ci label. (2026-02-01 06:37:47)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c7a9a4e18c2c1defa4261b852f38f6d67f18eb1c --onto 42a0e9245300da6b3d971fa0033d726bb8e11cc3. You can force reference manual CI using the force-manual-ci label. (2026-02-01 17:59:53)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-01 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-02-01 23:59:25)

@leodemoura leodemoura force-pushed the instance_reducible_2 branch from 8276a52 to 7a33829 Compare February 1, 2026 19:00
@leodemoura leodemoura added the changelog-language Language features and metaprograms label Feb 1, 2026
@kim-em kim-em force-pushed the instance_reducible_2 branch 2 times, most recently from e3cfdf9 to a249288 Compare February 1, 2026 23:10
@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 1, 2026
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2026
Update lean-toolchain for testing leanprover/lean4#12263
803b680
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 2, 2026
Update lean-toolchain for testing leanprover/lean4#12263
4c4d894
@github-actions 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 Feb 2, 2026
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Feb 2, 2026
kim-em added a commit to leanprover-community/batteries that referenced this pull request Feb 2, 2026
@kim-em
adaptations for leanprover/lean4#12263
9ee5c9d
kim-em added a commit to leanprover-community/plausible that referenced this pull request Feb 2, 2026
@kim-em
adaptations for leanprover/lean4#12263
297eedb
kim-em added a commit to leanprover-community/batteries that referenced this pull request Feb 3, 2026
@kim-em @claude
fix: use isInstance instead of isInstanceReducible in docBlame linter
ef2da8a 
leanprover/lean4#12263 removed isGlobalInstance. The previous adaptation
used isInstanceReducible, but this doesn't cover all cases - structure
field projections that are instances (like AlgCat.isRing) have
isInstance=true but isInstanceReducible=false.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
@kim-em kim-em force-pushed the instance_reducible_2 branch from a249288 to 6fd6f65 Compare February 3, 2026 03:48
@kim-em kim-em removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 3, 2026
@kim-em kim-em enabled auto-merge February 3, 2026 03:48
@kim-em kim-em added this pull request to the merge queue Feb 3, 2026
Merged via the queue into master with commit e02a140 Feb 3, 2026
19 checks passed
@Rob23oba Rob23oba mentioned this pull request Feb 5, 2026
Closed
This was referenced Feb 17, 2026
Merged
Closed
kim-em added a commit to leanprover-community/plausible that referenced this pull request Feb 17, 2026
@kim-em
chore: bump toolchain to v4.29.0-rc1 (#65)
a8191ec 
* patches for nightly-2025-01-04, and drop Batteries dependency

* fix adaptation note

* merge main

* fixes for leanprover/lean4#7516

* merge lean-pr-testing-7516

* deprecations

* toolchain

* list deprecations

* bump toolchain

* adaptations for leanprover/lean4#12263

* merge lean-pr-testing-12263

* chore: bump toolchain to v4.29.0-rc1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@datokrat datokrat Awaiting requested review from datokrat datokrat is a code owner

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features and metaprograms force-mathlib-ci mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@leodemoura @leanprover-bot @kim-em @Kha