Skip to content

test: add language server startup benchmark#3558

Merged
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:mhuisi/server-startup-bench
Mar 4, 2024
Merged

test: add language server startup benchmark#3558
mhuisi merged 1 commit intoleanprover:masterfrom
mhuisi:mhuisi/server-startup-bench

Conversation

@mhuisi
Copy link
Copy Markdown
Contributor

@mhuisi mhuisi commented Mar 1, 2024

Benchmark to catch future regressions as the one fixed in #3552.

@mhuisi mhuisi requested a review from Kha March 1, 2024 16:56
@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 Mar 1, 2024
@ghost
Copy link
Copy Markdown

ghost commented Mar 1, 2024

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7e944c1a309728581257cb6351c9bc0b9c741b7e --onto 43d6eb144e7a84af7c6eb40e60c9d2538367d6eb. (2024-03-01 17:12:37)

@Kha
Copy link
Copy Markdown
Member

Kha commented Mar 4, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 4, 2024

Here are the benchmark results for commit 3cfe06b.
There were no significant changes against commit 7e944c1.

@mhuisi mhuisi added this pull request to the merge queue Mar 4, 2024
Merged via the queue into leanprover:master with commit 093e1cf Mar 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Kha approved these changes

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

@mhuisi @Kha @leanprover-bot