8000 feat: elaborate theorem bodies in parallel by Kha · Pull Request #5864 · 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 #5864

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
Closed
wants to merge 218 commits into from
Closed

feat: elaborate theorem bodies in parallel #5864

wants to merge 218 commits into from

Conversation

Kha
Copy link
Member
@Kha Kha commented Oct 28, 2024

Draft in need of cleanups, smaller fixes, and incremental upstreaming, opened for benchmarking

Kha added 30 commits July 5, 2024 10:36
@Kha
feat: parallel linting
35bbf70
@Kha
fix
2873696
@Kha
hacky async kernel
61f44b8
@Kha
feat: disable old cmdline driver
a485c34
@Kha
opt
184569e
@Kha
linearize
a1e6ff4
@Kha
single promise
7e28a50
@Kha
porgess
8097c73
@Kha
add back
379b94e
@Kha
restore server code
edd8a81
10000
@Kha
more
686f407
@Kha
final
c874da0
@Kha
more
03a88ec
@Kha
fix tests
cfa4752
@Kha
Merge branch 'het-snaps-cmdline' into async-kernel
2e32033
@Kha
minimalSnapshots for async linting
aea190b
@Kha
minimalSnapshots for async TC
f820121
@Kha
Merge branch 'master' of https://github.com/leanprover/lean4 into asy…
2b7e048 
…nc-kernel
@Kha
fix
3bd32d7
@Kha
go back to theorems only for now
17452b6
@Kha
chore: update stage0
cc66581
@Kha
oops
3f3a03e
@Kha
disable async linting again
23f61d1
@Kha
Revert "chore: update stage0"
64673a1 
This reverts commit cc66581.
@Kha
cleanup
d3079a6
@Kha
Merge branch 'master' of https://github.com/leanprover/lean4 into asy…
bd3003d 
…nc-kernel
@Kha
Merge branch 'master' of https://github.com/leanprover/lean4 into asy…
0f5390d 
…nc-kernel
@Kha
fix trace.Elab.snapshotTree
5a20929
@Kha
Merge branch 'master' of https://github.com/leanprover/lean4 into asy…
41a2b52 
…nc-kernel
@Kha
fix
763cd89
@Kha Kha force-pushed the async-proofs branch 4 times, most recently from 9c58b37 to 017c334 Compare January 13, 2025 09:49
@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 Jan 13, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Jan 13, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7939cfb03c78820b069ba9c931900d44b11f58e --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-13 10:10:28)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7939cfb03c78820b069ba9c931900d44b11f58e --onto a955708b6c5f25e7f9c9ae7b951f8f3d5aefe377. (2025-01-15 15:38:57)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7fd8733334bb0053e4e7ce39b4d241abe08f456 --onto a955708b6c5f25e7f9c9ae7b951f8f3d5aefe377. (2025-01-16 15:28:51)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5fb2e892c8bea5d359c0cd9ee59b271155db5538 --onto d4070d4bfbeb821b1614455e74198f5a11f557d5. (2025-01-18 23:04:51)

@Kha Kha force-pushed the async-proofs branch 10 times, most recently from 425e014 to 3afc828 Compare January 22, 2025 14:41
@Kha Kha changed the base branch from async-proofs-base to master February 5, 2025 10:32
@Kha Kha mentioned this pull request Feb 14, 2025
Merged
@Kha
Copy link
Member Author
Kha commented Apr 14, 2025

Obsoleted by #7084

@Kha Kha closed this Apr 14, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 Awaiting requested review from digama0 digama0 will be requested when the pull request is marked ready for review digama0 is a code owner

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi will be requested when the pull request is marked ready for review mhuisi is a code owner

@kmill kmill Awaiting requested review from kmill kmill will be requested when the pull request is marked ready for review kmill is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

@zwarich zwarich Awaiting requested review from zwarich zwarich will be requested when the pull request is marked ready for review zwarich is a code owner

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-bot @leanprover-community-bot
0