Skip to content

Conversation

@leodemoura
Copy link
Member

@leodemoura leodemoura commented May 25, 2025

This PR adds seal commands at grind_ite.lean to workaround expensive definitionally equality tests in the canonicalizer. The new module system will automatically hide definitions such as HashMap.insert and TreeMap.insert which are being unfolded by the canonicalizer in this test.
This PR also adds a profileItM for tracking the time spent in the grind canonicalizer.

@leodemoura leodemoura added the changelog-no Do not include this PR in the release changelog label May 25, 2025
@leodemoura leodemoura enabled auto-merge May 25, 2025 00:35
@leodemoura leodemoura added this pull request to the merge queue May 25, 2025
@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 May 25, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a54872f5f64c9e8e0b89276384a2793b008b0078 --onto d5060e9e66aee1eee60bbeeea8ae9b9c94e29a47. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-25 01:00:51)

Merged via the queue into master with commit 2a1354b May 25, 2025
20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog 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.

3 participants