Skip to content

Conversation

@algebraic-dev
Copy link
Member

@algebraic-dev algebraic-dev commented Oct 3, 2025

This PR adds more selectors for TCP and Signals.

It also fixes a problem with Selectors that they cannot be closures over a promise, otherwise it causes the waiter promise to never be dropped.

@algebraic-dev algebraic-dev self-assigned this Oct 3, 2025
@algebraic-dev algebraic-dev requested a review from TwoFX as a code owner October 3, 2025 21:12
@algebraic-dev algebraic-dev changed the title feat: adds acceptSelector and modified the signal selector to be used more than one. feat: adds acceptSelector and modified the signal selector to be used more than one Oct 4, 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 Oct 4, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 4, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5ef7b45afaedd794fb39b0fbd70924b573694a00 --onto 0b2193c7715a55246d0596a4db548c1b5b81562a. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-04 01:13:22)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase aa86d95c0897a5aca9535dad6ffb1fd0f20cd5f1 --onto c32a57e5806476ed6bac4c9cf1bb11cea2b02ea2. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-09 13:51:00)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase aa86d95c0897a5aca9535dad6ffb1fd0f20cd5f1 --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-17 00:18:33)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase aa86d95c0897a5aca9535dad6ffb1fd0f20cd5f1 --onto 4ce7ad19cea348506876685a19a7e0cca442c6d0. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-17 14:50:40)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 4, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5ef7b45afaedd794fb39b0fbd70924b573694a00 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-04 01:13:23)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase aa86d95c0897a5aca9535dad6ffb1fd0f20cd5f1 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-09 13:51:04)

@algebraic-dev algebraic-dev changed the title feat: adds acceptSelector and modified the signal selector to be used more than one feat: adds acceptSelector and modified selectors. Oct 9, 2025
@algebraic-dev algebraic-dev changed the title feat: adds acceptSelector and modified selectors. feat: adds acceptSelector and modified selectors Oct 9, 2025
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be great to have some theses for these changes.

@algebraic-dev algebraic-dev requested a review from TwoFX October 16, 2025 23:05
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good after addressing the last comment.

@algebraic-dev algebraic-dev added this pull request to the merge queue Oct 17, 2025
Merged via the queue into leanprover:master with commit f9adafe Oct 17, 2025
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

4 participants