Skip to content

Conversation

Kha
Copy link
Member

@Kha Kha commented Oct 2, 2025

Fixes #10613

@Kha Kha added the changelog-no Do not include this PR in the release changelog label Oct 2, 2025
@Kha
Copy link
Member Author

Kha commented Oct 2, 2025

!bench

@leanprover-radar
Copy link

Failed to find a commit to compare against.

@Kha
Copy link
Member Author

Kha commented Oct 2, 2025

!radar

@leanprover-radar
Copy link

Failed to find a commit to compare against.

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 767663f.
There were significant changes against commit 24c86fc:

  Benchmark                 Metric                     Change
  ====================================================================
- Init size                 bytes .olean                 4.3%
- Init.Data.BitVec.Lemmas   wall-clock                  35.4% (53.3 σ)
- big_deceq_rec             branch-misses                2.2% (23.0 σ)
- grind_ring_5.lean         branch-misses                3.4% (30.4 σ)
- mut_rec_wf                branch-misses                4.4% (29.2 σ)
- riscv-ast.lean            branch-misses                3.9% (22.9 σ)
- simp_bubblesort_256       branch-misses                6.1% (20.3 σ)
- stdlib                    congr simp thm              71.8% (40.7 σ)
- stdlib                    number of imported bytes     2.2%
- stdlib size               bytes .olean                 2.8%

@nomeata nomeata changed the title fix: make congr theorems private fix: make .congr_simp theorems private Oct 2, 2025
@Kha
Copy link
Member Author

Kha commented Oct 2, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Oct 2, 2025

Benchmark results for 767663f against 24c86fc are in! @Kha

@Kha
Copy link
Member Author

Kha commented Oct 3, 2025

Given the regressions, this will need some further adjustments to preserve sharing while avoiding the name clash issues.

@Kha Kha force-pushed the push-xtvyynrswuqx branch from 767663f to 124f573 Compare October 10, 2025 13:00
@Kha
Copy link
Member Author

Kha commented Oct 10, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Oct 10, 2025

Benchmark results for 124f573 against fbfb075 are in! @Kha

@Kha
Copy link
Member Author

Kha commented Oct 10, 2025

!bench

@leanprover-radar
Copy link

leanprover-radar commented Oct 10, 2025

Benchmark results for bb0b792 against fbfb075 are in! @Kha

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit bb0b792.
There were significant changes against commit fbfb075:

  Benchmark   Metric                  Change
  ====================================================
- Init size   bytes .olean              1.1%
- stdlib      blocked (unaccounted)     6.6%  (49.0 σ)
- stdlib      congr simp thm           41.0%  (27.8 σ)
+ stdlib      maxrss                   -1.6% (-26.3 σ)

@Kha Kha force-pushed the push-xtvyynrswuqx branch from bb0b792 to acc3d5b Compare October 12, 2025 11:42
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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Panic in Lean.MapDeclarationExtension.insert

3 participants