How to Debug An Extension

Stream: lean4

[Jeremy Salwen]

I am interested in debugging the NormCastExt extension to better understand how it works (https://github.com/leanprover/std4/blob/5aa4ab4f0c096e8d0600e3ae41b8577dcf6edb13/Std/Tactic/NormCast/Ext.lean#L108). I'd like to print out the values of the instance

import Std.Tactic.NormCast.Ext
#eval Std.Tactic.NormCast.normCastExt

In order to see what its value is.

But it doesn't seem printable:

expression
  Std.Tactic.NormCast.normCastExt
has type
  Std.Tactic.NormCast.NormCastExtension
but instance
  Lean.MetaEval Std.Tactic.NormCast.NormCastExtension
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

Is there a way I can print it out to see how my declarations affect its value, or is there another way I should be investigating this?

[Jeremy Salwen]

Bump on this thread, does anyone have an idea how to do it?

[Eric Wieser]

What do you expect #eval to do here?

[Eric Wieser]

Did you mean to use #check or #print?

[Chris Bailey]

It looks like it's three simp sets, so I guess #eval would show you whatever the Repr instance is for that NormCastExtension. You need an instance of Repr, so you'll have to figure out what information you want to view and implement Repr for NormCastExtention in a way that shows the relevant information.

[Chris Bailey]

https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/NormCast/Ext.html#Std.Tactic.NormCast.NormCastExtension

[Eric Wieser]

It seems highly unlikely to me that there is a sensible implementation of Reprfor docs4#Std.Tactic.NormCast.NormCastExtension, so I suspect that's not helpful advice.

[Jeremy Salwen]

Yeah I tried to see if it was simple to define a ToString, but it seems like it's un-Repr-able types nested inside un-Repr-able types. So it would be a big undertaking to define ToString. (Also, I don't really understand most of the contained types, and printing them out was part of how I wanted to understand them).

[Jeremy Salwen]

Eric Wieser said:

Did you mean to use #check or #print?

Yeah I wasn't clear on the different between #check and #print, I just wanted to see some representation of the value of normCastExt.

[Wojciech Nawrocki]

Yeah, the type NormCastExtension is the configuration data of the environment extension, not its "actual" data present in the environment. A Repr instance could at best print some of this configuration. The pattern for accessing the actual data is to get an Environment object and then query it using methods on the extension.

[Jeremy Salwen]

I have spent more time investigating this on my own since I originally posted, and my conclusion was that I had two difficulties, first that it wasn't like "a real value" it was hidden behind Meta Monad stuff (or something like that), and the second part was that I couldn't figure out how to just print a value without recursively defining ToString implementations for a bunch of types.

[Wojciech Nawrocki]

Here is an example (I don't know how NormCastExtension works, so this is just a guess as to which data you'd want to print out):

#eval (do
  -- Note that `getTheorems` is a convenience wrapper around
  -- `ext.getState (← getEnv)`
  let thms ← Std.Tactic.NormCast.normCastExt.down.getTheorems
  thms.lemmaNames.foldM (fun _ nm => do
    IO.println nm.key
    pure ()) ()
   : Lean.MetaM Unit)

[Wojciech Nawrocki]

Note that we have to do the access in MetaM (or at least CoreM) because that's the monad which has access to the environment.

[Jeremy Salwen]

Wojciech Nawrocki said:

Note that we have to do the access in MetaM (or at least CoreM) because that's the monad which has access to the environment.

Ok thanks! I think this answers the question about how to handle the MetaM wrapping. It still seems like there is a lot of work to just dump the value of these objects? Is there no automated way to see a representation of some object you didn't define without having to define functions which walk through all its (recursive) fields?

[Wojciech Nawrocki]

Is there no automated way to see a representation of some object you didn't define without having to define functions which walk through all its (recursive) fields?

The automated way would be to implement a deriving handler so that you can write deriving instance PrintAllTheStuff for MyType and then use #eval PrintAllTheStuff.print (t : MyType), but there is no such deriving handler at the moment.

[Jeremy Salwen]

I see, the debugging page also mentions that debuggers can't print out sensible representations of lean values: https://leanprover.github.io/lean4/doc/dev/debugging.html . So there is basically no way to inspect something without hand rolling the Repr implementation for all relevant types?

[Wojciech Nawrocki]

There is a deriving handler for Repr, you can use deriving instance Repr for MyType. For values which need access to monad state you have to write the code manually.

[Eric Wieser]

I doubt you are at the level of debugging where you need to invoke gdb on Lean code, which that page is describing

[Eric Wieser]

That should only be needed to debug things in lean itself

[Jeremy Salwen]

Eric Wieser said:

That should only be needed to debug things in lean itself

I see, I was just thinking about other languages, such as Java, where even if you don't define toString, you can also open the debugger and see a tree representation of the values of any variable.

[Eric Wieser]

Not every type has a meaningful repr; what would you expect the repr of fun x => x*x : Nat -> Nat to be?

[Jeremy Salwen]

Wojciech Nawrocki said:

There is a deriving handler for Repr, you can use deriving instance Repr for MyType. For values which need access to monad state you have to write the code manually.

Ohh, I see, I can derive Repr automatically, I just need to derive it for every type in the hierarchy. So not ideal but I don't have to manually implement Repr for anything.

[Eric Wieser]

This feels like an #xy problem though; you're asking "how do I get repr for my norm_num extension" but presumably your question is actually "what tools are available to debug [vague description of problem] in my norm_num extension"?

[Jeremy Salwen]

Eric Wieser said:

