Expression to string

Stream: lean4

[Yicheng Qian]

Is there an easy way to turn an expression into a string while printing the user name of fvars/mvars?
I'm trying to debug a custom tactic, but printing expressions as MessageData always crashes the Lean server, presumably because there are too many expressions to print and MessageData is expensive. However, Lean.Expr.dbgToString prints fvars/mvars as uniq..., which makes them hard to read. Calling MessageData.toString on the MessageData gives the same result as Lean.Expr.dbgToString.

[Damiano Testa]

Could you give an example of what you want? Maybe simply modifying inspect in this thread to print what you want for fvars/mvars would be enough?

[Mario Carneiro]

lean 3 used to have a depth limit in the pretty printer, but I can't find that option in lean 4 or in the code

[Mario Carneiro]

you could hack something together where you depth-truncate the expr itself before printing it

[Yicheng Qian]

Mario Carneiro said:

you could hack something together where you depth-truncate the expr itself before printing it

What does "depth-truncate" expression mean? Also I think in my case, the problem is caused by there being too many expressions to print, not because individual expressions are too large.

[Mario Carneiro]

meaning replace all subexpressions at depth > n with some nonsense like .lit "..."

[Mario Carneiro]

it won't typecheck of course, but it might be well formed enough for the delaborator to accept it

[Mario Carneiro]

If you have too many expressions, have you considered... not printing so many expressions?

[Yicheng Qian]

I'm trying to debug the saturation procedure of duper and needs to print either the result of each inference step or the final set of clauses. For nontrivial examples both of them contains hundreds of expressions. If duper saturates on examples that are unsat, I think I have no choice but to print (all the inference steps/the final set of clauses) because I don't know which inference rule was buggy.

[Mario Carneiro]

what about using f! to turn it into a plain format?

[Yicheng Qian]

It works, but similar to the previous workaround, it does not print the username of fvars/mvars

[Yicheng Qian]

Oh, probably I can turn the fvars/mvars into const with their username.

[Yicheng Qian]

Mario Carneiro said:

meaning replace all subexpressions at depth > n with some nonsense like .lit "..."

Inspired by this.