feat: add async timer primitives based on libuv #6219

algebraic-dev · 2024-11-26T00:38:22Z

This PR adds support for Timer and a event loop thread that gets requests from another threads and executes it.

leanprover-community-bot · 2024-11-26T01:04:04Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0eca3bd55de7f29320e90b83ef2f43e9dff7546b --onto 20acc72a29a8bb4d55223651caa0553ffa82ac88. (2024-11-26 01:04:03)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0eca3bd55de7f29320e90b83ef2f43e9dff7546b --onto 6d495586a1836da3e12efb4fbf9946bd9088ac5f. (2024-11-29 23:10:28)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b2f70dad52dfd72975ab08c8b24d5d46f79e9d7b --onto 3c5e612dc54733cd707becb929457d2f9d8ca6fd. (2024-12-03 04:50:45)
❗ 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-03 17:50:20)
❗ 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 16:45:12)
✅ Mathlib branch lean-pr-testing-6219 has successfully built against this PR. (2025-01-02 18:10:02) View Log
✅ Mathlib branch lean-pr-testing-6219 has successfully built against this PR. (2025-01-02 20:17:03) View Log
✅ Mathlib branch lean-pr-testing-6219 has successfully built against this PR. (2025-01-03 11:13:15) View Log
✅ Mathlib branch lean-pr-testing-6219 has successfully built against this PR. (2025-01-03 23:05:15) View Log
✅ Mathlib branch lean-pr-testing-6219 has successfully built against this PR. (2025-01-04 21:13:18) View Log

src/Std/UV.lean

src/runtime/libuv.cpp

src/runtime/uv_scheduler.h

src/runtime/libuv.cpp

src/Std/Internal/UV.lean

src/runtime/event_loop.cpp

src/runtime/libuv.h

src/runtime/libuv.cpp

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

src/Std/Internal/UV.lean

hargoniX

(Just to remove my changes requested)

hargoniX · 2025-01-04T19:23:31Z

@algebraic-dev and I went over the code yesterday, adding some tracing into the allocator/deallocator and observing the behavior of programs allocating many timers in a loop, the memory management seems to work fine now. Unless someone speaks up I'll merge this into the ft-async branch on Monday evening European time.

This PR adds support for `Timer` and a event loop thread that gets requests from another threads and executes it. --------- Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Henrik Böving <hargonix@gmail.com>

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.

This PR adds support for `Timer` and a event loop thread that gets requests from another threads and executes it. --------- Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Henrik Böving <hargonix@gmail.com>

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.

This PR adds support for `Timer` and a event loop thread that gets requests from another threads and executes it. --------- Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Henrik Böving <hargonix@gmail.com>

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.

This PR adds support for `Timer` and a event loop thread that gets requests from another threads and executes it. --------- Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Henrik Böving <hargonix@gmail.com>

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 requested a review from TwoFX as a code owner November 26, 2024 00:38

algebraic-dev marked this pull request as draft November 26, 2024 00:39

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 26, 2024

hargoniX reviewed Nov 26, 2024

View reviewed changes

eric-wieser reviewed Nov 27, 2024

View reviewed changes

src/runtime/libuv.cpp Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 27, 2024

View reviewed changes

src/runtime/libuv.cpp Outdated Show resolved Hide resolved

hargoniX reviewed Dec 2, 2024

View reviewed changes

src/runtime/uv_scheduler.h Outdated Show resolved Hide resolved

src/runtime/uv_scheduler.h Outdated Show resolved Hide resolved

src/runtime/libuv.cpp Outdated Show resolved Hide resolved

hargoniX reviewed Dec 2, 2024

View reviewed changes

src/Std/Internal/UV.lean Outdated Show resolved Hide resolved

TwoFX added the release-ci Enable all CI checks for a PR, like is done for releases label Dec 3, 2024

TwoFX reviewed Dec 3, 2024

View reviewed changes

algebraic-dev force-pushed the libuv branch 2 times, most recently from add268b to f7c1771 Compare December 3, 2024 13:40

algebraic-dev added 10 commits December 3, 2024 10:42

feat: start of the libuv bindings

db87acf

fix: a bunch of stuff

8bc0253

feat: start of the libuv bindings

a084c1a

fix: a bunch of stuff

7b7c6f9

fix: memory leak

dbee15e

fix: problem with the mutex and fixed a bunch of stuff

e702976

feat: add assert

bed7c2f

feat: change some things to make the ownerhsip better

d073efc

fix: some simple fixes

096278c

chore: improve docs

7b60b9d

algebraic-dev force-pushed the libuv branch from f7c1771 to 7b60b9d Compare December 3, 2024 13:42

algebraic-dev and others added 6 commits December 3, 2024 10:45

chore: update src/runtime/libuv.cpp

ecd2314

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

chore: update src/runtime/libuv.cpp

59f2482

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

chore: code style

8037415

Merge branch 'libuv' of github.com:algebraic-dev/lean4 into libuv

cc977da

chore: change filename and copyright mark that was wrong

b04f77d

fix: finish timer impl

ccce6d0

feat: more informative error messages

1313a7d

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 2, 2025

Trigger CI for leanprover/lean4#6219

6aa030f

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 2, 2025

Trigger CI for leanprover/lean4#6219

5aff1fe

TwoFX reviewed Jan 3, 2025

View reviewed changes

src/Std/Internal/UV.lean Outdated Show resolved Hide resolved

src/Std/Internal/UV.lean Outdated Show resolved Hide resolved

doc: review comments

70f2a97

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 3, 2025

Trigger CI for leanprover/lean4#6219

18ce3d5

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 3, 2025

Trigger CI for leanprover/lean4#6219

2fc3287

hargoniX and others added 4 commits January 3, 2025 20:08

fix: free timer control resources

59a9490

fix: double free

84b09c6

fix: memory leak in the foreach function of the register_external_class

460f18e

chore: account for even more of this *** jitter

b9247cf

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 3, 2025

Trigger CI for leanprover/lean4#6219

d0b45c5

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 3, 2025

Trigger CI for leanprover/lean4#6219

796df65

chore: share duplicated code

c3dfabe

hargoniX marked this pull request as ready for review January 4, 2025 19:19

hargoniX added the changelog-no Do not include this PR in the release changelog label Jan 4, 2025

hargoniX approved these changes Jan 4, 2025

View reviewed changes

hargoniX added the will-merge-soon …unless someone speaks up label Jan 4, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 4, 2025

Trigger CI for leanprover/lean4#6219

2ceb62b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 4, 2025

Trigger CI for leanprover/lean4#6219

9d6b2c1

hargoniX merged commit b6f02ac into leanprover:ft-async Jan 6, 2025
28 of 29 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add async timer primitives based on libuv #6219

feat: add async timer primitives based on libuv #6219

algebraic-dev commented Nov 26, 2024

leanprover-community-bot commented Nov 26, 2024 •

edited

Loading

hargoniX left a comment

hargoniX commented Jan 4, 2025

feat: add async timer primitives based on libuv #6219

feat: add async timer primitives based on libuv #6219

Conversation

algebraic-dev commented Nov 26, 2024

leanprover-community-bot commented Nov 26, 2024 • edited Loading

hargoniX left a comment

Choose a reason for hiding this comment

hargoniX commented Jan 4, 2025

leanprover-community-bot commented Nov 26, 2024 •

edited

Loading