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

feat: asynchronous timer API #6306

Draft
wants to merge 54 commits into
base: ft-async
Choose a base branch
from
Draft

feat: asynchronous timer API #6306

wants to merge 54 commits into from

Conversation

hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Dec 4, 2024

This PR implements a basic asynchronous timer API on top of the libuv work.

It purposely puts this into Std.Internal as we might still have to change the API as we continue develop of the async library across releases so I would only like to stabilize it once we are certain this is a fine API.

A few additional notes:

  • we currently do not implement a bind operator on AsyncTask on purpose as Task.bind on Task.pure is a non trivial operation and users should be aware of it. Furthermore there is the consideration that as they will have to bind on both IO and AsyncTask we might want to make potential task points explicit in the syntax (did somebody say await?).
  • the API generally takes inspiration from https://docs.rs/tokio/latest/tokio/time/index.html, though it has to adapt as Rust's and Lean's asynchronity concepts are sufficiently different.

Stacked on top of #6219.

algebraic-dev and others added 26 commits December 3, 2024 10:42
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
@hargoniX hargoniX added the changelog-no Do not include this PR in the release changelog label Dec 4, 2024
@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 4, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 4, 2024

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00718c3959d93972b43ee30ac008e9d655d9f151 --onto cb600ed9b436e4290b819b0529f8454490bffeb6. (2024-12-04 14:08:17)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00718c3959d93972b43ee30ac008e9d655d9f151 --onto 019f8e175f9650b829aca8ee501f41c0a5d9076d. (2024-12-05 17:09:27)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00718c3959d93972b43ee30ac008e9d655d9f151 --onto 6e60d130845855a9c3263c235bcbcc543b9b5c32. (2024-12-06 16:42:58)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-01-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2025-01-02 13:44:03)
  • 🟡 Mathlib branch lean-pr-testing-6306 build against this PR was cancelled. (2025-01-03 09:46:57) View Log
  • ✅ Mathlib branch lean-pr-testing-6306 has successfully built against this PR. (2025-01-03 10:29:39) View Log

@hargoniX hargoniX changed the base branch from master to ft-async January 2, 2025 09:36
@hargoniX hargoniX force-pushed the hbv/async-sleep branch 2 times, most recently from 4199e25 to d34ae04 Compare January 2, 2025 13:21
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 3, 2025 09:20 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 3, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 3, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 3, 2025 09:33 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 3, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 3, 2025
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jan 3, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog 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