[ base ] Add non-blocking and timeout variants for channelGet

[Matthew-Mosior]

Description

This PR adds a two new functions in System.Concurrency, channelGetNonBlocking and channelGetWithTimeout (only for the chez backend).

Credit to @emdash and @cypheon for review and feedback.

This PR closes #3424.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[emdash]

I'm not really a member of this project, so I can't approve it, but I'll at least provide some initial feedback.

Hopefully this will get some other folks to chime in.

[Matthew-Mosior]

I'm not really a member of this project, so I can't approve it, but I'll at least provide some initial feedback.

Hopefully this will get some other folks to chime in.

Thank you for taking your time to look this over and provide feedback.

[emdash]

I'm pretty satisfied with the general shape of this now. I will yield the conversation to more seasoned Idris devs.

[cypheon]

If I understand correctly, you introduced the generic object to/from Scheme conversion because, essentially you need to return a Maybe a from a %foreign scheme: function, but I think there are to better alternatives to that:

1. In the Scheme support code, directly return '() (which is the runtime encoding of Nothing or (box $RESULT) which corresponds to Just $RESULT.
   Advantage: less code, Disadvantage: couples the code to the runtime representation of Maybe a
2. Return a Scheme record like (define-record channel-result (present val)), (present is a boolean indicating if the result contains a value) along that, define two extra %foreign functions: prim_channelObjectIsPresent : ChannelObject -> Int and prim_channelObjectGet : ChannelObject -> a. This pattern is for example already used in the codebase here: libs/base/System/Clock.idr:237-241
   Advantage: more robust with regards to future changes in the runtime representation, Disadvantage: slightly more code

Both approaches share the advantage, that they don't couple the two functions directly to the Chez runtime and other backends can implement them by providing implementations for the 2 (or 4)%foreign functions related to non-blocking channel access.

Furthermore, it should be possible to implement blodwen-channel-get-with-timeout without a busy-waiting loop that repeatedly calls sleep:
Chez's condition-wait function takes an (optional) third argument to pass a timeout limit. This is already used here: support/chez/support.ss:460. Using that I think you can get rid of the sleep calls in the loop.

[Matthew-Mosior]

If I understand correctly, you introduced the generic object to/from Scheme conversion because, essentially you need to return a Maybe a from a %foreign scheme: function, but I think there are to better alternatives to that:

1. In the Scheme support code, directly return `'()` (which is the runtime encoding of `Nothing` or `(box  $RESULT)` which corresponds to `Just $RESULT`.
   Advantage: less code, Disadvantage: couples the code to the runtime representation of `Maybe a`

2. Return a Scheme record like `(define-record channel-result (present val))`, (`present` is a boolean indicating if the result contains a value) along that, define two extra `%foreign` functions: `prim_channelObjectIsPresent : ChannelObject -> Int` and `prim_channelObjectGet : ChannelObject -> a`. This pattern is for example already used in the codebase here: [libs/base/System/Clock.idr:237-241](https://github.com/idris-lang/Idris2/blob/ec74792a49bf4d22509172d1f03d153ffca1b95c/libs/base/System/Clock.idr#L237C1-L241C24)
   Advantage: more robust with regards to future changes in the runtime representation, Disadvantage: slightly more code

Both approaches share the advantage, that they don't couple the two functions directly to the Chez runtime and other backends can implement them by providing implementations for the 2 (or 4)%foreign functions related to non-blocking channel access.

Furthermore, it should be possible to implement blodwen-channel-get-with-timeout without a busy-waiting loop that repeatedly calls sleep: Chez's condition-wait function takes an (optional) third argument to pass a timeout limit. This is already used here: support/chez/support.ss:460. Using that I think you can get rid of the sleep calls in the loop.

Thank you for your feedback! I will work on implementing alternative 1.

Ah I see, I'll work on re-working blodwen-channel-get-with-timeout to use that additional timeout argument instead of using a sleep loop.

[Matthew-Mosior]

@cypheon

I've addressed your feedback via 6b13dc8 / fa50df7.

[cypheon]

This looks really good now! Thanks for taking the time for this non-trivial rework!

[jarlah]

if i can test this in my idris2-http fork that would be awesome :) i have a test there that just hangs. Hopefully I can rewrite the code to use one of these functions :)

