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

chore: speedcenter: count max symbols in shared libraries #3418

Merged
merged 2 commits into from
Feb 20, 2024
Merged

chore: speedcenter: count max symbols in shared libraries #3418

merged 2 commits into from
Feb 20, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Feb 20, 2024

No description provided.

@Kha
Copy link
Member Author

Kha commented Feb 20, 2024

!bench

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 20, 2024 11:48 Inactive
@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 20, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Feb 20, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-02-20 11:58:36)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 15cbcae7b280569924be7b4eb8361c6c77eaa5d7 --onto 8b8e001794e6a8b481d37f24fa77bb07797682a1. (2024-02-20 19:30:07)

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 97bfb72.
There were no significant changes against commit 15cbcae.

@Kha Kha added this pull request to the merge queue Feb 20, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 20, 2024
@Kha Kha enabled auto-merge February 20, 2024 19:11
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 20, 2024 19:18 Inactive
@Kha Kha added this pull request to the merge queue Feb 20, 2024
Merged via the queue into master with commit c9aea32 Feb 20, 2024
10 checks passed
@Kha Kha deleted the max-dynamic-symbols branch February 20, 2024 20:04
@Kha Kha mentioned this pull request Feb 21, 2024
Closed
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
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Kha @leanprover-community-mathlib4-bot @leanprover-bot