MMT is a language, system and library (in Scala) to represent a broad range of languages in the OMDoc format: this supports formal, informal, semi-formal content. The MMT repository includes
general APIs to operate on OMDoc theories, together with various tools and applications. There are several MMT sub-projects to connect to other systems. This includes Isabelle/MMT, which appeared as preliminary version already in Nov-2018.
The release of Isabelle2019 (June 2019) is an opportunity to distribute MMT version 17.0.0 (May 2019) as Isabelle application. An alternative is to incorporate the underlying Isabelle component manually into Isabelle2019 in
$ISABELLE_HOME_USER/etc/settings like this:
init_component ".../mmt-20190611" — where the three dots refer to the directory where the component
tar.gz has been unpacked.
In either case, the
mmt.jar of the MMT distribution is included in the Isabelle/Scala package name space. The component provides Isabelle command-line tools as follows:
isabelle mmt_buildto (re)build the MMT project inside the Isabelle system environment (only required after change of the Scala sources)
isabelle mmt_importto import the content of a headless Isabelle/PIDE session into MMT (OMDoc and RDF/XML triples)
isabelle mmt_serverto present imported content using the built-in HTTP server of MMT
isabelle mmtto run the interactive MMT shell inside the Isabelle system environment, e.g. for experimentation within the Isabelle + MMT package namespace, using the
The main functionality is provided by
isabelle mmt_import: that is a medium-sized Scala module (57KB) within the MMT code-base (file
src/mmt-isabelle/src/info/kwarc/mmt/isabelle/Importer.scala). It refers to general export facilities of Isabelle/Scala, which are part of the Isabelle2019 distribution (file
src/Pure/Thy/export_theory.scala). The latter may be studied independently of MMT in the implementation of the
isabelle dump tool (file
src/Pure/Tools/dump.scala); see also the Isabelle System Manual, section 2.6.
The following papers provide further explanations on Isabelle/MMT:
- Relational data across mathematical libraries, notably section 3.1 about exported content (OMDoc and RDF/XML).
- Isabelle technology for the Archive of Formal Proofs, notably section 4 about tool integration.