[Matthew-Mosior]

if i can test this in my idris2-http fork that would be awesome :) i have a test there that just hangs. Hopefully I can rewrite the code to use one of these functions :)

Yeah I'm super excited for that work and to see it come to fruition! 😃 I think we're just waiting on a core maintainer review/approval/merged 🤞

[mattpolzin]

There should be nothing stopping someone from testing this commit against a local build of a fork of some library though, to be clear.

[jarlah]

if i can test this in my idris2-http fork that would be awesome :) i have a test there that just hangs. Hopefully I can rewrite the code to use one of these functions :)

Yeah I'm super excited for that work and to see it come to fruition! 😃 I think we're just waiting on a core maintainer review/approval/merged 🤞

i might need some help reviewing why it wont build though ... it seems to be both issues with installing idris2-lsp and runniing pack build from my fork of idris2 here jarlah@fa50df7 which i use here https://github.com/idris-community/idris2-http/blob/testing_chunked/pack.toml#L14

when running pack install everything completes. When i run pack build it fails

╰─ pack build
[ info ] Found local config at /home/jarlah/projects/idris2-http/pack.toml
[ info ] Using package collection nightly-241107
[ warning ] Package tls uses custom build hooks. Continue (yes/*no)?
yes
[ info ] Installing libraries:
- elab-util
- sop
- tls
[ info ] Installing library (with sources): elab-util
[ build ] 1/21: Building Language.Reflection.Syntax (src/Language/Reflection/Syntax.idr)
[ build ] Error: While processing right hand side of mkTy. When unifying:
[ build ] FC
[ build ] and:
[ build ] WithFC Name
[ build ] Mismatch between: FC and WithFC Name.
[ build ]
[ build ] Language.Reflection.Syntax:477:21--477:28
[ build ] 473 | |||
[ build ] 474 | ||| This is an alias for MkTyp EmptyFC.
[ build ] 475 | public export %inline
[ build ] 476 | mkTy : (name : Name) -> (type : TTImp) -> ITy
[ build ] 477 | mkTy = MkTy EmptyFC EmptyFC
[ build ] ^^^^^^^
[ build ]
[ build ] Error: While processing right hand side of claim. When unifying:
[ build ] FC
[ build ] and:
[ build ] WithFC IClaimData
[ build ] Mismatch between: FC and WithFC IClaimData.
[ build ]
[ build ] Language.Reflection.Syntax:491:30--491:37
[ build ] 487 | -> (opts : List FnOpt)
[ build ] 488 | -> (name : Name)
[ build ] 489 | -> (type : TTImp)
[ build ] 490 | -> Decl
[ build ] 491 | claim c v opts n tp = IClaim EmptyFC c v opts (mkTy n tp)
[ build ] ^^^^^^^
[ build ]
[ info ] Installing library (with sources): sop
[ build ] Uncaught error: EmptyFC:Failed to resolve the dependencies for sop:
[ build ] base-0.7.0; required elab-util any but no matching version is installed
[ build ]
[ info ] Installing library (with sources): tls
[ build ] Uncaught error: EmptyFC:Failed to resolve the dependencies for tls:
[ build ] base-0.7.0; contrib-0.7.0; network-0.7.0; linear-0.7.0; required sop >= 0.6.0 but no matching version is installed
[ build ]
[ fatal ] Error when executing system command.
Command: "/home/jarlah/.pack/install/fa50df76de7892dc42f5588a36fb5657a4299242/idris2/bin/idris2" "--build" "elab-util.ipkg"
Error code: 1

some incompabilities between latest main on idris2 and libraries? I got some real nerves doing these kinds of things, because its like swimming in a dark ocean with no land in sight 🤣 luckily i have my tricks to keep me sane :D

[Matthew-Mosior]

if i can test this in my idris2-http fork that would be awesome :) i have a test there that just hangs. Hopefully I can rewrite the code to use one of these functions :)

Yeah I'm super excited for that work and to see it come to fruition! 😃 I think we're just waiting on a core maintainer review/approval/merged 🤞

i might need some help reviewing why it wont build though ... it seems to be both issues with installing idris2-lsp and runniing pack build from my fork of idris2 here jarlah@fa50df7 which i use here https://github.com/idris-community/idris2-http/blob/testing_chunked/pack.toml#L14

when running pack install everything completes. When i run pack build it fails

╰─ pack build
[ info ] Found local config at /home/jarlah/projects/idris2-http/pack.toml
[ info ] Using package collection nightly-241107
[ warning ] Package tls uses custom build hooks. Continue (yes/*no)?
yes
[ info ] Installing libraries:
- elab-util
- sop
- tls
[ info ] Installing library (with sources): elab-util
[ build ] 1/21: Building Language.Reflection.Syntax (src/Language/Reflection/Syntax.idr)
[ build ] Error: While processing right hand side of mkTy. When unifying:
[ build ] FC
[ build ] and:
[ build ] WithFC Name
[ build ] Mismatch between: FC and WithFC Name.
[ build ]
[ build ] Language.Reflection.Syntax:477:21--477:28
[ build ] 473 | |||
[ build ] 474 | ||| This is an alias for MkTyp EmptyFC.
[ build ] 475 | public export %inline
[ build ] 476 | mkTy : (name : Name) -> (type : TTImp) -> ITy
[ build ] 477 | mkTy = MkTy EmptyFC EmptyFC
[ build ] ^^^^^^^
[ build ]
[ build ] Error: While processing right hand side of claim. When unifying:
[ build ] FC
[ build ] and:
[ build ] WithFC IClaimData
[ build ] Mismatch between: FC and WithFC IClaimData.
[ build ]
[ build ] Language.Reflection.Syntax:491:30--491:37
[ build ] 487 | -> (opts : List FnOpt)
[ build ] 488 | -> (name : Name)
[ build ] 489 | -> (type : TTImp)
[ build ] 490 | -> Decl
[ build ] 491 | claim c v opts n tp = IClaim EmptyFC c v opts (mkTy n tp)
[ build ] ^^^^^^^
[ build ]
[ info ] Installing library (with sources): sop
[ build ] Uncaught error: EmptyFC:Failed to resolve the dependencies for sop:
[ build ] base-0.7.0; required elab-util any but no matching version is installed
[ build ]
[ info ] Installing library (with sources): tls
[ build ] Uncaught error: EmptyFC:Failed to resolve the dependencies for tls:
[ build ] base-0.7.0; contrib-0.7.0; network-0.7.0; linear-0.7.0; required sop >= 0.6.0 but no matching version is installed
[ build ]
[ fatal ] Error when executing system command.
Command: "/home/jarlah/.pack/install/fa50df76de7892dc42f5588a36fb5657a4299242/idris2/bin/idris2" "--build" "elab-util.ipkg"
Error code: 1

some incompabilities between latest main on idris2 and libraries? I got some real nerves doing these kinds of things, because its like swimming in a dark ocean with no land in sight 🤣 luckily i have my tricks to keep me sane :D

I think you may need to use a different pack snapshot, I would try pack switch latest. I think there was some core language work that effected some libraries in that way if I'm not mistaken?

[mattpolzin]

Yes, the WithFC error will be resolved if building the latest of pack’s collection against the latest of the compiler. The relevant compiler change was made last week (followed by fixes for various libraries in pack’s database).

[jarlah]

i just gave to repeat what others have said before .. but seriously .. pack is so god damn good ... it just works .. such things as pack switch latest and pack build .. boom

[jarlah]

@Matthew-Mosior added a test here :) thanks for the tips .. it helped .. so i have full lsp help locally now on idris2 from your branch ;)

idris-community/idris2-http#15 (comment)

as mentioned there, we might need to do some type aliasing to make the new function work properly (or to comprehend the start request function

[Matthew-Mosior]

@Matthew-Mosior added a test here :) thanks for the tips .. it helped .. so i have full lsp help locally now on idris2 from your branch ;)

idris-community/idris2-http#15 (comment)

as mentioned there, we might need to do some type aliasing to make the new function work properly (or to comprehend the start request function

Awesome thanks for trying this out! I'm not by my computer right now, but will take a look asap!