Zulip Chat Archive

Stream: lean4

I know Lean has IO.Mutex, but does it have anything resembling a read/write lock?

If not, how feasible/easy would it be to implement a version of it?

If we're just shooting for something like https://doc.rust-lang.org/std/sync/struct.RwLock.html that relies on the underlying OS implementation, seems doable

Coming from Rust, that's exactly what I had in mind :grinning:

So if I understand this correctly there would be some C code / OS hook involved

My understanding is that in this case, that should be in core since std4 does not feature such low-level code

And Mutex is already there

Is that correct? @Gabriel Ebner

I would be interested in taking a shot at contributing RwLock, especially since there's already code for Mutex so even I might be able to do it

I think it's pretty straightforward to build a (non-reentrant) read-write mutex using regular mutexes and condition variables (which we both have).

Interesting, and would you say it'd be better putting that in std if it's pure Lean?

I have no idea if Mario wants to have extra mutex stuff in std, but there's no need for such an implementation to be in core.

If there is a good API for it and core doesn't want it I don't see any issue with putting it in std

Last updated: Dec 20 2023 at 11:08 UTC