From 6ebae968a7d8a2404735e83d63cd7dec193e301b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jun 2022 13:00:59 -0700 Subject: [PATCH] feat: use `IO.getRandomBytes` to initialize random seed See https://github.com/leanprover/lean4-samples/pull/2 --- RELEASES.md | 2 ++ src/Init/Data/Random.lean | 4 +++- src/Lean/Server/FileWorker.lean | 2 -- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index d730d6032e..3605ded476 100644 --- a/RELEASES.md +++ b/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 diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index 42cec3efdd..b00e375163 100644 --- a/src/Init/Data/Random.lean +++ b/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) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index ff62e535e8..ce9c819f3f 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/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