Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jun 11, 2025

Thanks to mmap, startup time is not necessarily related to this figure, but it can be used as a rough measure for that and how much data the module depends on, i.e. the rebuild chance.

Also adds new cumulative benchmarks for this metric as well as the number of imported constants and env ext entries.

@Kha
Copy link
Member Author

Kha commented Jun 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit b67e2f7.
There were significant changes against commit 0002ea8:

  Benchmark                            Metric       Change
  =================================================================
- Std.Data.Internal.List.Associative   task-clock     4.6% (35.5 σ)
- Std.Data.Internal.List.Associative   wall-clock     4.8% (25.6 σ)
- bv_decide_mod                        task-clock     2.7% (25.9 σ)
- bv_decide_mod                        wall-clock     2.8% (32.6 σ)
- parser                               task-clock     6.4% (27.6 σ)
- parser                               wall-clock     6.4% (27.5 σ)

@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 11, 2025
@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 0002ea8a3702a0c2191b03e1274aefc05b53ca8c --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 16:43:11)

@Kha Kha force-pushed the push-ltuxppuwwuok branch from b67e2f7 to 0e09804 Compare June 11, 2025 16:44
@Kha
Copy link
Member Author

Kha commented Jun 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 0e09804.
There were significant changes against commit 0002ea8:

  Benchmark                         Metric                  Change
  ==========================================================================
- Init.Data.BitVec.Lemmas re-elab   branch-misses             1.2%  (31.5 σ)
- rbmap_library                     task-clock                6.8%  (26.9 σ)
- rbmap_library                     wall-clock                6.7%  (24.1 σ)
- stdlib                            blocked (unaccounted)     1.3% (132.7 σ)

@Kha Kha added this pull request to the merge queue Jun 12, 2025
@Kha Kha removed this pull request from the merge queue due to a manual request Jun 12, 2025
@Kha Kha enabled auto-merge June 12, 2025 08:09
@Kha Kha added this pull request to the merge queue Jun 12, 2025
Merged via the queue into leanprover:master with commit f0347ee Jun 12, 2025
15 checks passed
@Kha Kha deleted the push-ltuxppuwwuok branch June 12, 2025 16:13
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
Thanks to `mmap`, startup time is not necessarily related to this
figure, but it can be used as a rough measure for that and how much data
the module depends on, i.e. the rebuild chance.

Also adds new cumulative benchmarks for this metric as well as the
number of imported constants and env ext entries.
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
Thanks to `mmap`, startup time is not necessarily related to this
figure, but it can be used as a rough measure for that and how much data
the module depends on, i.e. the rebuild chance.

Also adds new cumulative benchmarks for this metric as well as the
number of imported constants and env ext entries.
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