Skip to content

Conversation

@hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Jan 6, 2026

No description provided.

@hargoniX hargoniX requested a review from mhuisi as a code owner January 6, 2026 22:45
@hargoniX
Copy link
Contributor Author

hargoniX commented Jan 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Jan 6, 2026

Benchmark results for bee153e against 11e4e44 are in! @hargoniX

Medium changes (1✅)
  • build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: -1.2G (-0.5%)
Small changes (14✅, 1🟥)
  • 🟥 build/module/Lean.Server.References//instructions: +46.3M (+0.4%)
  • build/module/Std.Data.DHashMap.Lemmas//instructions: -400.9M (-0.6%)
  • build/module/Std.Data.DHashMap.RawLemmas//instructions: -292.6M (-0.2%)
  • build/module/Std.Data.DTreeMap.Lemmas//instructions: -795.3M (-1.1%) (reduced significance based on absolute threshold)
  • build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -676.9M (-0.8%) (reduced significance based on absolute threshold)
  • build/module/Std.Data.ExtDHashMap.Lemmas//instructions: -208.6M (-0.3%)
  • build/module/Std.Data.ExtDTreeMap.Lemmas//instructions: -531.2M (-0.8%) (reduced significance based on absolute threshold)
  • build/module/Std.Data.ExtHashMap.Lemmas//instructions: -72.6M (-0.2%)
  • build/module/Std.Data.ExtTreeMap.Lemmas//instructions: -232.7M (-0.6%)
  • build/module/Std.Data.HashMap.Lemmas//instructions: -155.3M (-0.4%)
  • build/module/Std.Data.Internal.List.Associative//instructions: -314.7M (-0.3%)
  • build/module/Std.Data.TreeMap.Lemmas//instructions: -358.0M (-0.9%) (reduced significance based on absolute threshold)
  • build/module/Std.Data.TreeMap.Raw.Lemmas//instructions: -311.1M (-0.6%) (reduced significance based on absolute threshold)
  • build/module/Std.Data.TreeSet.Lemmas//instructions: -82.8M (-0.6%)
  • build/module/Std.Do.SPred.DerivedLaws//instructions: -69.0M (-0.7%) (reduced significance based on absolute threshold)

@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 Jan 6, 2026
@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 11e4e44be070ec99bc734e40f8431fd92725842d --onto 0f866236c7c2e77e8d12ff61d08ef48694a0cbfb. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-06 23:44:36)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 11e4e44be070ec99bc734e40f8431fd92725842d --onto 0f866236c7c2e77e8d12ff61d08ef48694a0cbfb. You can force reference manual CI using the force-manual-ci label. (2026-01-06 23:44:38)

@hargoniX hargoniX added this pull request to the merge queue Jan 14, 2026
Merged via the queue into master with commit 8435dea Jan 14, 2026
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

6 participants