Shared mutable state

Stream: lean4

[Juan Pablo Romero]

Hi, Is there a way to share mutable state amongst tasks? (something like MVars in Haskell?)

[Gabriel Ebner]

You could abuse IO.Ref for this (which is an atomic reference) but that will busy-loop on contented accesses. If you wait a little, we'll soon have a Rust-style Mutex type for mutex-guarded shared mutable state.

[Gabriel Ebner]

https://github.com/gebner/lean4/blob/10983d956cca532fcd3bdd6e7cd30ee1b87532de/src/Lean/Mutex.lean

[Gabriel Ebner]

https://github.com/leanprover/lean4/issues/1280

[Juan Pablo Romero]

Nice!