pretty print for elaborator input?

Stream: general

[Fabian Glöckle]

We're wondering whether Lean4 has found a solution to the following problem: when copy-pasting pretty printed terms back into a Lean file, they frequently won't resolve (due to missing casts etc). Are there settings for unelaborator and elaborator that make them inverses?
cc @Amaury Hayat @gwennl

[Kyle Miller]

You could try setting set_option pp.analyze true, which adds in type ascriptions and @ annotations. It's not perfect though.

[Kyle Miller]

Of course, you can set set_option pp.all true, which should always work, at the cost of having very large terms.

[Fabian Glöckle]

In Lean3 I remember that even pp.all true wouldn't parse back the same; does it now?

[Eric Wieser]

No, it still doesn't:

def «forall» := 1

set_option pp.all true in
#check «forall» -- forall

#check forall -- error

[Kyle Miller]

That's a bug Eric, it's planned to be fixed.

[Kyle Miller]

@Fabian Glöckle I remember there were some bugs in the Lean 3 pretty printer, and it's possible you ran into them.

In principle, pp.all true should work. Please report any examples where it doesn't.

[Kyle Miller]

Also, if pp.analyze true doesn't work, it might be helpful having examples. It's drifted a bit, surely has issues, and has been getting very little attention, but reporting issues about it could help put resources into improving it.

[Fabian Glöckle]

cool, thanks so much!