Code generation

Stream: lean4

[Calvin Lee]

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

[Mario Carneiro]

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]

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]

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

[Leonardo de Moura]

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]

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)))))

but it seems I can only use the reader monad here

[Mario Carneiro]

It looks like no

[Mario Carneiro]

macros live in the MacroM monad which is pure

[Mario Carneiro]

Although you might not need it since MacroM implements MonadRef

[Calvin Lee]

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

[Mario Carneiro]

No, all macros live in MacroM

[Mario Carneiro]

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

[Calvin Lee]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Calvin Lee]

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)
Also it's nice because I don't have to worry about threading a reader through everything, especially if I want to prove things about this (which I want to be immutable)

[Paul-Olivier Dehaye]

(deleted)

[Max Nowak 🐉]

You are mixing up two concepts. For one, we have the "Propositions as types" thing which is the theory that Lean is based on, where proofs have a computational interpretation. You could run these proofs, but this is completely useless, as we are only interested in the existence of those proofs. This is all the stuff that lives in Prop. The other concept is the code generation itself, where we only care about everything non-Prop. We throw the Prop stuff away once we have the code.

[Max Nowak 🐉]

Rip post :(

[Kevin Buzzard]

It's still visible in the edit history (making deletion kind of pointless)

[Paul-Olivier Dehaye]

You guys are quick. I posted what's below and then realized it was threaded with a different conversation and thus tried to delete, which indeed is pointless.

Hi everyone. Lean is advertised at being relevant for code generation. My expectation reading that is that I would be able to chose a target language and compile Lean code to that language. Instead, all I can find in relation to Lean-generated code is that checking a math proof is like running a program, so we will compile Lean proofs to fast verified C code and run that to check the proof. My confusion might stem from my lack of awareness of non-math uses of Lean.

Q1. Is this understanding correct for the traditional use of Lean to generate code?
Q2. Are there instances where Lean was used to generate code in other languages? What advantages did Lean provide there?
Q3. If the answer to Q2 is no, why not? Are there alternatives you can suggest?

(my apologies if this is not the right forum to ask such questions)

[Paul-Olivier Dehaye]

@Max Nowak 🐉 when you say "The other concept is the code generation itself, where we only care about everything non-Prop", you refer to C code generation as I described, correct?

I guess I don't have definite answers to Q2 and Q3 then. Would it be possible to target something else than C? Could Lean generate Python code for instance?

[Kyle Miller]

Max is referring to "computational relevance". Only computationally relevant Lean code gets compiled, which excludes proofs.

The compilation pipeline right now is that definitions get converted to an intermediate representation (IR), and that can either be executed in a VM, or it can be translated to C, and that C is compiled to executable code.

I think there was work on translating that IR to JavaScript. In principle, yes, you should be able to translate this IR to Python, but maybe for efficiency it would be better to use the generated C and use Python's ffi.

[Kyle Miller]

"Compiled" might be an overloaded word here. All Lean code, including proofs, gets parsed, elaborated, and typechecked. This is the frontend to a normal compiler. Then there's the backend of a compiler, which includes code generation, and that is what we tend to refer to as compilation I believe. This sort of compilation only applies to things than meaningfully execute.

[Kyle Miller]

By the way, most of the Lean 4 system is written in Lean 4. If you look at the stage0 folder in the repository, that is the C code that the compiler generated from the Lean 4 sources.