StdGen (IORef?) Bug

Stream: lean4

[Henrik Böving]

While porting Control.Random to Lean 4 for my quickcheck experimentation I noticed that:

def foo : IO Unit := do
  let rng ← IO.stdGenRef.get
  IO.println s!"Random!: {Prod.fst $ RandomGen.next rng}"

#eval foo

will actually hang on the #eval directive, is this intended? I'm guessing this is related to fact that this is trying to obtain an IO.Ref value?

[Wojciech Nawrocki]

I am seeing

terminate called after throwing an instance of 'lean::exception'
  what():  cannot evaluate `[init]` declaration 'IO.stdGenRef' in the same module

in the output when I try this.

[Henrik Böving]

Hm for me on leanprover/lean4:nightly-2022-03-05 it just hangs in my emacs

Either way that's probably a bug right?

[Wojciech Nawrocki]

I think so, the initializer for IO.stdGenRef should run on startup, not when the #eval is executed.

[Sebastian Ullrich]

Should work now