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: move ext environment extension to Lean.Meta.Tactic #6681

Merged
merged 2 commits into from
Jan 17, 2025
Merged

refactor: move ext environment extension to Lean.Meta.Tactic #6681

merged 2 commits into from
Jan 17, 2025

Conversation

leodemoura
Copy link
Member

Motivation: we are going to use ext theorems in grind, and we don't want to depend on Elab.

@leodemoura leodemoura added the changelog-no Do not include this PR in the release changelog label Jan 17, 2025
@leodemoura leodemoura requested a review from digama0 as a code owner January 17, 2025 18:50
@leodemoura leodemoura enabled auto-merge January 17, 2025 18:51
@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 17, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 17, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6681
e19a4f1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 17, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6681
4d5d0d8
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 17, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@leodemoura
refactor: move ext environment extension to Lean.Meta.Tactic
7b96f67
@leodemoura
chore: update stage0
46e6474 
Manual update stage0 is required to get the test suite green.
@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Jan 17, 2025
@leodemoura leodemoura disabled auto-merge January 17, 2025 19:58
@leodemoura
Copy link
Member Author

Going to merge manually as soon as it is green and stage2 builds successfully.

@leodemoura
Copy link
Member Author

Stage2 is building correctly. Failure above was a RPC issue. Going to merge.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 17, 2025 20:17 Inactive
@leodemoura leodemoura enabled auto-merge January 17, 2025 20:30
@leodemoura leodemoura disabled auto-merge January 17, 2025 20:31
@leodemoura leodemoura merged commit 9b629cc into master Jan 17, 2025
12 of 14 checks passed
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 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-no Do not include this PR in the release changelog changes-stage0 Contains stage0 changes, merge manually using rebase 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
@leodemoura @leanprover-community-bot