Zulip Chat Archive

Stream: general

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


Daniel Donnelly (Nov 27 2021 at 17:49):

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 (Nov 27 2021 at 19:40):

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 (Nov 27 2021 at 19:42):

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 (Nov 27 2021 at 19:46):

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 (Nov 27 2021 at 19:50):

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

Patrick Massot (Nov 27 2021 at 20:07):

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

Daniel Donnelly (Nov 27 2021 at 21:05):

Patrick Massot said:

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

Says unicorns have taken over the github servers for now.

Daniel Donnelly (Nov 27 2021 at 21:07):

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 (Nov 27 2021 at 21:07):

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

Daniel Donnelly (Nov 27 2021 at 21:08):

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

Yaël Dillies (Nov 27 2021 at 21:09):

There's some information about the port.

Yaël Dillies (Nov 27 2021 at 21:09):

I don't know much more.

Eric Rodriguez (Nov 27 2021 at 22:10):

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


Last updated: Dec 20 2023 at 11:08 UTC