Does there exist a universal data format for Lean, Coq, etc?

Stream: general

[Daniel Donnelly]

If I wanted to import code into Lean using some data format like OMDoc/MMT (do there exist others?), does Lean 4 support importing of this format? Ideally there would be a format that you can convert to/from any proof assistant language in a faithful way. If there are a total of N proof assistant languages that you wanted to share knowledge between, then a universal data format for doing this gives you O(N) conversion scripts to write instead of O(N^2).

[Arthur Paulino]

At the moment, I don't think so. But just to spice it up, consider that different languages have different expressing powers.

[Yaël Dillies]

I don't think there's even that many, if any, conversion scripts at all at the moment. When it happens, porting is done by hand.

[Yaël Dillies]

Best example of that is that people are spending months to translate from Lean... to Lean. The Lean 4 port is already quite a big thing, so I dare not imagine when it's between properly different languages.

[Yaël Dillies]

However, I assume that an AST is a close first-order approximation of the universal language you're looking for.

[Patrick Massot]

See https://deducteam.github.io/ however

[Daniel Donnelly]

Patrick Massot said:

See https://deducteam.github.io/ however

Says unicorns have taken over the github servers for now.

[Daniel Donnelly]

Yaël Dillies said:

However, I assume that an AST is a close first-order approximation of the universal language you're looking for.

Can you provide a link to the type of AST needed that would be sufficient for encoding faithfully Lean?

[Yaël Dillies]

I'd encourage you to look in stream#lean4.

[Daniel Donnelly]

@Yaël Dillies Okay, I see #lean4 on the left in Zulip. But looks like a lean4 Q&A to me

[Yaël Dillies]

There's some information about the port.

[Yaël Dillies]

I don't know much more.

[Eric Rodriguez]

https://github.com/leanprover-community/mathport may be of interest to you.