This feels like an #xy problem though; you're asking "how do I get repr for my norm_num extension" but presumably your question is actually "what tools are available to debug [vague description of problem] in my norm_num extension"?

I suppose so, yeah, my question is how to debug it

"Is there a way I can print it out to see how my declarations affect its value, or is there another way I should be investigating this?"

[Eric Wieser]

I think the answer is "the value isn't affected at all, because declaring new constants doesn't affect the value of other constants in the environment"

[Eric Wieser]

Jeremy Salwen said:

Ohh, I see, I can derive Repr automatically, I just need to derive it for every type in the hierarchy. So not ideal but I don't have to manually implement Repr for anything.

I don't know how to apply a deriving handler after the fact, but even if you do it manually it becomes pretty obvious that there's no useful information available to you:

import Std.Tactic.NormCast.Ext

instance : Repr (Lean.ScopedEnvExtension.Descr α β σ) where
    reprPrec x _ := "{ name := " ++ repr x.name ++ " }"

instance : Repr (Lean.ScopedEnvExtension α β σ) where
    reprPrec x _ := "{ descr := " ++ reprArg x.descr ++ ", ext := _ }"

instance : Repr (Std.Tactic.NormCast.NormCastExtension) where
    reprPrec x _ := Std.Format.bracket "{ " (
            "up := " ++ reprArg x.up ++ "," ++ Std.Format.line ++
            "down := " ++ reprArg x.down ++ "," ++ Std.Format.line ++
            "squash := " ++ reprArg x.squash) " }"

#eval Std.Tactic.NormCast.normCastExt

[Jeremy Salwen]

Eric Wieser said:

Not every type has a meaningful repr; what would you expect the repr of fun x => x*x : Nat -> Nat to be?

For example in Java it would represent it using the file and line number of the definition, which is not great, but better than nothing.

[Jeremy Salwen]

Eric Wieser said:

Jeremy Salwen said:

Ohh, I see, I can derive Repr automatically, I just need to derive it for every type in the hierarchy. So not ideal but I don't have to manually implement Repr for anything.

I don't know how to apply a deriving handler after the fact, but even if you do it manually it becomes pretty obvious that there's no useful information available to you:

import Std.Tactic.NormCast.Ext

instance : Repr (Lean.ScopedEnvExtension.Descr α β σ) where
    reprPrec x _ := "{ name := " ++ repr x.name ++ " }"

instance : Repr (Lean.ScopedEnvExtension α β σ) where
    reprPrec x _ := "{ descr := " ++ reprArg x.descr ++ ", ext := _ }"

instance : Repr (Std.Tactic.NormCast.NormCastExtension) where
    reprPrec x _ := Std.Format.bracket "{ " (
            "up := " ++ reprArg x.up ++ "," ++ Std.Format.line ++
            "down := " ++ reprArg x.down ++ "," ++ Std.Format.line ++
            "squash := " ++ reprArg x.squash) " }"

#eval Std.Tactic.NormCast.normCastExt

I think this needs to be combined with the MetaM monad unwrapping like Wojciech suggested. But if you can't derive repr after declaration then that is a problem... :(

[Wojciech Nawrocki]

But if you can't derive repr after declaration then that is a problem...

To make this super-clear, I don't think you have to worry about Repr at all in this case because Repr is only useful for pure values. When printing out values of environment extensions which use MetaM, you have to access monad state which is not something you can do in Repr implementations.

[Wojciech Nawrocki]

I think the answer is "the value isn't affected at all, because declaring new constants doesn't affect the value of other constants in the environment"

I'm assuming the question is not about the value of normCastExt (which is indeed left unaffected) but rather about the state stored for normCastExt in the environment, which is affected.

[Jeremy Salwen]

Wojciech Nawrocki said:

But if you can't derive repr after declaration then that is a problem...

To make this super-clear, I don't think you have to worry about Repr at all in this case because Repr is only useful for pure values. When printing out values of environment extensions which use MetaM, you have to access monad state which is not something you can do in Repr implementations.

Hmm, I think the best way to describe my thinking is the following code:

#eval (do
  let thms ← Std.Tactic.NormCast.normCastExt.down.getTheorems
-- Now on this line I want to actually print out thms.  How do I do that?
) ()
   : Lean.MetaM Unit)

[Wojciech Nawrocki]

I think because this is fairly low-level stuff, the only answer to 'how do I print x' is 'read code in Lean/mathlib4 that does something with x and figure out how to print it'. For example this prints the post-traversal discrimination tree (which might not be what you want):

import Mathlib.Data.Rat.Basic
import Std.Tactic.NormCast.Ext

#eval (do
  let thms ← Std.Tactic.NormCast.normCastExt.squash.getTheorems
  IO.println thms.post.format
  : Lean.MetaM Unit)

[Wojciech Nawrocki]

Also, I made a mistake above; I used logInfo but you should use IO.println. logInfo needs lean4#1967 to work.

[Jeremy Salwen]

Wojciech Nawrocki said:

I think because this is fairly low-level stuff, the only answer to 'how do I print x' is 'read code in Lean/mathlib4 that does something with x and figure out how to print it'. For example this prints the post-traversal discrimination tree (which might not be what you want):

import Mathlib.Data.Rat.Basic
import Std.Tactic.NormCast.Ext

#eval (do
  let thms ← Std.Tactic.NormCast.normCastExt.squash.getTheorems
  IO.println thms.post.format
  : Lean.MetaM Unit)

Ok Thanks Wojciech! The .format function was definitely helpful in combination with everything else you've said, and I've been able to print out and understand the data to my satisfaction!