Lean 4 export format

Stream: lean4

[Koundinya Vajjha]

There’s a long-stagnant PR to lean4export by @Chris Bailey that introduces some useful enhancements to the Lean 4 export format. Are there any plans to merge this, or are there concerns preventing it?

Having it merged would be good as I’ve completed a parser for the Lean 4 export format—potentially as a step toward an external type checker for Lean 4—based on Chris’ Type Checking in Lean 4, which assumes these additions in its grammar specification.

[Koundinya Vajjha]

The additions are relatively minor, and would be useful to avoid an intermediate "compilation" step between parsing and constructing the environment before the actual type-checking. But presumably there are other options being explored (JSON format?), so I wanted to reach out and ask the Lean devs if there was any such plans. Thanks in advance!

[Mario Carneiro]

I think lean4export is not really being maintained. I think this kind of thing should be maintained as a community tool (i.e. coordinated by all the external kernels that interact with the format), it doesn't require lean core support