Making Isabelle Content Accessible in Knowledge Representation Formats

TL;DR

This paper presents a method to export Isabelle proof assistant libraries into the OMDoc format, making them accessible for external tools and enabling applications like dependency management and proof checking.

Contribution

The authors developed an integration of PIDE and MMT to systematically export all Isabelle libraries into OMDoc format, covering over 12,000 theories.

Findings

Successful export of Isabelle libraries into OMDoc/XML

Coverage of full Isabelle distribution and AFP

Enables new applications like dependency management

Abstract

The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult. After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and MMT that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) -- more than 12 thousand theories and locales resulting in over 65GB of OMDoc/XML. Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search.