Skip to content

step 1#14074

Draft
hargoniX wants to merge 3 commits into
masterfrom
hbv/nametrie
Draft

step 1#14074
hargoniX wants to merge 3 commits into
masterfrom
hbv/nametrie

Conversation

@hargoniX

Copy link
Copy Markdown
Contributor

No description provided.

@hargoniX

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jun 16, 2026

Copy link
Copy Markdown

Benchmark results for b56c7d6 against 99683cc are in. There are significant results. @hargoniX

  • build//instructions: -16.0G (-0.14%)

Medium changes (3✅)

  • build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -4.2G (-1.83%)
  • build/module/Std.Data.DHashMap.RawLemmas//instructions: -1.1G (-0.80%)
  • misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -4.4G (-1.97%)

Small changes (44✅, 2🟥)

Too many entries to display here. View the full report on radar instead.

@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 Jun 16, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jun 16, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 99683cc4dbbf60324235b721c81e0bd8ca4c3b69 --onto 24c48fe0fdbf4bca5b6f907e638732c871dcd2db. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-16 10:44:14)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 99683cc4dbbf60324235b721c81e0bd8ca4c3b69 --onto 4792cd22887c8b529a351f6563b693426ff2a8f8. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-18 09:40:11)

@leanprover-bot

Copy link
Copy Markdown
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 99683cc4dbbf60324235b721c81e0bd8ca4c3b69 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-16 10:44:17)

@hargoniX

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jun 18, 2026

Copy link
Copy Markdown

Benchmark results for 091d3fc against 99683cc are in. There are significant results. @hargoniX

  • build//instructions: -19.3G (-0.17%)

Medium changes (3✅)

  • build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -4.4G (-1.88%)
  • build/module/Std.Data.DHashMap.RawLemmas//instructions: -1.1G (-0.85%)
  • misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -4.3G (-1.91%)

Small changes (60✅, 2🟥)

Too many entries to display here. View the full report on radar instead.

@hargoniX

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jun 18, 2026

Copy link
Copy Markdown

Benchmark results for e307570 against 99683cc are in. There are significant results. @hargoniX

  • build//instructions: -20.6G (-0.18%)

Medium changes (3✅)

  • build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -4.4G (-1.88%)
  • build/module/Std.Data.DHashMap.RawLemmas//instructions: -1.2G (-0.87%)
  • misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -4.3G (-1.92%)

Small changes (58✅, 2🟥)

Too many entries to display here. View the full report on radar instead.

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.

3 participants