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

refactor: lake: generalize targets #7185

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

refactor: lake: generalize targets #7185

wants to merge 6 commits into from
+439 −285

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Feb 22, 2025

This PR refactors Lake's internals to enable the introduction of targets and facets beyond packages, modules, and libraries.

(WIP)

@tydeu tydeu added the changelog-lake Lake label Feb 22, 2025
@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 22, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 22, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7185
ffe70da
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 22, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7185
f7e00c8
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Feb 22, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 22, 2025 •
edited
Loading

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
aaa0b2a
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
37ce52a
@tydeu tydeu force-pushed the lake/target-refactor branch from a78dca6 to f352f4a Compare February 26, 2025 20:15
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 26, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
580a68c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 26, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
cf705ee
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 27, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
e0b572f
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 27, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
ea2b78b
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 27, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
abb30d8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 27, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
7258c52
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Feb 28, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
5e7d6bf
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Feb 28, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#7185
605a31f
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
builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake 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.
2 participants
@tydeu @leanprover-community-bot