Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: bench building with N cores #7031

Closed
wants to merge 4 commits into from

Conversation

Kha
Copy link
Member

@Kha Kha commented Feb 11, 2025

No description provided.

@Kha
Copy link
Member Author

Kha commented Feb 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 64e100a.
The entire run failed.
Found no significant differences.

@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 Feb 11, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 11, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase feb8cc2d4ad32a5df123222565317c2103814233 --onto d61f506da254b919f93e571a84247319de78f526. (2025-02-11 08:56:46)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase feb8cc2d4ad32a5df123222565317c2103814233 --onto befee896b38349a51dad1627360adbab317f3192. (2025-02-11 11:29:52)

@Kha
Copy link
Member Author

Kha commented Feb 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 64e100a.
The entire run failed.
Found no significant differences.

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 64e100a.
There were significant changes against commit feb8cc2:

  Benchmark                   Metric                    Change
  ======================================================================
+ bv_decide_inequality.lean   task-clock                 -5.4% (-17.5 σ)
+ bv_decide_inequality.lean   wall-clock                 -5.4% (-11.6 σ)
- stdlib                      attribute application      80.6%  (32.4 σ)
- stdlib                      dsimp                     157.5%  (67.4 σ)
- stdlib                      instantiate metavars       62.1% (272.3 σ)
- stdlib                      process pre-definitions   138.5%  (14.0 σ)
- stdlib                      tactic execution           89.7%  (23.0 σ)
+ stdlib                      task-clock                 -5.0% (-21.0 σ)
- stdlib                      type checking             110.6%  (36.7 σ)
- stdlib                      wall-clock                 66.1% (121.5 σ)

@Kha Kha force-pushed the push-uqknotylrnzs branch from 64e100a to f568974 Compare February 11, 2025 09:17
@Kha
Copy link
Member Author

Kha commented Feb 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit f568974.
There were significant changes against commit feb8cc2:

  Benchmark             Metric                    Change
  =================================================================
+ bv_decide_mod         task-clock                 -2.9%  (-58.9 σ)
+ bv_decide_mod         wall-clock                 -2.8% (-152.0 σ)
+ bv_decide_realworld   task-clock                 -4.6%  (-68.4 σ)
+ bv_decide_realworld   wall-clock                 -2.6%  (-45.2 σ)
- ilean roundtrip       parse                       4.7%   (16.2 σ)
+ import Lean           wall-clock                 -3.3%  (-10.2 σ)
+ parser                task-clock                 -8.9%  (-57.6 σ)
+ parser                wall-clock                 -8.9%  (-55.2 σ)
- qsort                 task-clock                  3.1%   (55.0 σ)
- qsort                 wall-clock                  3.1%   (65.3 σ)
+ rbmap                 task-clock                 -8.5%  (-14.4 σ)
+ rbmap                 wall-clock                 -8.5%  (-12.9 σ)
- stdlib                attribute application     110.2%   (89.6 σ)
- stdlib                dsimp                     257.8%   (14.4 σ)
- stdlib                fix level params          100.5% (1337.7 σ)
- stdlib                instantiate metavars      120.8%   (11.5 σ)
- stdlib                instructions                2.6%  (304.5 σ)
- stdlib                maxrss                     25.7%   (72.3 σ)
- stdlib                process pre-definitions   427.7%  (163.0 σ)
- stdlib                tactic execution          130.9%  (156.4 σ)
- stdlib                task-clock                  1.7%   (32.9 σ)
- stdlib                type checking             143.4%   (82.7 σ)
- stdlib                wall-clock                 72.0% (2024.7 σ)

@Kha
Copy link
Member Author

Kha commented Feb 11, 2025

!bench

@Kha Kha changed the title chore: bench building with 4 cores chore: bench building with N cores Feb 11, 2025
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 18ff4cf.
There were significant changes against commit feb8cc2:

  Benchmark           Metric                    Change
  ==============================================================
- big_do              task-clock                  7.9%  (13.1 σ)
- big_do              wall-clock                  7.9%  (13.1 σ)
- big_omega.lean      task-clock                  1.9%  (11.5 σ)
- big_omega.lean      wall-clock                  1.9%  (11.6 σ)
+ big_omega.lean MT   task-clock                 -3.8% (-24.1 σ)
+ big_omega.lean MT   wall-clock                 -3.8% (-23.7 σ)
+ import Lean         task-clock                 -4.2% (-11.4 σ)
+ import Lean         wall-clock                 -4.2% (-11.5 σ)
- stdlib              attribute application      12.0%  (35.3 σ)
- stdlib              dsimp                      48.5%  (76.8 σ)
- stdlib              fix level params           23.4%  (49.0 σ)
- stdlib              instantiate metavars       13.6%  (95.9 σ)
- stdlib              process pre-definitions    33.8%  (10.1 σ)
- stdlib              tactic execution           19.6%  (15.1 σ)
+ stdlib              task-clock                 -4.5% (-15.4 σ)
- stdlib              type checking              24.7% (542.3 σ)
- stdlib              wall-clock                 13.2%  (42.0 σ)
- workspaceSymbols    task-clock                  3.9%  (13.3 σ)
- workspaceSymbols    wall-clock                  3.9%  (13.3 σ)

@Kha
Copy link
Member Author

Kha commented Feb 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 74c44cd.
There were significant changes against commit feb8cc2:

  Benchmark          Metric                    Change
  =============================================================
+ lake config elab   task-clock                 -3.6% (-17.0 σ)
+ lake config elab   wall-clock                 -3.7% (-15.2 σ)
+ parser             task-clock                 -4.4% (-10.1 σ)
+ rbmap_fbip         task-clock                 -4.2% (-19.7 σ)
+ rbmap_fbip         wall-clock                 -4.2% (-19.9 σ)
+ simp_arith1        task-clock                 -4.6% (-22.6 σ)
+ simp_arith1        wall-clock                 -4.5% (-22.5 σ)
- stdlib             dsimp                     108.7%  (36.8 σ)
- stdlib             fix level params           22.1%  (12.4 σ)
- stdlib             instantiate metavars       36.9%  (13.2 σ)
- stdlib             instructions                2.5% (239.3 σ)
- stdlib             maxrss                     25.3%  (18.5 σ)
- stdlib             process pre-definitions   181.7%  (70.1 σ)
- stdlib             tactic execution           42.7%  (45.9 σ)
- stdlib             task-clock                  2.6%  (18.3 σ)
- stdlib             type checking              73.4%  (19.3 σ)
- stdlib             wall-clock                  9.7%  (48.7 σ)
+ unionfind          task-clock                 -7.2% (-67.4 σ)
+ unionfind          wall-clock                 -7.2% (-59.0 σ)

@Kha Kha closed this Feb 11, 2025
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