feat: use IO.getRandomBytes to initialize random seed

See https://github.com/leanprover/lean4-samples/pull/2

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* Use `IO.getRandomBytes` to initialize random seed for `IO.rand`. See discussion at [this PR](https://github.com/leanprover/lean4-samples/pull/2).
+
 * Improve dot notation and aliases interaction. See discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/282946185) for additional details.
   Example:
   ```lean

src/Init/Data/Random.lean

@@ -112,7 +112,9 @@ def randBool {gen : Type u} [RandomGen gen] (g : gen) : Bool × gen :=
   let (v, g') := randNat g 0 1
   (v = 1, g')
 
-initialize IO.stdGenRef : IO.Ref StdGen ← IO.mkRef mkStdGen
+initialize IO.stdGenRef : IO.Ref StdGen ←
+  let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8))
+  IO.mkRef (mkStdGen seed)
 
 def IO.setRandSeed (n : Nat) : IO Unit :=
   IO.stdGenRef.set (mkStdGen n)

src/Lean/Server/FileWorker.lean

@@ -488,8 +488,6 @@ def workerMain (opts : Options) : IO UInt32 := do
   let o ← IO.getStdout
   let e ← IO.getStderr
   try
-    let seed ← (UInt64.toNat ∘ ByteArray.toUInt64LE!) <$> IO.getRandomBytes 8
-    IO.setRandSeed seed
     let exitCode ← initAndRunWorker i o e opts
     -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
     -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code