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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: add comparative benchmarking script #756

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat: add comparative benchmarking script #756

wants to merge 1 commit into from

Conversation

semorrison
Copy link
Contributor

This script:

  1. does a complete build of mathlib (using downloaded oleans) and mathlib4 (slowly).
  2. rebuilds just the "theory" files in mathlib4
  3. rebuilds the corresponding files in mathlib3
  4. reports the time taken for steps 2. and 3.

I propose posting the output of this script regularly at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20benchmark

Please feel free to edit this PR to change formatting / make more robust / etc.

@semorrison semorrison added the awaiting-review The author would like community review of the PR label Nov 27, 2022
@urkud
Copy link
Member

urkud commented Nov 28, 2022

Do you have an example output?

@semorrison
Copy link
Contributor Author 

mathlib4 theory files:
    320.70 real 307.63 user 47.21 sys
corresponding files in mathlib3:
    348.44 real 500.98 user 8.54 sys

@fpvandoorn
Copy link
Member

LGTM

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Nov 30, 2022
bors bot pushed a commit that referenced this pull request Nov 30, 2022
@semorrison
feat: add comparative benchmarking script (#756)
7d27cfc 
This script:
1. does a complete build of mathlib (using downloaded oleans) and mathlib4 (slowly).
2. rebuilds just the "theory" files in mathlib4
3. rebuilds the corresponding files in mathlib3
4. reports the time taken for steps 2. and 3.

I propose posting the output of this script regularly at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20benchmark

Please feel free to edit this PR to change formatting / make more robust / etc.


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Nov 30, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: add comparative benchmarking script [Merged by Bors] - feat: add comparative benchmarking script Nov 30, 2022
@bors bors bot closed this Nov 30, 2022
@bors bors bot deleted the benchmark_script branch November 30, 2022 11:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@semorrison @urkud @fpvandoorn