Skip to content

Conversation

@hargoniX
Copy link
Contributor

This PR inlines several Decidable instances for performance reasons.

Unlike the previous #10934 it does not attempt to also simplify the Decidable instance system as
that has proven to have non trivial performance impact.

@hargoniX hargoniX force-pushed the hbv/inline_instances_tame branch from bdd7406 to 1952da6 Compare October 29, 2025 08:19
@hargoniX hargoniX added the changelog-library Library label Oct 29, 2025
@Rob23oba
Copy link
Contributor

I don't really think this is performance difference but rather a bug in the instance size calculation (see #11009)

@hargoniX
Copy link
Contributor Author

That's good to know, I would just like to avoid people hitting this bug so we'll do the revert and tamer change first and if the instance size is eventually fixed we can go back again.

@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 Oct 29, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-10-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-29 09:12:00)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-28 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. (2025-10-29 09:12:01)

@hargoniX
Copy link
Contributor Author

Works with mathlib: leanprover-community/mathlib4-nightly-testing#101

@hargoniX hargoniX force-pushed the hbv/inline_instances_tame branch from 1952da6 to b33f428 Compare October 29, 2025 10:48
@hargoniX hargoniX enabled auto-merge October 29, 2025 10:48
@hargoniX hargoniX added this pull request to the merge queue Oct 29, 2025
Merged via the queue into master with commit a51822e Oct 29, 2025
14 checks passed
@hargoniX hargoniX deleted the hbv/inline_instances_tame branch October 29, 2025 12:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants