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

feat: replay constants into an Environment #2617

Merged
merged 2 commits into from
Oct 11, 2023
Merged

feat: replay constants into an Environment #2617

merged 2 commits into from
Oct 11, 2023

Conversation

kim-em
Copy link
Collaborator

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

This is the core functionality of lean4checker.

It is separately useful for users who need to copy constants from one Environment to another safely, without using Environment.add, which we will like to make private as in #2604.

@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 3, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 3, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2617
77d11ad
@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 3, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

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

@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Oct 4, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 4, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2617
076b20e
@kim-em kim-em mentioned this pull request Oct 4, 2023
Merged
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 4, 2023
@kim-em
Trigger CI for leanprover/lean4#2617
b8b13ee
kim-em added a commit to kim-em/aesop that referenced this pull request Oct 9, 2023
@kim-em
fix: use replay from leanprover/lean4#2617
5c8d78e
@kim-em kim-em mentioned this pull request Oct 9, 2023
Closed
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 9, 2023
@kim-em
use aesop#71 to test leanprover/lean4#2617
2800375
@kim-em kim-em mentioned this pull request Oct 9, 2023
Merged
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 9, 2023
@kim-em
trigger CI for leanprover/lean4#2617
146b626
@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 merged commit 076908d into leanprover:master Oct 11, 2023
@enricozb
Copy link
Contributor

enricozb commented Oct 13, 2023 •
edited
Loading

Does this not conflict with the NameSet.append in mathlib4?

https://github.com/leanprover-community/mathlib4/blob/c98e6b7f0f028f7958b90fe156a7756f9b7a1939/Mathlib/Lean/Expr/Basic.lean#L118-L127

Having some issues trying to write a nix derivation for the current mathlib.

@kim-em
Copy link
Collaborator Author

kim-em commented Oct 13, 2023

@enricozb, yes, it conflicts. The nightly-testing branch of Mathlib has already removed NameSet.append, and when Mathlib next moves to a new release candidate or stable release we will remove it from the master branch too.

@enricozb
Copy link
Contributor

Ah got it thanks for the info, didn't realize mathlib had a nightly branch. Thanks!

kim-em added a commit to leanprover-community/aesop that referenced this pull request Oct 16, 2023
@kim-em
chore: bump to v4.2.0-rc2 (#72)
0bd8465 
* fix: use replay from leanprover/lean4#2617

* chore: adapt to leanprover/lean4#2621

* bump to v4.2.0-rc2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@david-christiansen david-christiansen david-christiansen left review comments

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 @enricozb @david-christiansen