random number generator

Stream: Is there code for X?

[Kenny Lau]

Do we have an RNG? Presumably it will take in the system time in some way or another

[Chris Hughes]

I remember seeing one somewhere in core I think.

[Kenny Lau]

there's io.rand in https://github.com/leanprover-community/lean/blob/master/library/system/io.lean

[Kenny Lau]

but it doesn't use the system time

[Reid Barton]

You could read bytes from /dev/urandom (probably)

[Kenny Lau]

how do you read a file?

[Chris Hughes]

It's an actual function, so you can prove theorems about it if you want

[Kenny Lau]

I just want random numbers for a programming kata

[Reid Barton]

like this: https://github.com/leanprover-community/lean/blob/master/leanpkg/leanpkg/manifest.lean#L105

[Kevin Buzzard]

Kenny Lau said:

I just want random numbers for a programming kata

I would recommend 37

[Jalex Stark]

Kenny Lau said:

I just want random numbers for a programming kata

you want the tests to be random?
you could generate ~10 tests, hardcode them in, and not expose them to the user

[Kenny Lau]

that is impossible, as demonstrated by the back-and-forth in https://leanprover.zulipchat.com/#narrow/stream/238266-Codewars/topic/hackproofing.20programming.20katas

[Jalex Stark]

oof

[Yaël Dillies]

How does one use randomness? I'm trying to understand file#control/random ...

[Yaël Dillies]

Can it only be used within tactics? This doesn't work because it's missing {g : Type} [random_gen g].

import control.random

#eval rand.random_r (2 : ℕ) 2 le_rfl = 2 -- don't know how to synthesize placeholder

[Yaël Dillies]

Ohoh! I think I figured out

import control.random

#eval rand_nat (mk_std_gen 37) 0 2564645983587834878

Replace 37 by whatever you want it will generate another random number.

[Kevin Buzzard]

Is 37 not random enough for you?

[Mario Carneiro]

obligatory XKCD: https://xkcd.com/221/