OMDoc/MMT export of many ITP libraries

Stream: general

[Jason Rute]

I just came across Experiences from Exporting Major Proof Assistant Libraries by Michael Kohlhase and Florian Rabe. They talk about their experiences translating the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. The paper is a bit long so I've only skimmed it but here are some interesting points.

[Jason Rute]

I think they export the libraries of these provers into a common format called MMT, which can recheck the proofs. For many provers, this is a big undertaking and they outline the steps they took for each prover. While this alone doesn't make these systems interoperable, it is one step closer.

[Jason Rute]

They mention that Lean (and HOL4) are notably lacking. They point out that even though Lean and Coq have similar foundations, what matters for this work is the implementation and they have very different implementations.

[Jason Rute]

They also have some good quotes:

• "Users of theorem provers often approach (and occasionally exasperate) developers with requests to be able to use, e.g., Coq’s tactics together with Isabelle’s sledgehammer tool, requests that sound simple to users but are infeasible for developers."
• "Even a bug as blatant as accidentally generating all theorem files as empty strings (which then trivially recheck) can be surprisingly hard to notice because these exports involve large sets of large files often containing formalizations from domains that neither the prover expert nor the MMT expert understand."

[Jason Rute]

In the final section, they have advice for designers of theorem provers and libraries (emphasis theirs).

• "We have a single clear and important recommendation for developers of theorem provers and libraries: design systems with exports in mind!"
• "Provers should trace user-level content on its way through the elaboration pipeline into the kernel-level syntax." (They however point out this needs to be balanced with performance.)
• "Provers should commit to maintaining a system-near export in some standard data format such as XML or JSON and with a well-documented schema."
• "Provers should allow users to structure formalizations with library integration in mind." (I think they are saying here that in say Coq, one could check that a definition or theorem is actually compatible with HOL. I don't think I understand the details.)

[Jason Rute]

This also sounds similar in spirit to @Mario Carneiro's MMO project, but maybe I am mistaken.

[Kevin Buzzard]

Isn't Dedukti something like this?

[Patrick Massot]

Yes, Dedukti is meant to do exactly that.

[Reid Barton]

This talk from Thursday is probably relevant too (unfortunately I missed it and haven't watched it yet).

[Jason Rute]

Here is the MMT project website.

[Kevin Buzzard]

Isn't this insanity? How does MMT know that Lean's Banach spaces are the same as Isabelle's?

[Jason Rute]

They don't. They make it very clear that library alignment is a separate and hard problem.

[Kevin Buzzard]

So their goal is to make one system which contains the disjoint union of all the theorems in the other provers? With an emphasis on disjoint?

[Kevin Buzzard]

I think my operating system does that already

[Jason Rute]

I think the ultimate goal is alignment and interoperability (and they have written some papers on those topics), but I think they view this as a first step. I don't know if their format is the correct one, but I imagine if Lean only lives in Lean and Isabelle only lives in Isabelle, then there is no hope at interoperability. One needs an interchange format (that is better than Lean source code or .olean files).

[Reid Barton]

It seems they mention Lean's export format once in passing. I wonder whether they did not include it as an example because it is already basically solved, or because there is something making the export format not usable.

[Jason Rute]

I could also imagine that they don't have Lean, because they approached the Lean developers and they replied "wait until we've built Lean 4".

[Gabriel Ebner]

One of the coauthors of the paper sent me an email some time ago because they wanted to parse and type-check the Lean export format using my trepplein tool. They were interested in it because both trepplein and MMT are written in Scala.

[Gabriel Ebner]

But apparently they didn't use it after all..

[Jason Rute]

Just for my own information, where can I find more on Lean's export format? Is this what is in .olean files? Is it also the information accessible in the "environment" in Lean?

[Reid Barton]

https://github.com/leanprover-community/lean/blob/master/doc/export_format.md

[Reid Barton]

I don't think it contains all of that information (e.g., notation is absent I think), just the important stuff.

[Reid Barton]

Probably attributes are absent too. Important = important for an external type checker to verify the proofs.

[Reid Barton]

No position information either.

[Gabriel Ebner]

Regarding elaboration, Isabelle is special among proof assistants in that it a very complex processing pipeline from heterogeneous user-level declarations to homogeneous kernel-level declarations.

I must be missing something. Isabelle's term-level syntax is extremely close to the kernel syntax, no hidden implicit arguments, etc. Data types are elaborated similar to HOL. And Isar is just as close to the kernel proofs as ssreflect tactics are to Coq proof terms.

[Jason Rute]

If it helps, here is a separate paper just on the Isabelle export: https://arxiv.org/pdf/2005.08884.pdf

[Jason Rute]

I don't know enough about Isabelle to comment more.

[Sebastian Ullrich]

Calling Lean a reimplementation of Coq is harsh

[Gabriel Ebner]

they are neither binary nor source compatible with Coq

They say it like it's a bad thing.

[Jason Rute]

@Reid Barton I don't think from their point of view the Lean export format is really a solution. They seem to be interested in keeping user-level information, such as the tactics used in the proofs. I'm less sure I understand the motivation of their project, so I can't comment on why they want that information. However, I can comment on my own machine learning purposes. Proof recording at the tactic level is really important for building systems like TacticToe. For my own purposes, I've found ways to hack the Lean tactic library to record the information I need. I would be great if theorem provers made it easy to do this without hacks.

[Jason Rute]

And I think Lean 4 might have some cool features in that regard which I look forward to seeing!