Zulip Chat Archive

Stream: general

Topic: OMDoc/MMT export of many ITP libraries

Jason Rute (May 25 2020 at 13:34):

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 (May 25 2020 at 13:34):

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 (May 25 2020 at 13:34):

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 (May 25 2020 at 13:34):

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 (May 25 2020 at 13:35):

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 (May 25 2020 at 13:43):

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

Kevin Buzzard (May 25 2020 at 13:44):

Isn't Dedukti something like this?

Patrick Massot (May 25 2020 at 13:44):

Yes, Dedukti is meant to do exactly that.

Reid Barton (May 25 2020 at 13:46):

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

Jason Rute (May 25 2020 at 13:49):

Here is the MMT project website.

Kevin Buzzard (May 25 2020 at 13:52):

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

Jason Rute (May 25 2020 at 13:53):

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

Kevin Buzzard (May 25 2020 at 13:53):

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 (May 25 2020 at 13:54):

I think my operating system does that already

Jason Rute (May 25 2020 at 13:59):

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 (May 25 2020 at 14:00):

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 (May 25 2020 at 14:03):

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 (May 25 2020 at 14:06):

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 (May 25 2020 at 14:07):

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

Jason Rute (May 25 2020 at 14:16):

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 (May 25 2020 at 14:16):


Reid Barton (May 25 2020 at 14:17):

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

Reid Barton (May 25 2020 at 14:17):

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

Reid Barton (May 25 2020 at 14:18):

No position information either.

Gabriel Ebner (May 25 2020 at 14:18):

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 (May 25 2020 at 14:21):

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

Jason Rute (May 25 2020 at 14:22):

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

Sebastian Ullrich (May 25 2020 at 14:24):

Calling Lean a reimplementation of Coq is harsh

Gabriel Ebner (May 25 2020 at 14:28):

they are neither binary nor source compatible with Coq

They say it like it's a bad thing.

Jason Rute (May 25 2020 at 14:50):

@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 (May 25 2020 at 15:08):

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

Last updated: Dec 20 2023 at 11:08 UTC