Skip to content

Conversation

@hargoniX
Copy link
Contributor

No description provided.

@hargoniX
Copy link
Contributor Author

!bench

@leanprover-radar
Copy link

leanprover-radar commented Jan 16, 2026

Benchmark results for 8cd3032 against 960c01f are in! @hargoniX

Large changes (2✅, 13🟥)
  • binarytrees.st//instructions: -81.8M (-0.1%)
  • 🟥 build/module/Lean.Elab.Deriving.BEq//bytes .olean: +19kiB (+64.4%)
  • 🟥 build/module/Lean.Elab.Deriving.DecEq//bytes .olean: +20kiB (+66.1%)
  • 🟥 build/module/Lean.Elab.Deriving.Ord//bytes .olean: +16kiB (+56.4%)
  • 🟥 build/module/Lean.Elab.Deriving.ToExpr//bytes .olean: +15kiB (+60.0%)
  • 🟥 build/module/Lean.Elab.Inductive//bytes .olean: +21kiB (+51.3%)
  • 🟥 build/module/Lean.Elab.InheritDoc//bytes .olean: +13kiB (+50.2%)
  • 🟥 build/module/Lean.Elab.PreDefinition.PartialFixpoint.Induction//bytes .olean: +19kiB (+59.4%)
  • 🟥 build/module/Lean.Elab.Tactic.Ext//bytes .olean: +26kiB (+59.7%)
  • 🟥 build/module/Lean.Server.Rpc.Deriving//bytes .olean: +16kiB (+57.3%)
  • 🟥 hashmap.lean//instructions: +86.1M (+2.2%)
  • nat_repr//instructions: -794.9M (-18.8%)
  • 🟥 size/all/.olean//bytes: +6MiB (+1.8%)
  • 🟥 treemap.lean//instructions: +187.8M (+0.8%)
  • 🟥 unionfind//instructions: +72.0M (+0.3%)
Medium changes (2✅, 81🟥)

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

Small changes (37✅, 156🟥)

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

@hargoniX hargoniX force-pushed the hbv/closed_term_ctor_tree branch from 8cd3032 to 0456eed Compare January 16, 2026 12:27
@hargoniX
Copy link
Contributor Author

!bench

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Jan 16, 2026
@leanprover-radar
Copy link

leanprover-radar commented Jan 16, 2026

Benchmark results for 0456eed against 12adfbf are in! @hargoniX

Large changes (2✅, 3🟥)
  • binarytrees.st//instructions: -82.7M (-0.1%)
  • 🟥 hashmap.lean//instructions: +85.8M (+2.2%)
  • tests/compiler//sum binary sizes: -11.4M (-0.9%)
  • 🟥 treemap.lean//instructions: +187.4M (+0.8%)
  • 🟥 unionfind//instructions: +71.3M (+0.3%)
Medium changes (2✅)
  • lake startup//instructions: -6.2M (-2.4%)
  • nat_repr//instructions: -518.6M (-13.1%)
Small changes (57✅, 9🟥)

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

@hargoniX
Copy link
Contributor Author

!bench

@leanprover-radar
Copy link

leanprover-radar commented Jan 16, 2026

Benchmark results for efee610 against 12adfbf are in! @hargoniX

Large changes (1✅, 4🟥)
  • 🟥 binarytrees.st//instructions: +52.8M (+0.1%)
  • 🟥 hashmap.lean//instructions: +86.3M (+2.3%)
  • tests/compiler//sum binary sizes: -40.5M (-3.3%)
  • 🟥 treemap.lean//instructions: +187.8M (+0.8%)
  • 🟥 unionfind//instructions: +70.5M (+0.3%)
Medium changes (3✅)
  • lake startup//instructions: -7.1M (-2.7%)
  • nat_repr//instructions: -576.9M (-14.6%)
  • size/install//bytes: -11MiB (-0.5%)
Small changes (102✅, 8🟥)

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

@hargoniX hargoniX force-pushed the hbv/closed_term_ctor_tree branch from efee610 to f7f467b Compare January 16, 2026 16:18
@hargoniX hargoniX force-pushed the hbv/closed_term_ctor_tree branch from f7f467b to d9f4556 Compare January 16, 2026 16:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants