Skip to content

hbv/johan test - #14353

Closed
hargoniX wants to merge 11 commits into
masterfrom
hbv/johan-test
Closed

hargoniX wants to merge 11 commits into
masterfrom
hbv/johan-test

Conversation

@hargoniX

Copy link
Copy Markdown
Member
  • Initial commit to fork; Added .DS_Store to gitignore
  • Copied over the new implementation and cleaned it up a bit
  • Migrated the new staged dnf Implemented ordOfLt Cleaned up and made naming more consistent Added a few explanatory comments
  • Corrected a spelling mistake
  • Fixed proofs keeping lean from compiling
  • Removed .DS_Store from .gitignore
  • perf: inline qsort wrappers
  • Added inline at ordOfLt and dnfstaged
  • Removed inlines on wrappers for testing

@hargoniX

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

Copy link
Copy Markdown

Benchmark results for f278a7c against f0ef737 are in. (These commits have already been benchmarked in a previous command.) There are significant results. @hargoniX

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

  • Bench repo commit hashes for run build differ between commits.
  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build//instructions: +41.7G (+0.37%)

Large changes (3🟥)

  • 🟥 compiled/io_compute//instructions: +4.4G (+38.78%)
  • 🟥 misc/leanchecker --fresh Init//instructions: +11.3G (+3.13%)
  • 🟥 size/Init/.olean.private//bytes: +5MiB (+2.02%)

Medium changes (2🟥)

  • 🟥 elab/big_omega//instructions: +215.3M (+1.01%)
  • 🟥 elab/big_omega_MT//instructions: +210.8M (+0.98%)

Small changes (70✅, 30🟥)

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

@hargoniX

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Jul 10, 2026

Copy link
Copy Markdown

Benchmark results for 915b89a against f0ef737 are in. There are significant results. @hargoniX

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

  • Bench repo commit hashes for run build differ between commits.
  • Bench repo commit hashes for run other differ between commits.
  • 🟥 build//instructions: +41.2G (+0.36%)

Large changes (3🟥)

  • 🟥 compiled/io_compute//instructions: +4.3G (+38.20%)
  • 🟥 misc/leanchecker --fresh Init//instructions: +11.2G (+3.11%)
  • 🟥 size/Init/.olean.private//bytes: +5MiB (+2.02%)

Medium changes (1✅, 2🟥)

  • 🟥 elab/big_omega//instructions: +202.3M (+0.95%)
  • 🟥 elab/big_omega_MT//instructions: +212.1M (+0.99%)
  • elab/bv_decide_large_aig//instructions: -1.2G (-2.92%)

Small changes (68✅, 21🟥)

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

@hargoniX hargoniX closed this Jul 10, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants