Available options for compiler and tracing output

Stream: lean4 dev

[Tom]

I have tried looking at some code using set_option ... true in to start looking at LCNF and to look a bit more into what the compiler is doing. Are these options documented anywhere?

As a second follow-up, I was trying to see if there's a way to see what the result of instance search is. For example, if I have e.g.

#eval Functor.map (.*2) [1,2,3]

and do the following:

set_option trace.Meta.synthInstance true in
#eval Functor.map (.*2) [1,2,3]

I can see the output of instance search/resolution. However, is there a way to see the "transformed" code, where e.g. the Functor.map has been "substituted" with List.map, as per map in the functor instance?
I can for example look at the code at the LCNF level, e.g. using set_option trace.Compiler true but that's a bit low level.

Finally, is there an equivalent of the above, say to see what the result of operator application is? E.g. #eval (.*2) <$> [1,2,3]

Thanks!

[Henrik Böving]

Well there isn't really any substitution happening at the Lean level. For the the entirety of Lean, excluding the compiler, this is literally Functor.map but the implicit [Functor List] instance will have been inserted as an explicit argument in the internal Expr version of this you can make this visible like so:

set_option pp.explicit true in
#check Functor.map (.*2) [1,2,3]

Which will give you the term that Lean will actually operate on internally:

@Functor.map List List.instFunctorList Nat Nat (fun a => @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) a 2)
  (@List.cons Nat 1 (@List.cons Nat 2 (@List.cons Nat 3 (@List.nil Nat)))) : List Nat

While using List.map could be proven to be equivalent (in fact even definitionally equivalent) Lean will never do this without the user telling it to do so ever. Only when we move to LCNF and start simplifying the code we will start to substitute these things in.

[Henrik Böving]

Oh and regarding the question of where these options are documented...basically nowhere since their definitions are spread all over the code and we are adding new ones every other day but if you do set_option the auto completion will give you an exhaustive list of suggestions

[Tom]

Perfect - the pp.explicit is what I was looking for - thanks! What does pp stand for in this context? I assume it's not the "PreProcessor" :smile:

[Henrik Böving]

pretty printer

[Tom]

Henrik Böving said:

Oh and regarding the question of where these options are documented...basically nowhere since their definitions are spread all over the code and we are adding new ones every other day but if you do set_option the auto completion will give you an exhaustive list of suggestions

Thanks, I noticed but they are still alien to me; I assume most of them are pass-specific anyway.

[Tom]

Henrik Böving said:

pretty printer

D'oh!

[Mario Carneiro]

Most of the options are not compiler related at all, the ones for the new compiler are primarily in trace.Compiler

[Mario Carneiro]

the main useful one is trace.Compiler.result if you want to see the final result of compilation

[Mario Carneiro]

or trace.compiler.ir.result for the result of the old compiler

[Tom]

That's great to know, thank you both for your help!