Getting ASTs of Lean file

Stream: lean4

[Jaeboum Kim]

Hi! How can I get Abstract Syntax Trees of Lean file?
I saw the following command of Lean 3. However, it does not work in Lean 4.
"lean --make --ast computability/ackermann.lean"

[Henrik Böving]

The process is quite a lot more involved than that, why are you looking into getting the Lean AST?

[Jaeboum Kim]

I would like to get structural embedding via Lean AST. ( ex. Lean AST -> graph -> graph embedding) Are there any better ways?

[Henrik Böving]

Okay so you are interested in doing AI things yes? We usually point people interested in interacting with lean through AI here: https://github.com/leanprover-community/repl

[Jaeboum Kim]

Thanks for your kind and quick reply! Would it be a good idea to leave a question in that repo? or parse info from the output of repl?

[Henrik Böving]

You can ask there if you want, the authors are also here on the Zulip, most notably @Scott Morrison (they are probably asleep right now but will be around in a few hours)

[Kim Morrison]

We don't really have a great pure text representation of Lean.Syntax. You should look at that type, and then if you can tell us something about how you would like it represented probably we can give some pointers.