Lean4 AST

Stream: lean4

[Bhakti Shah]

is there a way to extract the AST for a particular source file? I think I saw something about lean3 having an AST fork where you could pass --ast as an argument, but does something similar exist for lean4?
apologies if this is documented somewhere, I couldn't really find anything

[Mario Carneiro]

lean 4 has much better out of the box support for AST traversal, so the hack that was done to lean 3 is not really necessary anymore. lean files parse into objects of type Syntax and you can just write that out as JSON if you want

[Bhakti Shah]

Mario Carneiro

lean files parse into objects of type Syntax and you can just write that out as JSON if you want

I see -- so the .ilean file is basically the AST, can't believe it was that simple, I just never thought to look there. Is there any known documentation on the grammar other than the Parser directory in the source code?

[Mario Carneiro]

the grammar is extensible, so no not really, it's context sensitive and defined by the syntax lines that have occurred so far

[Sebastian Ullrich]

The syntax trees are not persisted. .ilean is just a serialization of docs4#Lean.Server.Ilean, no syntax trees there.

[Bhakti Shah]

I see -- my bad, didn't look closely enough

is there a way to extract the syntax object from a program, then? sorry if these are super basic, I'm more of a coq user

[Alex Keizer]

I don't know if there's a more elegant way, but this (mostly) works

import Lean
open Lean.Elab
open Lean.Elab.Command

elab "dbg" cmd:command+ : command => do
    for cmd in cmd do
        dbg_trace "\n{cmd}\n\n"
        elabCommand cmd

It does slightly change the meaning of the commands, since parsing and elaboration are now no longer interspersed, all parsing happens at the start, so this will break if you define and directly use parser extensions in the code you're examining

[Mario Carneiro]

Here's another trick to get the commands, using a linter and a global variable:

Test/SpySyntax.lean:

import Lean
initialize syntaxes : IO.Ref (Array Lean.Syntax) ← IO.mkRef #[]
initialize Lean.addLinter fun stx => syntaxes.modify (·.push stx)

Test.lean:

import Test.SpySyntax
open Lean

set_option pp.rawOnError true
elab "foo" : tactic => do
  for stx in ← syntaxes.get do
    try logInfo m!"{← PrettyPrinter.formatCommand stx}"
    catch _ => pure ()
  syntaxes.set #[]

example : True := by foo

[Mario Carneiro]

The "right" way to do this is to use a custom driver based on runFrontend. That will allow you to get the AST for any file without modifying the target file

[Bhakti Shah]

Thank you! I'll start with these and probably try to work my way up to the "right" way