elaborating from InfoTree

Stream: lean4

[Patrick Massot]

Assume I have a docs4#Lean.Elab.TacticInfo object info and I get some Syntax object derived from part of info.stx. Can I elaborate this to an Expr?

[Patrick Massot]

@Sebastian Ullrich do you know about the above question? Is there a magic monad lifting or hidden state to save me or should a I somehow recreate a TermElabM context by hand?

[Wojciech Nawrocki]

@Patrick Massot what are you trying to do using this? The syntax for a TacticInfo is generally going to be a tactic which you could evaluate with evalTactic. But you should generally not have to do this.

[Patrick Massot]

evalTactic is even worse than elabTerm from this point of view since it needs to be in the TacticM monad, right?

[Patrick Massot]

The context is trying to translate a tactic proof into natural language.

[Sebastian Ullrich]

So there's a syntactic term embedded in info.stx and you want to (re-)elaborate it?

[Wojciech Nawrocki]

What Expr do you expect to get out of this? The code of the tactic metaprogram being run? The target / goal type? Something else?

[Patrick Massot]

Yes. It would be even better to access the result of the prior elaboration but I guess this isn't recorded anywhere.

[Sebastian Ullrich]

It should be, there should be a TermInfo node nested in the tactic node

[Sebastian Ullrich]

Are we talking about a set of specific tactics?

[Patrick Massot]

For instance if you have in you proof apply my_quantified_assumption my_object then I want the expression corresponding to my_quantified_assumption my_object.

[Patrick Massot]

Sebastian Ullrich said:

It should be, there should be a TermInfo node nested in the tactic node

Oh indeed!

[Patrick Massot]

I didn't open enough nested stuff!

[Patrick Massot]

So this was a stupid question, I'm sorry.

[Sebastian Ullrich]

That's the advantage of using Emacs, I don't have tree nodes I can open to begin with

[Wojciech Nawrocki]

trace.Elab.info is not currently collapsible however! It shows the whole thing at once.

[Patrick Massot]

Actually I don't know how to get a nice tree in VSCode. We have code dumping xml that I then open in Firefox.

[Patrick Massot]

Can you display collapsible InfoTrees in VSCode?

[Gabriel Ebner]

See also https://github.com/leanprover/lean4/issues/1678 The built-in visualization options aren't great yet.

[Patrick Massot]

Thanks Wojciech and Sebastian anyway. I should be unstuck now.