8000 feat: elaborate theorem bodies in parallel by Kha · Pull Request #7084 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: elaborate theorem bodies in parallel #7084

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
merged 9 commits into from
Mar 14, 2025
Merged

feat: elaborate theorem bodies in parallel #7084

merged 9 commits into from
Mar 14, 2025

Conversation

Kha
Copy link
Member
@Kha Kha commented Feb 14, 2025 •
edited
Loading

This PR enables the elaboration of theorem bodies, i.e. proofs, to happen in parallel to each other as well as to other elaboration tasks.

Specifically, to be eligible for parallel proof elaboration,

  • the theorem must not be in a mutual block
  • deprecated.oldSectionVars must not be set
  • Elab.async must be set (currently defaults to true in the language server, false on the cmdline)

To be activated for downstream projects (i.e. in stage 1) pending further Mathlib validation.

@Kha Kha force-pushed the push-xkzsuvwvlstz branch 3 times, most recently from ba5db15 to 8000 fbfc185 Compare February 14, 2025 18:07
@Kha Kha force-pushed the push-xkzsuvwvlstz branch 12 times, most recently from 22593b0 to 0386264 Compare March 8, 2025 10:58
@Kha Kha force-pushed the push-xkzsuvwvlstz branch 10 times, most recently from 51b51bb to c3f52a0 Compare March 12, 2025 14:33
@Kha
Copy link
Member Author
Kha commented Mar 12, 2025

!bench

@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 12, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Mar 12, 2025 •
edited
Loading

Mathlib CI status (docs):
Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-03-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-03-12 14:59:12)

  • 💥 Mathlib branch lean-pr-testing-7084 build failed against this PR. (2025-03-12 15:04:46) View Log
    Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-03-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2025-03-12 16:13:04)
  • 💥 Mathlib branch lean-pr-testing-7084 build failed against this PR. (2025-03-12 16:18:30) View Log
  • 💥 Mathlib branch lean-pr-testing-7084 build failed against this PR. (2025-03-12 21:02:42) View Log
  • ❌ Mathlib branch lean-pr-testing-7084 built against this PR, but testing failed. (2025-03-13 13:13:56) View Log
  • ✅ Mathlib branch lean-pr-testing-7084 has successfully built against this PR. (2025-03-13 13:37:57) View Log
  • ✅ Mathlib branch lean-pr-testing-7084 has successfully built against this PR. (2025-03-13 16:19:16) View Log
    Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase af82d75e86d42ef6e358af7e171c1ad30af6c02c --onto c1d145e9d70569274ac868805b4a8591d09718af. (2025-03-13 19:23:20)
  • 💥 Mathlib branch lean-pr-testing-7084 build failed against this PR. (2025-03-13 19:25:49) View Log
    Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 07ee2eea21545fb055f1a8bdb848e2a419502c97 --onto c1d145e9d70569274ac868805b4a8591d09718af. (2025-03-13 20:49:44)
  • 💥 Mathlib branch lean-pr-testing-7084 build failed against this PR. (2025-03-13 20:52:26) View Log
8000

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 12, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7084
76a271b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 13, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7084
3515004
@Kha Kha force-pushed the push-xkzsuvwvlstz branch 3 times, most recently from bc95397 to f8772bf Compare March 13, 2025 18:57
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 13, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7084
c6bd8f8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 13, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7084
49b7d8f
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Mar 13, 2025
@Kha Kha force-pushed the push-xkzsuvwvlstz branch from f8772bf to ab0ceb6 Compare March 13, 2025 20:25
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Mar 13, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7084
f931699
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 13, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7084
38fdb32
@Kha Kha marked this pull request as ready for review March 14, 2025 07:49
@Kha Kha requested review from mhuisi and kim-em as code owners March 14, 2025 07:49
@Kha Kha enabled auto-merge March 14, 2025 07:49
@Kha Kha added the changelog-language Language features, tactics, and metaprograms label Mar 14, 2025
@Kha Kha added this pull request to the merge queue Mar 14, 2025
Merged via the queue into leanprover:master with commit e1d1594 Mar 14, 2025
21 of 22 checks passed
@Kha Kha deleted the push-xkzsuvwvlstz branch March 14, 2025 08:24
@Kha Kha mentioned this pull request Apr 14, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms force-mathlib-ci 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-bot @leanprover-bot
0