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.

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

refactor: move IO.Channel and IO.Mutex to Std.Sync #6282

Merged
merged 1 commit into from
Dec 3, 2024
Merged

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Dec 2, 2024

This PR moves IO.Channel and IO.Mutex from Init to Std.Sync and renames them to Std.Channel and Std.Mutex.

Note that the original files are retained and the deprecation is written manually as we cannot import Std from Init so this is the only way to deprecate without a hard breaking change. In particular we do not yet move Std.Queue from Init to Std both because it needs to be retained for this deprecation to work but also because it is already within the Std namespace and as such we cannot maintain two copies of the file at once. After the deprecation period is finished Std.Queue will find a new home in Std.Data.Queue.

@hargoniX hargoniX added the changelog-library Library label Dec 2, 2024
@hargoniX hargoniX added the awaiting-review Waiting for someone to review the PR label Dec 2, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc December 2, 2024 10:38 Inactive
@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 Dec 2, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 2, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 2, 2024
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 2, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@hargoniX hargoniX added this pull request to the merge queue Dec 3, 2024
Merged via the queue into master with commit 24b412e Dec 3, 2024
27 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants