Experiences from Exporting Major Proof Assistant Libraries

We use OMDoc [35] as the standard XML format for holding the library exports. Its semantics and API are provided by the Mmt system [55, 56]. Mmt also provides implementations of logical frameworks such as LF [21] and extensions (collectively named LFX; see [43]) we have developed for representing theorem prover logics adequately. With that, the general pattern for exporting the library \(\mathcal {L}\) of a theorem prover \(\mathcal {T}\) is as follows: The resulting collection of libraries is shown in Fig. 1. Here, the third level from the top shows the theorem prover language and the bottom level the libraries of the corresponding provers. For example, the NASA library, the Mizar Mathematical Library, and the Archive of Formal Proofs are the major libraries of PVS, Mizar, and Isabelle. The second level shows the logical framework in which we represented the prover language: mostly LF [21] or extensions thereof (LFX); because the Isabelle system is a logical framework itself, it occurs at this level. All of these framework are realized within Mmt.

Crucially, this enables a separation of skill sets: The first step can be best executed by an expert on the logic of \(\mathcal {T}\) (and LF/LFX), and the second step by an expert for system \(\mathcal {T}\), often a core developer. The latter is required as no system is documented well enough to make an export feasible without an expert on the inside. The system-near export can be implemented as a stand-alone component of the system, e.g., as a traverser for the internal data structures; or it may be a major part of the system, maybe developed over years or requiring changes all across the codebase. In the latter case, we were often not even able to precisely quantify the effort in terms of developer time or lines of code.

The third step can be best executed by an Mmt expert given a direct line of communication to the \(\mathcal {T}\) expert about the meaning and details of \(\mathcal {L}'\). A good practice is for the two of them to jointly write or document the schema for the system-near export. A two-week research visit proved to be the minimal investment necessary to synchronize this part and to specify (not implement) the export. The implementation usually consists of a straightforward parser of the system-near export followed by a traversal to translate it. This part is usually implemented as a self-contained add-on to Mmt of relatively small size—usually a few thousand lines of code depending on how many productions the grammar for the internal data structures has. An exception was HOL Light, where the data structures were so simple that we included the second part in the prover instrumentation.

The separation above allows maintaining the generation of \(\mathcal {L}'\) together with the \(\mathcal {T}\) release process and that of \(\mathcal {L}^*\) with the Mmt release process. This has proved to be the best recipe against the bit-rot of exporters, which is one of the biggest problems in practice.

Even so, the involved tasks are badly incentivized: they are very difficult, very work-intensive, and tend to produce brittle implementations that generate only one paper. This is an open problem with academic system development in general and prover library exports in particular—our exports were only possible due to well-orchestrated collaborations that drove the creation and documentation of the system-near export. For example, a big part of our PVS export was working with the developers to document and debug the generation of XML files. In the case of Coq, Claudio Sacerdoti Coen’s kernel export plugin [59] was developed specifically for the occasion, the Isabelle export was enabled by heavy investments by Makarius Wenzel into the PIDE infrastructure. Both of these efforts required months of full-time work.

Rarely used or experimental language features pose a related problem. Often the prover expert notices missing cases in her export only when the feature is actually used in a library, which may be very far down the line. For example, in our Coq export, we encountered kernel features that were not used at all in any of the libraries that we could build with the latest Coq version. We noticed that issue because we actually looked for uses of the feature in order to reverse-engineer the intended semantics from the way it was used.

To ensure the correctness of exporters, we found the skill-separating export approach above extremely valuable. It allows for the system-near export to be relatively trustworthy as it is a straightforward serialization of the kernel data structures, and it pushes all logical transformations (e.g., eliminating subtyping) to a later phase. Mixing the serialization of the data structures with such logical transformations is not only undesirable (because information is lost) but has also proved error-prone because the former is a major implementation effort and the latter extremely difficulty theoretically.

Even so, we found that any logical transformation in later phases must remain simple and compositional: any non-compositional transformation is usually a huge theoretical challenge, ends up incomplete or hacky because the theory did not cover all cases that are actually used in the prover, and is the first thing to break upon new prover releases.

There are multiple general approaches to setting up the export of libraries. The most direct approach of exporting from the source files basically never works in practice because it would essentially require reimplementing the entire prover. Instead, only exports that use the kernel data structures are feasible. Instrumenting the kernel means that the library is checked by the kernel, and kernel hooks are used to generate the export. It requires rechecking the entire library. (If proof exports are not needed, it may be possible to tweak the kernel to skip all proofs, which is the most expensive part.) But if the kernel is small and well-structured, instrumentation is relatively easy to implement and maintain. Traversing the kernel data structures means that we first check a unit of source code (e.g., file) and then traverse its internal representation to generate the export. The code for this can be inserted as a plugin or by modifying the system sources.

If the kernel-generated files are not used internally but are only written out for export purposes (as for PVS), it is easier to negotiate changes to their format (e.g., to include additional information). But there is little assurance that they were generated correctly in the first place. In that case, an initial debug cycle may be necessary until the files are generated correctly. But that is still much easier than building an instrumentation from scratch.

A subtle practical issue we encountered with kernel-generated files in multiple situations (e.g., PVS/NASA) is a reliance on case-sensitive file systems. Because logical names declared inside source files are usually case-sensitive, care is needed when generating a separate file for every such declaration: developers must encode the names to make the generated file names unique without relying on case. Otherwise, exports may be entirely unusable on some systems, e.g., when cloning a git repository on a case-insensitive file system, the second file overrides the first; then git detects a change, and every subsequent pull fails.

The main drawback of kernel-based exports is that the user-level data structures in the source can be very different from the kernel-level data structures that make up the export. Most systems employ complex processing chains that translate the user-level into kernel-level data structures. Proof assistants support a varied and growing set of transformations including disambiguation, type inference, proof completion, normalization, and feature elimination, and we group all of them together under the term elaboration.

Disambiguation includes user-level unqualified or partially qualified identifiers that have to be resolved into kernel-level qualified ones, as well as user-level notations that have to be parsed into kernel-level abstract syntax trees. Both cases may be ambiguous and systems usually employ idiosyncratic resolution mechanisms. If the identifiers have the flavor of selectors, disambiguation can be intertwined with type inference: the type or type class of an object o may be used to disambiguate a selector applied to o, or the resolution of the selector may be used to infer the type of o.

Typical examples for normalization are definition expansion, \(\beta \)-reduction, and computation of inductive functions. Normalization is always needed as an ephemeral operation during verification. But depending on the system, some normalization steps are permanent in the sense that the kernel-level language only represents the normalized terms. An extreme example is Mizar’s permanent normalization of implication into a disjunction.

Almost all elaboration steps are not injective, and the information of what the user originally wrote is often lost along the way. Thus, a lot of high-level structure is elaborated away on its way to the kernel. But that structure would be extremely valuable for virtually any application other than proof-checking, and it is extremely difficult or even impossible to recover this information in an export. For example, most systems provide some support for common high-level features such as mathematical structures (modules, records, etc.) and term languages (inductive, co-inductive types), and when translating between systems or integrating libraries, it is highly desirable to match these up with each other. But in the common situation where different systems eliminate these features in different ways, this is not possible. Exports that preserve this user-level structure remain an open problem for all systems. For example, we only had the resources to preserve Coq sections and Isabelle locales but none of the many other high-level constructs.

Advanced user-level declarations such as inductive types or recursive functions definitions are typically justified by meta-theorems that establish their conservativity. The meta-proof may be used explicitly in the system by elaborating user-level declarations (as in Isabelle) or be left to the literature about the system (as when adding inductive types to the calculus of constructions in Coq). Both can be problematic: The former can lead to more numerous and less intuitive declarations in the kernel, which can cause a strong disconnect between user and kernel-level declarations. The latter may cause very subtle issues (in fact so subtle that discussions usually stay limited to small circles of experts) when the meta-theorems do not perfectly match the implementation, e.g., if the conservativity of two features is proved individually relative to the base calculus without noticing that their combination in the implementation may violate conservativity.

The representation of these user-level features in logical frameworks is much harder and less well studied than the representations of kernel-level languages. That is partially because kernel-level syntax is often defined using the highly standardized methods of context-free grammars and context-sensitive type and proof systems, which yields a strong relation between specification and implementation. The elaboration of user-level syntax, however, often uses relatively unconstrained programs in Turing-complete programming languages. To catch and mimic this practice, Mmt provides two mechanisms for representing elaboration-based features. Declaration patterns [23, 25] are used for statements whose elaboration can be defined declaratively by simple rules. We use it to define HOL type definitions and the various definition principles of Mizar. Secondly and more generally, arbitrary elaboration can be defined in the Scala language underlying Mmt. We use this to define a few advanced features such as PVS includes and Coq sections, and we could also use it to capture Isabelle’s heavily used corresponding mechanism for arbitrary elaboration. We recently described details and collected more examples in [45].

The conflict between user-level and kernel-level is particularly critical for the export of proofs. It is still unclear what the best way to export proofs is.

The export of kernel-level proofs is often straightforward, but the proof objects become huge. This is particularly severe when proofs include automatically found parts, which may be much larger than necessary. For example, our Coq export runs out of memory on some very large proofs in the Feit–Thompson proof [19]. This might be because an unnecessarily large proof term is built internally. But a detailed investigation has so far been impossible because it would require precious system export resources. Moreover, kernel-level proofs have only limited value, independent proof checking essentially being their only use.

A third option is to export dependency-only proofs, where an Mmt expression \( dependsOn (d_1,\ldots ,d_n)\) is used as the proof that records only the dependencies that were used. This is sufficient for some applications such as change management and premise selection as done in [32]. In the simplest case, each \(d_i\) is an axiom or theorem identifier, but it can be any expression of the prover’s logic, e.g., the application of a polymorphic theorem to the type arguments with which it was used in the proof. Thus, the same type system that is used for the logical data can be used for logical fragments inside extra-logical data.

In any case, kernel-level proofs may still have logical gaps making them insufficient even for proof checking, e.g., if automated proving or decision procedures are part of the kernel (as for Mizar and PVS). They may also have pragmatic gaps if the logic includes powerful computation (as for Coq) as opposed to logics that record computations in explicit rewrite steps (as for Isabelle). Depending on the application, these gaps may be seen as advantages (skipping low-level steps that can be more easily recreated after translating the proof to another system) or disadvantages (precluding the rechecking of the proofs).

In general, a major lesson of our exports is that the community has not yet converged on a good solution for exporting mid-level proofs that combines the relevant structure of user-level proofs with the inferred information and re-checkability of kernel-level proofs. In particular, it would be great if applications processing proofs could gradually choose the level at which a subproof is seen. For example, a proof translation tool should try to map every high-level proof rule to the target’s counterpart whenever such a counterpart exists.

Therefore, all of our exports have de-emphasized proof export and usually opted for dependency-only exports. We only experimented with a few kernel-level proofs for Coq to test the scalability of the approach.

Most proof assistants use what we call the homogeneous method, which fixes one foundational logic and builds on it using conservative extensions such as definitions and theorems. Thus, all domain knowledge is ultimately represented in terms of the same primitive concepts. We speak of the heterogeneous method if systems define theories that encapsulate choices of primitive concepts or notions and then considers truth relative to a theory. The homogeneous method can be seen as the special case where a single theory is fixed, e.g., the underlying set theory of Mizar or the theory of an infinite type in HOL Light.

The heterogeneous method allows capturing the mathematical maxim of stating every result in the weakest possible theory and moving results between theories in a truth-preserving way. (The formal tool to capture this moving operation is theory morphisms.) This is often called the little theories approach [15] as pioneered by IMPS and supported by Isabelle and PVS. Even if heterogeneous reasoning is possible, it may be optional, e.g., users of Coq and Isabelle often do not make use of heterogeneity even when they could. PVS and IMPS, on the other hand, force users to state results inside theories, and IMPS strongly encourages the use of theory morphisms.

Almost all systems support the heterogeneous method in some way because it is needed at least to capture mathematical structures, such as groups or topological spaces, which are naturally represented as theories (i.e., sets of operations and axioms). In this context, a critical distinction is whether the heterogeneity is external or internal (which we discussed in [44]).

We speak of internal heterogeneity if the base logic allows expressing a theory as a type (or a similar construct) in a way that allows arbitrary quantification over all models of the theory. Internal heterogeneity is usually realized via record types such as in PVS and Coq. Mizar structures behave similarly. But internal heterogeneity is not always an option. For example, even higher-order logic with record types can only express theories without axioms as record types; dependent type theory does not have that limitation because axioms can expressed as usual record fields.

We speak of external heterogeneity if it is a language feature that sits on top of the base logic and provides a way to specify theories. It can be added relatively easily to virtually every base logic (whereas adding internal heterogeneity may be impossible or difficult) and is present in most systems: Coq modules, OCaml modules for HOL Light, IMPS theories, Isabelle theories, locales, and type classes, and PVS theories. Usually, a limited form of binding variables typed by a theory is still possible, e.g., via functors in Coq and HOL Light, parametric theories in PVS, or type class ascriptions in Isabelle.

The distinction is important for library integration. Internal heterogeneity tends to be more flexible and more expressive, especially in large projects involving mathematical structures. A good experiment here is the Coq library where both internal and external features are well supported and in competition with each other: We see that the external module system is falling out of use somewhat and the internal record types are becoming the predominant source of heterogeneity, most prominently in the Mathematical Components project [17]).

Therefore, from the perspective of library integration, it is critical to use preserve external heterogeneity in the exports. We were able to do that directly for PVS and IMPS. For Isabelle, heterogeneity only exists at the user-level, and elaboration reduces it to a homogeneous kernel-level formalization. But we were able to reconstruct the user-level locale structure and export it in addition. We also preserved it for Coq, but this has limited practical value as Coq modules are not widely used throughout the libraries.

Most provers allow more language at the top level than the logic they are based on.

Processing instructions are extra-logical declarations that control the system behavior down the line. This may even involve side-effectful instructions, whose semantics depends on the prover’s linear processing of the source files. The most important application is to guide otherwise inefficient search algorithms. For example, a source file might contain a line that switches on a search heuristic that is then used in subsequent declarations. These instructions may depend on not widely known implementation details, be under-documented, or even be open to user extension. Examples for the latter are users writing a Coq plugin or inlining ML code in Isabelle files.

A common application is to complement undirected proof search with dedicated algorithms for specific subproblems. For example, equational theorems in Horn form can be used for rewriting as an optimized simplification procedure. But only some of those theorems may be used at the same time to ensure termination, and systems like Isabelle and PVS a set of theorems that are to be used automatically for rewriting. Users can then flexibly add or remove theorems to it. A related example is type-checking in softly typed systems, where type-checking is reduced to proof search. Mizar allows registrations, which are special theorems about typing that are to be used for automated type checking. Similarly, unification hints such as Coq’s canonical structures guide the type inference algorithm when having to choose a record if only some it its field are known.

Implicit toplevel binding are free or specially bound variables that are treated as if they were universally quantified at the beginning of the containing statement. Characteristically, the respective logic does not feature the corresponding universal quantifier so that these variables can never be bound in subexpressions, and their implicit binding at the toplevel of a statement is the only way to introduce such variables at all. Examples are type variables in HOL, type and subtype variables in PVS, and function and predicate variables in Mizar. Internally, universes in Coq behave accordingly although no user-level syntax is provided.

Technically, allowing such toplevel binding changes the logic. However, as a general rule, this is conservative over the base logic: toplevel binding can be eliminated in favor of all (i.e., usually infinitely many) ground substitution instances. This is well known from axiom schemas in axiomatic set theory: in order to stay within first-order logic, authors often state a single second-order axiom as a set of infinitely many first-order substitution instances of a schema. Interestingly, when defining the logics in an LF-like logical framework, the formalization of these toplevel binders requires no additional work: they are directly represented using the \(\varPi \)-binder of LF. This can be seen as a rigorous argument for why these binders are in fact conservative.

While this is a relatively minor theoretical observation, we mention it here explicitly because it is not widely known in all its generality. Therefore, the details in individual provers are not always cleanly documented or implemented, and their treatment can occasionally be confusing when writing exports.

There are a number semantically irrelevant language features that are often critical to export as well. In some cases, it is even strongly advisable to prioritize them higher than some logical features.

By far the most important non-logical aspect of an export is attaching source references. These annotate each element in the export with the corresponding physical location (if any) in the source (i.e., file, line, column). Even though some form of source references is needed anyway for provers to report useful error messages, it is not always easy to preserve them in the export, depending on how they are processed and stored internally. This can be especially difficult if elaboration substantially changes the syntax tree. But source references are crucial to enable many applications of the exports because they allow pointing users to the human-readable sources whenever they interact with a part of the export, especially in the typical case where the kernel-level data structures in the export may look entirely unfamiliar to the user. A typical example is search, where one wants to search through the export but show results in the source. Source references should ideally be present everywhere, i.e., for each subexpression, but are at least needed for every statement (definition, theorem etc.). In the worst case, source references for statements can be recoverable by parsing the source in a separate process.

Finally, semantic web-style ontological abstractions have proved very successful in many areas such as biology and medicine. The analogues for proof assistant libraries systematically abstract away all symbolic expressions (types, formulas, proofs, etc.) and only retain identifiers (of modules, statements, etc.) and properties and relations on them such as authorship, dependency, or check time. While these do not capture the entire semantics of the library, they are extremely powerful for limited problems: Their level of abstraction is sufficient for shallow services such as semantic navigation, search, or querying. Even better, at this level, the huge formal differences between the libraries disappear and services can easily span multiple libraries, e.g., to find related formalizations in different libraries. Moreover, standardized formalisms such as RDF [58] and SPARQL [64] and highly scalable tools are readily available. While such applications were already envisioned years ago, e.g., in [3, 5], they could so far not be realized at large scales because provers were unable to export the necessary data. Therefore, we have recently carried out two major case studies in supplementing the exports described so far with exports of ontological abstractions: in [11], we define an upper library ontology and use it to export linked data representations for the Isabelle (40M RDF triples) and Coq (12M RDF triples) libraries. This enables, for example, querying for all Isabelle or Coq theorems about a given mathematical concept. Corresponding extensions of the other exports are straightforward conceptually; they still require a considerable investment in collaboration with the system expert but are significantly easier than full logical exports.

Due to the tremendous logistical challenges in maintaining large libraries with many authors over decades, multiple models for the structure of libraries have been developed. Typically each system is integrated with a standard library that is co-released with the system, often maintained in the same repository as the system’s source code. This library can be comprehensive or small and be extended by any number of external distributed libraries—HOL Light with its integrated library mostly curated by the main developer and Coq with many distributed libraries developed by users can be seen as opposite extremes on this spectrum.

For external libraries, a critical question is whether these are co-maintained with the system, usually as part of the regression test suite that is checked before every system release. In that case, the library can be a collection of independent user-submissions or a single curated coherent body—Isabelle/AFP with many relatively unrelated submissions and the Mizar library carefully curated by a small committee are opposite extremes on this spectrum. Both are officially co-maintained with the system. PVS/NASA is special in that it is a single external library that is developed independently from the prover; in practice, it is used as the main regression suite for the system.

Table 1 gives an overview over the general aspects of the six exports we will discuss below.

Overview and Formalization Coq is based on the calculus of inductive constructions (CIC), which can be roughly seen as dependent type theory plus universe hierarchy plus (co)inductive types. The exact status of propositions is subtle, but essentially every proposition is a type. Generally, the most desirable representation in a logical framework is a Church-style typed one: it uses \(\texttt {tp}: \texttt {type}\) to represent every Coq-type A as an LF-term \(\ulcorner A\urcorner :\texttt {tp}\), and \(\texttt {tm}: \texttt {tp}\rightarrow \texttt {type}\) to represent every Coq-term t : A as an LF-term \(\ulcorner t\urcorner :\texttt {tm}\,\ulcorner A\urcorner \). This has the advantage that only well-typed terms can be encoded at all, and Coq’s typing rules are captured by the LF type system.

But this representation requires more type annotations than typically present. For example, if \(A\Rightarrow B\) encodes simple functions, the application operator is represented as \(\texttt {apply}: \varPi _{A,B:\texttt {tp}}\texttt {tm}(A\Rightarrow B) \rightarrow \texttt {tm}\,A\rightarrow \texttt {tm}\,B\). Thus, a Coq application is represented as an LF term that records its input type A and output type B. (Actually, Coq uses a dependent function space, but the same argument applies). In most cases, this additional information is advantageous and is already present in the kernel data structures or can be inferred relatively easily, by calling either Coq functions during the export or logical framework functions in Mmt. But it significantly increases the size of the export. This size explosion problem can be alleviated partially by using rewriting as in [9]. This allows annotating only \(\varPi \)-expressions with types but not applications. These approaches to size issues so far do not differentiate between terms, types, and proofs, and that might help in the future.

In the case of Coq, we exported low-level proof terms, and a typed representation would not have been feasible yet. We used an untyped Curry-style representation based on a single type \(\texttt {expr}:\texttt {type}\) of all Coq terms and types, and a separate typing judgment \(\texttt {of}:\texttt {expr}\rightarrow \texttt {expr}\rightarrow \texttt {type}\) of typing derivations. Now the application operator is simply formalized as \(\texttt {apply}:\texttt {expr}\rightarrow \texttt {expr}\rightarrow \texttt {expr}\) together with appropriate typing rules. However, our export does not preserve Coq’s internal structure sharing because it is unclear how to its purely syntactic sharing (where, e.g., even different variables of the same name are shared). This is presumably why even this untyped encoding ran out-of-memory on some of the largest proofs in the Feit–Thompson proof [19].

The untyped encoding also loses the types of Coq-identifiers c : A, which simply become \(c:\texttt {expr}\) in LF. To remedy this, one can represent c : A using two declarations \(c:\texttt {expr},\,c\_type:\texttt {of}\,c\,\ulcorner A\urcorner \). To avoid making the encoding non-compositional in this way, we used Mmt ’s ability to flexibly extend the logical framework: We switched to LF with predicate subtypes, and defined \(\texttt {tm}\,A\) as the subtype of \(\texttt {expr}\) containing only those \(e:\texttt {expr}\) that satisfy \(\texttt {of}\,e\,A\). This allows compositionally representing c : A as \(c:\texttt {tm}\,\ulcorner A\urcorner \) as in Church-style encodings.

Universes Coq’s universe hierarchy makes the Church representation even more complex because a second parameter is needed: \(\texttt {univ}:\texttt {type},\;\texttt {tp}:\texttt {univ}\rightarrow \texttt {type},\;\texttt {tm}:\varPi _{U:\texttt {univ}}.\texttt {tp}\,U\rightarrow \texttt {type}\). The application operator now takes four additional arguments instead of two as in \(\texttt {apply}: \varPi _{U,V:\texttt {univ},A:\texttt {tp}\,U,\varPi B:\texttt {tp}\;V}\texttt {tm}\, M\,(A\Rightarrow B) \rightarrow \texttt {tm}\,U\,A\rightarrow \texttt {tm}\,N\,B\). Moreover, additional formalization steps are needed to compute the universes M and N from U and V according to the Coq typing rules. Finally, as Coq’s universe hierarchy is cumulative, the Church representation breaks down entirely as injection functions have to be inserted non-compositionally all over the place to cast types into higher universes. This is an additional reason why only a Curry representation is feasible at this point.

Coq source syntax only contains the identifier \(\texttt {TYPE}\) without clarifying its universe, and the system internally introduces a fresh universe identifier for which it then infers constraints. Because these constraints are affected by how an identifier is declared and how it is used, this information must be maintained globally. If an identifier is used in multiple different source files or even libraries, the resulting constraints may be inconsistent with each other. Technically, a Coq export must include these universe constraints and treat them as assumptions relative to which the theorems are stated. This is what we did. But as this information is usually not interesting to the user and not portable to other provers, it remains an open question how to handle these constraints at all.

Inductive Types The description above is only accurate if we ignore Coq’s (co)inductive types. These are very complex, e.g., using multiple kinds of parameters and offering primitive operators for recursion and pattern-matching. Capturing the associated typing rules in a declarative logical framework has so far been out of reach, be it Church or Curry-style. And eliminating them is (even if we are willing to lose this high-level feature) is a prime example of a theoretically possible but practically doomed non-compositional logical transformation. Therefore, our representation had to go outside LF by using untyped Mmt symbols to represent recursion and pattern-matching. Since our representation was untyped anyway, this allowed exporting all Coq expressions regarding (co)inductive terms without significant additional loss. A representation in a stricter framework like LF or Dedukti (\(\hat{=}\) LF modulo) would be very difficult.

The Coq system has grown for several decades, and its internal workings are extremely complex. More recent reimplementations of essentially the same language like Matita [4] or Lean [14] have been able to simplify the implementation drastically. But because they are neither binary nor source compatible with Coq (Matita could read Coq binaries at one point but then diverged), they cannot process the huge Coq libraries.

Recently, Coq development has increasingly focused on giving users more control how their input is interpreted before it reaches the kernel. Type classes and canonical structures/unification hints are the most important examples. These are not visible to the kernel and therefore not part of exports like ours.

Similarly, all Coq proof objects are low-level \(\lambda \)-terms, and high-level structure via tactic languages is elaborated away. This makes Coq exports very big if they include proofs. Because computation (in particular, recursive functions on inductive types) is a kernel feature and thus not part of the proof terms at all, some complex proof steps do not have an effect on proof size. Therefore, it was feasible to export all proof terms.

The Coq module system is primitive and fully visible in the kernel. That allows fully preserving the modular structure. However, the trend in Coq development is toward using record types (which are treated as inductive types with one constructor) instead of modules. While visible to the kernel, this modular structure is very hard to recover. Therefore, there is no export yet that can identify this modular structure.

Maybe surprisingly, the Coq system includes several imperative aspects. For example, a section is checked as usual, but when closing a section the internal state of Coq holding the local context of the section is rolled-back and the section is installed in the way in which it is visible from the outside. Thus, the local context of the section no longer exists at all, which makes it impossible to export sections via the kernel-generated binary files and difficult to export via kernel instrumentation. We opted for the latter.

Coq has reached the usage size, where the central maintenance of libraries is no longer feasible. Instead, the Coq library has been factored into hundreds of repositories with a somewhat standardized build process. This allows distributed maintenance of the library. But it also means that not every repository always builds with the latest version of Coq. For example, when we ran our export in early 2019, only around 70 of around 250 repositories could be built, including the MathComp libraries (the situation has improved since then).

We used the XML files produced by kernel-instrumentation in [59] for our export [46]. Due to the distribution of libraries, significant additional scripting was needed to detect all libraries, identify their metadata and dependencies, and iterate through them. The metadata does not include which toplevel Coq namespace(s) a library’s declarations are in so that additional checks were needed to determine which declarations to export.

Alternative exports are presented in [6, 9] using Church representations in Dedukti after eliminating (co)inductive types and in [13] to first-order logic for the purpose of premise selection, but none covers the entire language.

The biggest future challenge for Coq is to scale up the export. Our export is deceptively scalable—to the point of including all proof terms—because it uses an untyped representation in the logical framework. Switching the export code to work relative to a typed representation would be straightforward but would yield much bigger exports. The usefulness of the untyped representations is limited because any kind of type inference of re-verification must implement the Coq type system from scratch. The rewriting-based representations in Dedukti may alleviate this problem. But we expect that only a systematic solution to proof export as indicated in Sect. 2.5 will eventually be successful.

This will require two investments: Firstly, Coq must process its proofs in a way that allows recovering mid-level proof terms—terms that includes more information than the users tactic script (e.g., all intermediate proof states and tactic invocations) but less than the low-level \(\lambda \)-terms. Secondly, proofs that are the result of search and other computations must be refactored to ensure they are not massively larger than necessary. That would also help cause of program extraction—it is plausible that some programmatically found current Coq proofs are so convoluted that they would not allow for extracting elegant programs. As a simple immediate step, it may help for Coq to display the internal size and possibly structure of every proof. That would allow users to notice when proofs are much bigger than expected.

A major Coq-specific logistical challenge is given by the distributed library. While necessary due to the size of the user community, it brings a host of new maintenance problems such as different libraries depending on different versions of Coq. It is likely that this problem will not go away as new versions of Coq will be released faster than all existing content will be adapted. Therefore, new tools will be needed to manage the symptoms. However, this is a general issue facing the Coq community, and we expect good package and build managers to emerge in the near future, which can then be integrated with exports. That will make the scripts obsolete that we used to run our export over all libraries and will ensure the maximal number of libraries can be exported.

Finally, while large-scale library integration and system interoperability is mostly a problem of the future, we can already foresee that the predominant use of record types for heterogeneity will cause problems. A good compromise might be to annotate those record types that are meant to be used in the sense of mathematical theories so that exports can translate those records differently. This might require limiting the use of such records: for example, record types cannot be mapped to Isabelle locales if they occur as the types of non-toplevel bound variables.

We formalized the HOL Light logic in LF using the analogue of the Church encoding sketched in the section on Coq. Because this was the first export we did, we refrained from exporting proof terms at all so that the Church encoding did not present a scalability hazard. Instead, we exported dependency-only proofs.

HOL Light is implemented inside the OCaml toplevel with only a few tweaks for parsing expressions. This makes the kernel very easy to instrument for generating an export. However, it makes it near impossible to export any of the high-level features used to build the library as these are arbitrary OCaml programs on top of the kernel. For example, the kernel is not even aware of the list of theorems, which are instead maintained by the OCaml context. Any high-level or tactic-based proofs are invisible to the kernel and only low-level exports scale to the whole library. This is particularly unfortunate in the case of HOL Light because the source level proofs are just highly concise tactic invocations and thus can be very hard to read. To remedy this problem, [49] patches individual tactics in order to export tactic applications in addition to kernel-level.

Because the source files can contain arbitrary OCaml code, recovering source references is difficult in principle. However, because the library uses consistent conventions it is relative easy to write parsers that identity the source lines of statements.

HOL Light inherits the OCaml module system. However, this is rarely used in practice. In any case, any modular features are invisible to the kernel.

The HOL Light library is highly integrated with the system and maintained by the same single person. That makes it very smooth to export by kernel instrumentation. Our export [31] modified the existing instrumentation to output OMDoc files directly. Additionally, it accesses an internal table with notations in order to preserve those in the export.

The most important other library is the Flyspeck proof [20]. We have not exported it because it is extremely big. It would also not be particularly interesting (except for porting the proof itself) as most generally reusable formalizations have been migrated from Flyspeck to the main library already.

HOL Light is among the easiest systems to export and to maintain an export for. This is due to the simplicity and stability of language, system, and library: The language is straightforward to model in a logical framework, and HOL Light avoids adding advanced or experimental features to HOL. The system is specifically designed as a lightweight rarely changing kernel, which makes it easy to understand and instrument the kernel to export proofs. And the library is very coherent and uses uniform conventions.

But its low-level kernel that users can feed arbitrarily with programmatically generated proofs makes it extremely difficult to export anything but low-level proof terms. Therefore, we cannot expect naive proof terms exports of large projects such as Flyspeck to scale without systematic changes. Even if a standard for mid-level proof terms in the sense of Sect. 2.5 exists, it will be difficult to export proof terms from HOL Light. The most realistic option would be to instrument not only the kernel but also individual tactics, and efforts in this direction have been made already [49]. But as users can write arbitrary tactics, this will require a significant investment of expert knowledge to be comprehensive. Establishing best practices and special macros for tactics with an eye toward instrumentation is helpful here.

Another major challenge is that HOL Light uses almost exclusively the homogeneous method, which makes it more difficult to integrate with other libraries. Here, it would be helpful to research the automated introduction of heterogeneity by abstracting from the assumptions theorems and grouping them according to their assumptions.

IMPS’s underlying logic, called LUTINS, is a variant of Andrews’ higher-order logic \(\mathbf {Q}^0\) [1]. Most characteristically, all functions are (potentially) partial, and terms may be undefined. The latter is captured by a primitive unary predicate for definedness.

IMPS uses a limited subtyping system: underneath each base type, a hierarchy of subtypes (called sorts in IMPS) may be introduced. Due to the partiality, the domain type of a function type is only an upper limit on the set of arguments for which the function is defined. Interestingly, that makes the function type operator covariant in both arguments.

Base types for individuals and binary booleans is built-in, and undefined constant applications that return booleans are considered false. Other base types and their subtypes can be declared in theories. Contrary to most other proof assistants, IMPS systematically uses the heterogeneous method, and theories routinely contain base types and operations on them whose properties are not given by definitions but by axiomatizations.

Some flexibility exists in how to represent LUTINS in LF. It is straightforward to give a Curry-style representation using \(\texttt {tp}:\texttt {type}\), \(\texttt {tm}:\texttt {type}\), and \(\texttt {of}:\texttt {tm}\rightarrow \texttt {tp}\rightarrow \texttt {type}\). Alternatively, we can give a Church-style representation for the maximal types and then a Curry-style representation for the sorts underneath each type: this would use \(\texttt {tp}:\texttt {type}\), \(\texttt {tm}:\texttt {tp}\rightarrow \texttt {type}\), \(\texttt {sort}:\texttt {tp}\rightarrow \texttt {type}\), and \(\texttt {of}:\varPi _{A:\texttt {tp}}\texttt {tm}\,A\rightarrow \texttt {sort}\,A\rightarrow \texttt {type}\). The latter allows LF to perform some type-checking automatically at the cost of making the representation a bit clunkier. For example, the latter requires all polymorphic operators to take two arguments: one for the type A and one for the sort \(S:\texttt {sort}\, A\). Finally, we can use a complete Church-style representation using \(\texttt {tp}:\texttt {type}\), \(\texttt {sort}:\texttt {tp}\rightarrow \texttt {type}\), and \(\texttt {tm}:\varPi _{A:\texttt {tp}}\texttt {sort}\,A\rightarrow \texttt {type}\). This yields the most elegant representation of the typing rules, but it requires explicit casts whenever subsorting is applied. It is relatively easy to switch between these, and the details of the trade off are ongoing work.

The only subtlety is the handling of binders as bound variables always range over defined values: All typing rules that introduce variables (\(\lambda \)-abstraction, universal introduction, existential elimination) must add assumptions to the context that assume the definedness of (the instances of) the bound variable. Correspondingly, the rules that perform substitutions (\(\beta \)-reduction, universal elimination, existential introduction) must have premises that ensure the substituting term is defined. In the first two alternative representations, this can be taken care of by formulating the rules in such a way that \(\texttt {of}\,t\,A\) only holds if t is indeed defined.

IMPS is implemented in LISP, and uses a LISP-like source syntax. Because it has not been maintained for years, it is rather difficult to work with. But previous work [42] had already developed a partial instrumentation to generate OMDoc files. Because that work predates Mmt and did not use any rigorous semantics for OMDoc, let alone logical frameworks, it is better seen as system-near XML export rather than as a semantics-preserving export.

IMPS stores proof objects that record tactic invocations made through a graphical interface. In addition to user-level tactics, special tactics (called Macetes in IMPS) are automatically generated from theorems of certain shapes, e.g., to turn theorems in Horn form into proof rules. This is particularly important to automate the tedious reasoning about subtyping and definedness. These proof objects contain gaps where IMPS automation was used. Thus, the proofs are already roughly mid-level proofs that can be more easily translated to other provers, and we expect that the missing steps can be recreated by the automation in those provers relatively easily.

Because the library is small, frozen, and part of the IMPS source code, it is relatively easy to export it once and for all in a single run.

Secondly, IMPS’s treatment of theory morphisms includes a subtle imperative part: after defining a theory T and some theory morphism \(m:S\rightarrow T\), users can install the morphism by imperatively adding the translations of S-theorems to T. While straightforward in an implementation that imperatively maintains theories as tables of declarations, it is problematic in exports. We could mimic it Mmt only by defining a new theory \(T_m\) that conservatively extends T with the corresponding definitions.

Finally, for a few rarely used unusual features such as the definition of what IMPS calls quasi-constructors, we simply collected all instances and formalized them in LF manually.

Our export provides an archive of the IMPS library in OMDoc. Additionally, because we also built system-near JSON representations and a fresh parser of the IMPS library, other exports can be built off these IMPS-near data structures in a way that by-passes OMDoc.

Even though IMPS is not in active use anymore, our export is designed to be maintainable so that future extensions can be developed. This would focus in particular on the export of mid-level proofs and on improvements to the representation of the idiosyncratic parts of the type system such as undefinedness and subtyping.

Isabelle uses a very simple higher-order logic called Pure as a logical framework. Therefore, we did not formalize Pure in LF; instead, we defined Pure as a logical framework in Mmt, i.e., as a sibling to LF.

Concretely, we represented Pure as the extension of LF with a type of propositions and shallow polymorphism. The latter allows using LF’s \(\varPi \)-binder also for type variables at the toplevel, which corresponds to the polymorphism of Pure. The primitive connectives of Isabelle (equality, universal quantification, and implication) are already part of the automated export because they are themselves declared in the theory Pure in Isabelle’s standard library. Extending LF is overkill as Pure is simply typed, not dependently typed, but an implementation of polymorphic LF was already available in Mmt. The additional expressivity has no downsides and is in fact helpful because we use the dependent types to represent Isabelle proofs as terms.

Because our export works at the level of Isabelle, it copies over all logic definitions in the Isabelle standard library as they are. In particular, as the types of Isabelle/HOL are a fragment of the types of Pure without using a Church or Curry encoding, both Pure and HOL types and functions are exported as types and functions of the logical framework. This eliminates the scalability hazard we discussed for Coq.

Isabelle features a complex module system with locales (and as a special case type classes) and morphisms between them. Their foundational details are very subtle and not always obvious, but these features are elaborated away almost entirely by Isabelle. Our export stays very close to the kernel-level representation, which is relatively simple to export and still recognizably similar to the user-level structure. While we usually advocate retaining the user-level structure as much as possible, the elaboration-based export has advantages here because Isabelle’s kernel-level language already regularizes some of the intricate idiosyncrasies of its user-level language. For example, we did not have to worry about the handling of type variables and contexts.

In particular, our export produces one predicate \(P_l\) for every locale l, which takes the types and operations of l as inputs and returns the conjunction of the axioms of l. All constants, definitions, and theorems of l are exported as constants that similarly abstract over all types and operations; additionally, theorems of l are relativized by \(P_l\).

Isabelle provides a heavily-used mechanism for users to define their own high-level declarations, whose semantics is defined by elaboration into more primitive one. Each one of those is called a specification construct. Examples include inductive types and recursive function definitions. These specification constructs are invisible to the kernel and lost during elaboration.

Mmt provides a corresponding mechanism for user-defined high-level features, which we could in principle use to preserve specification constructs features in the export. However, as elaboration is implemented directly in ML, this process cannot be automated, and a manual effort is needed for each specification construct to (i) define the corresponding feature in Mmt and (ii) extend the export with code for detecting and exporting its instances.

Similarly, the locale structure is lost entirely in the direct export. In particular, elaboration simulates the external heterogeneity of the user-level languages in terms of internal heterogeneity in the kernel. To recover the external heterogeneity, we have additionally reconstructed the original locale definitions and exported them as a diagram of Mmt theories. For example, a sublocale l and a locale \(l'\) become two theories \(T_l\) and \(T_{l'}\) with a morphism between them. The export is redundant in that it contains both these theories \(T_l\) and the predicates \(P_l\) produced by elaboration. While \(T_l\) covers all aspects of the definitions of a locale in a way close to user-level language, all uses of a locale are currently exported in terms of \(P_l\). A deeper integration between \(T_l\) and \(P_l\) remains future work.

Isabelle uses a coherent co-maintained standard library, which introduces in particular Isabelle/ZF and Isabelle/HOL. Additionally, user-submitted contributions are collected in the Archive of Formal Proofs library and, once accepted, also co-maintained.

Isabelle is the easiest to work with of all the systems we discuss here, featuring easy installation and a high-level export interface via Isabelle/PIDE. Our export work [38] is based on and helped facilitate major upgrades to the PIDE infrastructure, which has led to a very smooth kernel-instrumenting export module that is fully integrated with Isabelle. Moreover, because PIDE and Mmt are both written in Scala, we could skip the generation of intermediate files: we built an Isabelle plugin that makes the Mmt library available so that Isabelle can directly pass Mmt data structures to Mmt. This allows producing OMDoc files directly from Isabelle, making it the most maintainable and scalable of our exports.

However, even with the more space-efficient representation of expressions, Isabelle proof objects become very big. This is because (1) many commonly-used types (in particular inductive and record types) are elaborated, (2) Isabelle’s strong integration of automated provers makes it easy for users to build large proofs, and (3) the lack of implicit computation requires elaborating all computations into equational reasoning. Therefore, we have opted for a dependency-only export of proofs.

The Isabelle export is extremely well-maintainable as most of it was written by a core developer and deeply integrated with the Isabelle system and code base. The two biggest future challenges will be the avoiding elaboration and reducing the size of proofs terms.

Regarding elaboration, Isabelle is special among proof assistants in that it uses a very complex processing pipeline from heterogeneous user-level declarations to homogeneous kernel-level declarations. Not only does any export based on instrumenting the kernel lose a lot of valuable structure, it is also very difficult to modify the system to preserve that structure. The most realistic approach is to (1) modify the Isabelle data structures for user-level declarations in such a way that they must also govern how their concrete instances can be exported. For example, the feature for inductive types would have to include a function e for exporting any concrete inductive type definition. Existing language features would then (2) have to be adapted to this new interface, e.g., by adding that function e. This could then be combined with (3) mimicking the user-level features in Mmt to obtain a structure-preserving export. While (1) and (3) are relatively easy, (2) requires understanding and adapting a lot of code for the individual features—something that even experienced Isabelle kernel developers may not be able to do easily. For example, the developers of the inductive type feature themselves might have to write the function e, and doing that even for just the most important features would be a major effort.

Regarding the size of proofs, we expect the problem to be even bigger than for Coq because the computation of inductive functions (which is a primitive kernel feature in Coq) is realized via equality reasoning is Isabelle and therefore explicitly part of the proof term. Moreover, Isabelle’s extremely strong integration of automated provers increases the disconnect between user-level and kernel-level proof size: user-level proofs may simply consist of invoking automation, which then may produce highly circuitous proofs. In particular, the automatically found proof may differ strongly in size and structure from the proof a human would write or want. This can be alleviated somewhat by engineering efforts such as enabling structure sharing in the export. But to obtain an export of mid-level proofs as discussed in Sect. 2.5, investments into proof simplification may be needed. On the positive side, Isabelle’s Isar language already allows users to write mid-level proof terms explicitly. Thus, it is promising (but still difficult) to export Isar proof terms enriched with information from kernel-level proofs.

Due to its idiosyncratic syntax, the Mizar language is often confusing. But logically, it is actually very simple: it is a formalization of Tarski–Grothendieck set theory in untyped first-order logic with toplevel second-order binders (which are needed to formalize schemas). This can be formalized routinely in LF. Structures/records are realized as functions, whose domain is a special set of names. This is also easy to formalize although, without Mizar’s special syntax support for it, the representation is hard to read. Mizar allows for a large but fixed set of definition principles. These were difficult to identify and compile, but then straightforward to represent as high-level Mmt statements [26].

Additionally, Mizar uses a soft type system, where types are defined as unary predicates over sets. This type system is undecidable, and Mizar provides automation for discharging type-checking obligations, partially guided by user-tagged typing theorems (called registrations). Because this type system is internally represented as typing axioms/theorems about the terms in untyped first-order logic, the direct representation in LF is also straightforward.

However, we could do better: Our Mizar export predates Mmt implementations of LF with predicate subtypes. In a reimplementation, we would investigate representing a Mizar type T as the predicate subtype of the type of sets containing those sets that satisfy \(\ulcorner T\urcorner \) (akin to how we used predicate subtypes in the Coq export). This would allow preserving the type system in the export. However, in that case, rechecking the export would require reproving the type-checking conditions discharged by Mizar, a non-trivial task.

Mizar is one of the oldest proof assistants around and was originally designed in relative isolation. Moreover, due to its focus on mathematics, the user community has remained much smaller than those of the other systems that can be used for software verification. Therefore, it is the least accessible of all the provers we worked with.

A Mizar export can be best written based on the XML files generated by Mizar. In fact, these were introduced by Josef Urban for that purpose [63] and later became used internally. Therefore, they contain all relevant information. But the XML schema is very complex, not always documented, and may change across Mizar versions.

Our export [27] uses the XML files. It was relatively easy to build and to export the Mizar Mathematical Library, the single coherent library that is co-maintained with Mizar. The main difficulty was that a system expert was needed to explain the XML schema: because the XML is used internally, it also represents many implementation details that are irrelevant for the export and is therefore even more complex than the user-level language.

The internally used XML is undergoing regular improvements. While this has generally made the structure of the XML better and the export easier, partially in response to our feedback, this has made the export very expensive and near impossible to maintain over multiple years.

Mizar uses a big kernel with substantial built-in automation, in particular for the soft type system. These proof steps are not exported and therefore occur as omitted steps in the export. Except for these gaps, the proofs are mostly available in the same high-level format in which they were written by the user.

Maintainability is a big challenge for our and future Mizar exports. The concepts of the Mizar language, its code base, and the structure of the generated XML files are hard to understand. This is partially inherent in the system and partially an artifact of the Mizar community overlapping less with over proof assistant communities and the broader computer science community.

A logistical challenge here is that the Mizar developer community is small and mostly concentrated in Białystok, Poland, and therefore not as deeply connected with other prover communities. Moreover, the resource-intensive maintenance of the system and the library limits the community’s ability to invest into prover-near exports. But recent improvements to the Mizar XML representation by the Mizar developers are very promising, and we have recently resumed our export efforts in collaboration with Artur Kornilowicz.

A promising avenue is the reconstruction of the Mizar system in a logical framework in such a way that the Mizar library can be migrated to the framework and—in the long run—the Mizar retired. The main challenges here are mimicking the highly human-friendly concrete syntax of Mizar and the automated reasoning capabilities. Promising first results have been accomplished in [30] on top of Isabelle. A modern reimplementation on top of an LF-like framework, e.g., implemented in Mmt, could also be promising: it would allow for supporting Mizar’s dependent types more naturally but would hardly be able to match Isabelle’s automated reasoning.

A proof export from Mizar is generally difficult because not all proofs are currently stored in the system. Because the Mizar kernel is large and complex, instrumenting it for full proof export would require a major effort. However, an export of mid-level proofs in the sense of Sect. 2.5 is already possible although we did not focus on it. A related problem is that Mizar elaboration expands many abbreviations including for basic symbols like implication. Both instrumenting these expansions during or reintroducing the abbreviation after an export are very difficult, and only a few qualified system experts exist for such tasks. A reconstruction inside Isabelle would allow reducing those problems to the existing Isabelle export technology.

PVS uses higher-order logic for which a Church-encoding works well. But it adds major additional features that go beyond what can be formalized in any declarative logical framework. Therefore, we extended LF with appropriate features as described below.

Instead, we extended LF with predicate subtypes (which we already used for Coq already). This makes it possible to formalize PVS’s predicate subtypes in a straightforward way while maintaining the advantages of using a Church encoding. We inferred the additional arguments required for the Church representation in the logical framework, which turned out to be just feasible for a dependency-only export of the PVS libraries. Alternatively, we could have used the weaker Curry-encoding as for Coq.

Module System PVS uses an unusual module system. Theories may carry parameters, and theories may include multiple instances of the same theory with different arguments, e.g., to include lists over booleans and lists over integers. All these includes use the same included identifiers, and PVS disambiguates for each occurrence of an identifiers which instance it belongs to. Consequently, internally all included identifiers carry a long list of implicit arguments that instantiate the parameters.

There is a subtle problem here: As not every identifier depends on all parameters of a theory, it is possible that identifiers included via different instances are actually equal. As that equality is undecidable, it becomes undecidable which set of identifiers has been included. Therefore, PVS’s parametric includes are very difficult to eliminate in the export. Therefore, we chose to mimic them by adding a special include-declaration that abstracts over all parameters of a theory.

Finally, PVS uses primitive (co)inductive types and elaborates them into an axiomatization. That makes it possible to skip them and to export the elaborated statements only. But we still had to use some extensions of LF to represent the associated recursive functions.

PVS includes a very well-built export facility based on kernel-generated XML files written by Sam Owre. This is intended specifically for exports like our as well as knowledge management applications like search. PVS was the only system encountered that already had such a system-near export facility specifically designed for that purpose by the developers.

Because PVS uses a big kernel, very little elaboration takes place. Therefore, the XML files include all user-level information enriched with the information inferred by the kernel. This includes virtually the entire original source structure, down to source references and redundant brackets.

Because the type system in undecidable, every statement generates some type-checking-conditions, which must be proved separately. After proving these, PVS inserts them before the respective statement. Exports can choose to include or skip these additional theorems.

PVS uses a small standard library, called the PVS prelude. Other libraries are distributed, but only the big NASA library is used widely. PVS releases are regression-tested against this library.

Our export [36] used the generated XML files for both libraries. As a part of this export collaboration, the XML schema was heavily debugged and well-documented. Concretely, we represented the PVS XML schema in Scala, and then generated Mmt data structures from it directly. Our Scala implementation of the PVS XML schema is also a valuable resource as an alternative documentation of the PVS language. The export worked very smoothly (once the theoretical challenges had been resolved). A minor problem we encountered were that the source files in the NASA library must be built in a specific order, a process that PVS does not automate well yet.

PVS stores high-level proof objects in separate files. But the big prover kernel uses a lot of automation that is not recorded in these proof objects, in particular the heavy use of decision procedures. Thus, proofs have significant gaps.

PVS supports a very robust and well-documented export to XML that includes all user-level declarations. That makes it relatively easy to build and maintain exports.

The biggest challenge is that PVS uses a few unusual language features. This includes (co-)inductive types and recursion at a similar level of difficulty as in Coq. (Coq uses dependent types and PVS uses predicate subtypes; neither subsumes the other, but both cause similar difficulties.) But it also includes an unusual kind of includes between theories, theory parameters representing theory morphisms, anonymous record types, and operators for function/record updates. While these features are quite justifiable, their subtleties make representing the language in a logical framework difficult. We were able to do so by extending the LF with corresponding features so that transporting the library to other systems remains difficult.

Just like for Mizar, a complete export of proofs is not possible as many proof steps are performed automatically by a large kernel and not tracked. However, once an appropriate standard as discussed in Sect. 2.5 exists, an export of mid-level proof terms can be realized based on XML files containing partial proof objects.

The most important lesson to draw from our work is that prover library exports are possible but very difficult and tedious: Theoretically, they require state-of-the-art representations of logics in logical frameworks and even the design of new framework features. Here the development of Mmt, which makes implementing these logical framework feasible, was critical. Indeed the exports motivated and drove the development of new features in Mmt.

Practically, each export required enormous amounts of work both from us and from a dedicated collaborator on the system side. Each export runs into numerous rare and/or undocumented subtleties that require extensive communication between these two. Here careful planning was critical to avoid running out of time, personnel, or funding half way through. Because of this high threshold to have working exports at all, many added value services and system interoperability solutions that would otherwise be in reach (albeit still subject to substantial to research efforts) can hardly be attempted at all. With our six working exports this work can commence now, and indeed we are in contact with multiple groups that are already using them.

It is also difficult to rigorously represent the syntax and semantics of the logics of practical provers. Formal descriptions of the exact logics realized in the provers are typically incomplete, outdated, and/or distributed over multiple publications. In particular it is virtually impossible to clarify all details without talking to a system expert. We even routinely resorted to reverse-engineering the internals of the kernels to find out how corner cases are actually treated. It is even harder to then represent these logics in logical frameworks. While the latter are excellent for textbook logics such as FOL, HOL, or pure type systems, the representations of all features used in practical provers go beyond their current expressive power. This observation limits the promise of logical frameworks like LF and has been a major motivation behind the development of Mmt: it allows expanding the logical framework flexibly with the language features necessary to represent the object logic at hand, whereas any attempt to export a proof assistant library to a fixed logical framework is bound to hit expressivity limits. But even with the flexibility afforded by Mmt, the task remains very difficult. But the investment is well-spent, as the formalization can serve as an exact, consolidated, and up-to-date documentation of the details and semantics of the logic actually used in the system.

Because of the above, it is important that exports always preserve all details of the prover’s logic and refrain from mixing the export with non-compositional transformations to eliminate complex or idiosyncratic features of the logic. The latter may sometimes be necessary, especially to integrate libraries across provers. But the question of how to do such transformations is in itself a difficult research question, and it should be separated from the engineering question of realizing any export at all.

We have not touched on logic translations and library integration in this paper, a task that may build on top of the exports we have discussed. It remains a separate and very difficult problem, and we are not sure yet which approach will prove most successful here. However, we want to stress one negative result: it does not work to give a translation from base logic L to base logic \(L'\) and then use that to automatically translate an L-library to \(L'\). Believing that such an approach might work is a misconception that we suffered from ourselves 10 years ago and that we have encountered among many colleagues since.

For example, to translate the Coq library to PVS, it is neither sufficient nor necessary to give a translation from Coq’s calculus of inductive constructions to PVS’s higher-order logic. Giving such a translation is very difficult because the base logics are so different: several Coq features such as universes and dependent types cannot be expressed directly in terms of PVS features. A partial translation that leaves out those features would be impractical as well as pointless as they are used pervasively in Coq. But any translation that includes those features would have to be a deep embedding, e.g., by translating all Coq types to terms of a designated PVS type. This would induce a translation of the Coq library to PVS, but the image of the translation would be as semantically disconnected from the PVS library as the original Coq library was. Already the Coq propositions (which are types) would not be translated to the PVS booleans, and this alignment problem only gets worse the more advanced the concepts defined in the libraries become [28]. Note that the alignment problem exists even when there are easy translations such as the straightforward shallow embedding from HOL Light to PVS. Therefore, practical library translations must provide special case treatment not for the primitive features of L but for the concepts defined in the library of L. If such special treatment is done anyway, the translation between the base logics becomes optional.

Exports We are convinced that any future interoperability between proof assistants will require library exports of some kind. In the long run, the community must organize and invest efficiently the resources needed for prover developers to build and maintain such exports.

Major efforts will be needed to export libraries of more provers. Because of resource constraints, we had to choose representative provers so far, and some like ACL2, HOL4, Lean, Metamath, and Nuprl are still prominently absent at this point. We regret the lack of resources that has precluded us from developing exports for those systems as well. Some of them would be particularly interesting, e.g., to compare the much younger Lean system to the logically similar but older Coq, or to have more libraries that are untyped (ACL2, Metamath) or have very expressive type systems (Nuprl) to compare integration problems between the different styles of typing.

But we believe that our choice of systems is representative for the challenges faced during exports. However, note that logical similarly or even equivalence such as between Coq and Lean or HOL Light and HOL4 is not the most relevant indication for these challenges. While logical issues such as the representation of the type system in the logical framework are indeed similar, the biggest challenges are often in the engineering where equivalent systems often differ drastically. Indeed, perceived engineering improvements are often the reason behind system forks and re-implementations. For example, a Lean export would likely be entirely different from our Coq export, whereas an export HOL4 could be relatively similar to our HOL Light export.

In addition to what we presented here, we have so far developed additional (sometimes partial) exports for some systems including TPS, Specware, and Metamath as well as for a few computer algebra systems, while we have not discussed those here, our conclusions apply to and are informed by them as well.

Imports and Library Alignment Importing from a simple standardized representation format like ours into a prover is relatively simple in principle. However, that appearance hides the real difficulty, which is the alignment problem described in Sect. 9.1. Indeed, the exported libraries remain disconnected even the though they are now in the same format.

Even though the alignment problem was recognized in [50] already, which also gives the first solution in a practical setting, it has remained difficult. Major case studies so far are [61] for aligning many different small libraries and [18] for aligning two large ones. We gave a survey of issues in [28], and if anything, we see a longer list of difficulties by now.

Further research is needed to design such intermediate formats. State of the art formats are quite strong at representing expressions (terms, types, formulas, etc.) from a diverse set of systems in a simple uniform language. But they are much weaker at representing high-level declarations and proofs. Well-designed abstractions for declarations such as inductive types, functions, and proofs, or record types and terms would simplify the library integration problem.

Similarly, the treatment of extra-logical declarations is difficult because systems so widely here that it is unclear how much can even be reused in other libraries.

Direct Translations An alternative approach is to develop direct translations without an intermediate format. Current users are already doing that ad hoc and on a small scale when they manually port developments from one system to another based on need. We could invest into this by systematizing and automating the process.

Even though this is less attractive in principle as it would require translations for any pair of systems, this may still be sufficient in practice for two reasons. Firstly, there may never be that many major systems for which library integrations are critically needed, maybe even fewer than there are today. Secondly, even the more generic solutions via an intermediate format may end up requiring substantial library-pair-specific work anyway when fine-tuning the alignments.

We can imagine an approach similar to the automated generation by Isabelle’s sledgehammer component of structured Isar proofs from automatically found proofs. Here a theorem of system L could be turned into a theorem of system \(L'\) through a combination of a formal logic translation, a database of alignments between L-symbols and \(L'\)-symbols, and some (possibly machine-learned) heuristics. The resulting theorem and proof might not be well-formed in \(L'\) and require further editing. The latter could happen manually or via an automated iteration that tries multiple variants until one of them is accepted by \(L'\).

A logistic advantage of this approach is that it may be more appealing to the \(L'\) developer and user community for two reasons. Firstly, it has a more immediate return on investment for users. Secondly, it could plausibly yield \(L'\)-verifiable proofs faster than any approach based on an intermediate format. On the downside, due to the high resource requirements, only few systems \(L'\) might be able to sustain such translations.

Scalable and maintainable exports require some design decisions that are not obvious in the beginning because they often do not affect the remainder of the system. Exports typically only become interesting once a large library has been built, and at that point retrofitting export architectures to mature systems usually presents substantial difficulties. On the positive side, integrating these design recommendations into new systems is relatively easy and has overall positive side effects outside the export facility. Concretely, we recommend the following: