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

refactor: lake: use Job for all builtin facets #6418

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Dec 19, 2024

This PR alters all builtin Lake facets to produce Job objects.

@tydeu tydeu added the changelog-lake Lake label Dec 19, 2024
@tydeu tydeu force-pushed the import-jobs branch 3 times, most recently from adbbff2 to 7e9ade6 Compare December 20, 2024 04:50
@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 Dec 20, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1214e6463f4196f4e0e70cd3a282172b56164d87 --onto a8a160b09147c3225150703ac727eea6ee9a3b0e. (2024-12-20 05:08:08)

@tydeu
Copy link
Member Author

tydeu commented Dec 21, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 6b16b06.
There were significant changes against commit 1214e64:

  Benchmark         Metric       Change
  ==============================================
- ilean roundtrip   parse          3.5% (24.5 σ)
- parser            task-clock     3.5% (23.7 σ)
- parser            wall-clock     3.5% (23.3 σ)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-lake Lake 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