general JSON to lean4 support

Stream: mathlib4

[Bhakti Shah]

Hello! Very new to this zulip so apologies if I am posting this in the wrong stream.
I'm working on something where the goal is to compile to lean4 -- I've been looking at this chat, and just the mathport source in general -- if I'm not wrong it takes in a lean3 AST in JSON format and compiles that into lean4 code, which is something I think I could repurpose to my needs (though I might be wrong -- I haven't experimented yet). I was wondering if it's possible to get some more details about the same -- namely, can I generalize the code to take in a different AST if it is given the grammar for the same, and if yes, what the restrictions on the alternate grammar would be. I can provide more information if needed.

Thank you!

[Eric Wieser]

(deleted)

[Jannis Limperg]

Could you say a bit more about your use case? Perhaps the best option would be to write your compiler as a Lean 4 program. Then you'd have immediate access to the Lean 4 AST (and the concrete syntax tree) as well as the whole Lean 4 compiler.

[Bhakti Shah]

Jannis Limperg

Could you say a bit more about your use case?

Sure -- I'm trying to write a compiler from Coq to Lean, and the Coq AST is in the form of an s-expression (which i can easily convert to json / similar formats). I did just find out that the .ilean files contain just the AST object (not a big lean4 user and never thought it would be that simple to get the AST) -- so I might have a more direct way of going about this after all.

[Jannis Limperg]

In that case, I would indeed advise that you write the compiler in Lean 4. The concrete syntax tree is docs4#Lean.Syntax and you can use quotations to construct Syntax objects, e.g. `(Nat.succ (Nat.add $x $y)). You can then render these Syntax objects using Lean's own pretty-printer.

Alternatively, you could work with the Lean AST, which is mostly defined by the docs4#Lean.Expr and docs4#Lean.Declaration types. If you want to render declarations, you might need to write some pretty-printing code yourself.

Is your goal to get human-readable output or merely something that the Lean kernel can typecheck? And are you aware of the existing prototype which one of the Coq devs wrote at some point? (I'd have to look for the link again.)

[Bhakti Shah]

Jannis Limperg I see -- thank you for the links! I'll definitely look into it.

I haven't come across any existing prototype -- do you have more info on that? I specifically checked if something already existed, but all I could find was like informal translations between tactics, and a Lean import for coq

[Jannis Limperg]

Ah yes, this is what I had in mind and it is indeed in the wrong direction.