Generated definition can #reduce but not #eval

Stream: metaprogramming / tactics

[Markus de Medeiros]

I'm trying to figure out how to write metaprograms which add definitions the environment. I have figured out how to add definitions which reduce, but for some reason, I cannot figure out how to get them to compile. Any advice?

def MyDefinition : DefinitionVal :=
  mkDefinitionValEx `myDef []
    (.const `Nat [])
    (.app (.app (.app (.const `OfNat.ofNat [0]) (.const `Nat [])) (.lit <| .natVal 5)) (.app (.const `instOfNatNat []) (.lit <| .natVal 5)))
    (.regular 5)
    .safe
    [`myDef]

#eval addDecl (.defnDecl MyDefinition)

#check myDef -- myDef : Nat
#reduce myDef -- 5
#eval myDef
-- (interpreter) unknown declaration '_eval'
-- failed to compile definition, compiler IR check failed at '_eval._closed_0'. Error: depends on declaration 'myDef', which has no executable code; consider marking definition as 'noncomputable'

[Robin Arnez]

Use docs#Lean.addAndCompile instead

[Markus de Medeiros]

Oh great, thank you!

[Auguste Poiroux]

Interesting! There is a similar issue in the REPL when using the pickling/unpickling feature. It is relying on Lean's replayConstant method which is using addDecl (or more preciselyaddDeclCore). Is there a reason to only do addDecl and not compileDecl when replaying constants?

[Robin Arnez]

Some constants might not be computable

[Markus de Medeiros]

Yeah actually I ended up going back to addDecl because I used a recursor, lol

[Kyle Miller]

You can do compileDecl (logErrors := false) though to try compiling everything.

Maybe the deal is that the use case for REPL has been replaying proofs mostly, so compiled definitions have not been relevant? Maybe it ought to record which definitions were compiled when pickling, to be able to accurately re-run compileDecl.

[Auguste Poiroux]

Thanks for the help! I have other questions then ^^ What are the use-cases of the replayConstant method in Lean? The fact that computable constants are not compiled do not cause issues in these other use-cases?
Also, do we have access to the computability of the constants in the info field of the replayConstant? If so we can probably add a compileDecl automatically in these cases inside replayConstant, right?

[Kyle Miller]

The computability isn't stored in the ConstantInfo, and they're also the forms of the definitions that have been "compiled" for the kernel to eliminate explicit recursion. For example, if you have a structurally recursive definition on Nat, it's been "compiled" to a Nat.brecOn.

While compileDecl function is used directly on non-recursive definitions, for recursive and mutually recursive definitions instead the compiler is given "predefinitions", the definitions still in the explicitly recursive form.

To support compilation, you'd need to know which definitions are the ones that are supposed to actually get compiled. First, there's an environment extension that explicitly records this (I'm not sure exactly which one to look at). Second, you need to know which declarations correspond to the predefinition. For example, if f is recursive, then f._unsafe_rec is the corresponding partial definition that's compiled by compileDecl; it's an actual separate declaration with its own ConstantInfo that's been kernel-checked too. With mathlib, if you put whatsnew in before a declaration you can see all the environment modifications.

So, I think it should be possible to compile the declarations in a replayed environment but (1) you need more precise information about what was compiled and (2) you need to figure out how to redo some of the logic to make sure the compiler knows that these auxiliary declarations have the compiled code for the corresponding declarations.

It's worth mentioning that compiling declarations can happen after the environment is replayed.

I notice that replay doesn't include unsafe or partial definitions. Those are strictly necessary for this to succeed. The logic will also need to be modified to deal with the all field in Lean.DefinitionVal to add complete sets of mutually recursive partial definitions to the kernel simultaneously, otherwise the kernel will reject these definitions and replay will fail, even if you haven't yet gotten to compiling definitions.

[Auguste Poiroux]

Wow, thank you very much for such a detailed answer and for looking into this! This is indeed much more complicated than I thought. And so, what about doing the brute-force approach you suggested first, i.e. compileDecl (logErrors := false) (in topological order)? Would it be enough? Could it cause new issues?

[Kyle Miller]

I think the only thing to worry about is that there's a chance things won't be compiled even if you thought they'd be. Maybe you'll uncover some exciting exceptions. (Likely you can catch them with try/catch, and maybe if you want to be safe, restore the environment on failure; the code for withoutModifyingEnv' is a good reference.)

If your module only has non-recursive definitions, and nothing is marked partial, I'd expect success.