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

chore: make Environment.add private #2642

Merged
merged 4 commits into from
Oct 12, 2023
Merged

chore: make Environment.add private #2642

merged 4 commits into from
Oct 12, 2023

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Oct 9, 2023

This is currently stacked on top of #2617, because Aesop will need that to be merged first.

@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 Oct 9, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 9, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2642
7392141
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 9, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Oct 9, 2023 •
edited
Loading

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 9, 2023
@kim-em
trigger CI for leanprover/lean4#2642
3754b50
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 9, 2023
@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Oct 9, 2023
@kim-em kim-em marked this pull request as ready for review October 9, 2023 15:05
@lenianiva
Copy link
Contributor

What can we use in place of Environment.add?

@digama0
Copy link
Collaborator

digama0 commented Oct 9, 2023

You should be using addDecl in the first place, the use cases for bypassing the kernel using Environment.add are very limited. That said, you can call it using an extern, as demonstrated here for lake.

@kim-em kim-em merged commit 5d096c3 into leanprover:master Oct 12, 2023
18 checks passed
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
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR 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.
4 participants
@kim-em @leanprover-community-mathlib4-bot @lenianiva @digama0