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

Add coq-category-theory to bench #15543

Merged
merged 1 commit into from
Jan 26, 2022
Merged

Add coq-category-theory to bench #15543

merged 1 commit into from
Jan 26, 2022

Conversation

Janno
Copy link
Contributor

@Janno Janno commented Jan 25, 2022 •
edited
Loading

As discussed on Zulip (https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/performance.20of.20the.20category_theory.20dev), the category-theory development is unique in the stress it puts on conversion, specifically regarding universe polymorphic terms.

I am not sure if I did this correctly. I suspect somebody with permissions to do so will have to run the bench job to find out.

@Janno Janno requested a review from a team as a code owner January 25, 2022 10:47
SkySkimmer
SkySkimmer requested changes Jan 25, 2022
View reviewed changes
dev/bench/bench.sh Outdated Show resolved Hide resolved
@Janno Janno mentioned this pull request Jan 25, 2022
Merged
@Alizter
Copy link
Contributor

Alizter commented Jan 25, 2022

Now that coq/opam#2079 has been merged @Janno, can you update this PR?

@Alizter Alizter added kind: infrastructure CI, build tools, development tools. part: bench The benchmark for performance testing. labels Jan 25, 2022
@Janno Janno force-pushed the janno/bench-category_theory branch from 9d70efa to e7ed1d2 Compare January 26, 2022 09:09
@Janno
Copy link
Contributor Author

Janno commented Jan 26, 2022

@Alizter Done! I think just adding the package should suffice now that it's in the opam archive.

@Alizter Alizter self-assigned this Jan 26, 2022
@Alizter Alizter added this to the 8.16+rc1 milestone Jan 26, 2022
@Alizter
Copy link
Contributor

Alizter commented Jan 26, 2022

@SkySkimmer can you start a bench?

@SkySkimmer
Copy link
Contributor

bench https://gitlab.com/coq/coq/-/jobs/2017265718

@Janno
Copy link
Contributor Author

Janno commented Jan 26, 2022

The bench finished successfully.

┌─────────────────────┬─────────────────────────┬─────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                     │      user time [s]      │             CPU cycles              │           CPU instructions            │  max resident mem [KB]  │   mem faults    │
│                     │                         │                                     │                                       │                         │                 │
│        package_name │     NEW      OLD  PDIFF │           NEW            OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD  PDIFF │ NEW  OLD  PDIFF │
├─────────────────────┼─────────────────────────┼─────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-core │   96.30    96.79  -0.51 │  385748068638   387133577711  -0.36 │   433237288405    433335379814  -0.02 │  272872   273280  -0.15 │   0    0    nan │
│ coq-category-theory │ 1630.63  1626.82   0.23 │ 7454406958656  7437197487864   0.23 │ 15223837683981  15223420788018   0.00 │ 1318008  1318264  -0.02 │   0    0    nan │
│          coq-stdlib │  407.20   400.10   1.77 │ 1649582531769  1622141661361   1.69 │  1409146287401   1409129648763   0.00 │  595856   597848  -0.33 │   0    0    nan │
└─────────────────────┴─────────────────────────┴─────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

@Alizter
Copy link
Contributor

Alizter commented Jan 26, 2022

Excellent! Merging soon.

@Alizter
Copy link
Contributor

Alizter commented Jan 26, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 20b040d into coq:master Jan 26, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@Alizter Alizter

Labels
kind: infrastructure CI, build tools, development tools. part: bench The benchmark for performance testing.
Projects
None yet
Milestone
8.16+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@Janno @Alizter @SkySkimmer