## Stream: lean4

### Topic: Code generation

#### Calvin Lee (Mar 11 2021 at 01:25):

Would there be any easy way to generate a lot of constants automatically at once with random values?

#### Mario Carneiro (Mar 11 2021 at 05:55):

In lean 3 you can do that by calling add_decl to create new definitions, where the definition is a random value turned into a literal expression

#### Mario Carneiro (Mar 11 2021 at 06:12):

Here's some code that should work, and currently works in the command line but crashes the server for me:

import Lean

open Lean

def test : CoreM Unit := do
let decl := Declaration.defnDecl {
name        := foo,
levelParams := [],
value       := toExpr (← IO.rand 0 100),
type        := mkConst Nat,
hints       := ReducibilityHints.regular 0,
safety      := DefinitionSafety.safe
}
match (← getEnv).addAndCompile {} decl with
| Except.ok    env => setEnv env
| Except.error kex => pure ()

#eval test

#print foo
-- def foo : Nat :=
-- 77


#### Calvin Lee (Mar 11 2021 at 22:26):

Hmm, is there any way to do this without the #eval?

#### Leonardo de Moura (Mar 11 2021 at 22:52):

Here is an example using the macro system.

/- Helper syntax for defining the real macro. -/
syntax "gen_random_defs%" ident num num num : command

/-
gen_random_defs id n s creates n declarations of the form

def id_<idx> : Nat := <random value>

The "random values" are generated using the function stdNext and "seed" s
-/
macro "gen_random_defs" id:ident n:num s:num : command =>
(gen_random_defs% $id$n $s 1) -- s and 1 are the "seeds" for the random number generator macro_rules | (gen_random_defs%$id $n$s1 $s2) => open Lean in let (val, ⟨s1, s2⟩) := stdNext ⟨s1.toNat, s2.toNat⟩ let n := n.toNat let currId := id.getId.appendIndexAfter n if n == 0 then return mkNullNode else (def$(mkIdentFrom id currId) := $(quote val) gen_random_defs%$id $(quote (n-1))$(quote s1) $(quote s2)) gen_random_defs foo 4 10 -- Creates foo_1 ... foo_4 using random seed 10 #print foo_1 #print foo_2 #print foo_3 #print foo_4  #### Calvin Lee (Mar 17 2021 at 20:40): Is there any way to access IO in term or command macros in order to get rid of the seed argument here? I'm trying to write something like /- rand_nat_const creates a random Nat in the StdGen range -/ macro "rand_nat_const" : term => do ($(quote (<-(IO.rand (stdRange.fst) (stdRange.snd)))))


It looks like no

#### Mario Carneiro (Mar 17 2021 at 21:05):

macros live in the MacroM monad which is pure

#### Mario Carneiro (Mar 17 2021 at 21:10):

Although you might not need it since MacroM implements MonadRef

#### Calvin Lee (Mar 17 2021 at 21:10):

I see, if I have  : command does it live in CommandM instead? and does that include IO?

#### Mario Carneiro (Mar 17 2021 at 21:11):

No, all macros live in MacroM`

#### Mario Carneiro (Mar 17 2021 at 21:12):

but that just means that it is pure during macro expansion, you can just do your computation after macro expansion

#### Calvin Lee (Mar 17 2021 at 21:14):

Indeed
the issue is I would like to avoid the randomness on runtime

#### Mario Carneiro (Mar 17 2021 at 21:14):

I'm not sure what you mean. It's the same either way

#### Mario Carneiro (Mar 17 2021 at 21:16):

It's not really clear what counts as "runtime" here

#### Mario Carneiro (Mar 17 2021 at 21:17):

If you have a command-like that adds definitions to the environment, that will run when the lean file is processed. The olean files will contain the resulting definitions

#### Mario Carneiro (Mar 17 2021 at 21:17):

if this is then used in a dependent lean file, it will be as if you wrote all those definitions, so I guess it's "compile time"?

#### Mario Carneiro (Mar 17 2021 at 21:18):

That said, a lean file that elaborates differently depending on the phase of the moon seems like a bad idea

#### Calvin Lee (Mar 17 2021 at 21:36):

indeed but it's awfully convenient for this case where I want an algorithm to have some random parameters (for efficiency reasons) but I don't want it to be random on runtime (I don't want one of my runs to get some bad seed)