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

Merged
merged 9 commits into from
Jan 10, 2025
Merged

feat: asynchronous timer API #6306

merged 9 commits into from
Jan 10, 2025

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.

@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
  • 🟡 Mathlib branch lean-pr-testing-6306 build against this PR was cancelled. (2025-01-05 18:45:37) View Log
  • ✅ Mathlib branch lean-pr-testing-6306 has successfully built against this PR. (2025-01-05 19:25:58) View Log
  • ✅ Mathlib branch lean-pr-testing-6306 has successfully built against this PR. (2025-01-05 23:50:03) View Log
  • ✅ Mathlib branch lean-pr-testing-6306 has successfully built against this PR. (2025-01-07 10:18:32) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0b5d97725cef10e064acb792faafc4b5cdd35b39 --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-10 16:23:56)

@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 3 times, most recently from d34ae04 to d3ab1c3 Compare January 3, 2025 09:06
@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
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 5, 2025 18:21 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 5, 2025 18:32 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 5, 2025 22:55 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 5, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 7, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 7, 2025
@hargoniX hargoniX marked this pull request as ready for review January 10, 2025 16:01
@hargoniX hargoniX requested a review from TwoFX as a code owner January 10, 2025 16:01
@hargoniX hargoniX removed the request for review from TwoFX January 10, 2025 16:01
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 10, 2025 16:15 Inactive
@hargoniX hargoniX merged commit f1e506a into ft-async Jan 10, 2025
15 checks passed
hargoniX added a commit that referenced this pull request Jan 13, 2025
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.
hargoniX added a commit that referenced this pull request Jan 13, 2025
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.
hargoniX added a commit that referenced this pull request Jan 13, 2025
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.
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.

2 participants