Exporting ASTs in Lean 4

Stream: lean4

[Kaiyu Yang]

Hi,

Is it possible for Lean 4 to export ASTs similar to lean --ast --tsast --tspp in Lean 3? I'm building a tool for analyzing Lean 4 code, and having access to ASTs and tactic states would make things much easier.

If this feature is not readily available, what would be a potential avenue to implement it in Lean 4? Thank you so much!

[Mario Carneiro]

in lean 4 it is easiest to just use the metaprogramming framework to get Syntax objects for each command and do whatever with them

[Mario Carneiro]

The tactic states are available in the info tree after processing the command

[Kaiyu Yang]

Hi Mario,

I'm pretty new to Lean 4 and not familiar with Syntax or info trees. But they're really valuable pointers for me to take a deeper look! Please let me know if you're aware of any documentation or existing code samples using them. Thank you!

[Thomas Murrills]

You can learn a lot about Syntax through the metaprogramming book available here :)

[Kaiyu Yang]

Thank you, Thomas!

[Max Nowak 🐉]

Yeah. Even the VSCode Lean4 plugin does the heavy lifting inside the Lean4 compiler directly, so it has access to all the fancy features.

[Patrick Massot]

Another entry point is the source code of LeanInk.

[Patrick Massot]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Access.20to.20the.20proof.20goal/near/323185812.

[Kaiyu Yang]

@Max Nowak 🐺 @Patrick Massot This is very helpful. Thanks!