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_build to (re)build the MMT project inside the Isabelle system environment (only required after change of the Scala sources)
• isabelle mmt_import to import the content of a headless Isabelle/PIDE session into MMT (OMDoc and RDF/XML triples)
• isabelle mmt_server to present imported content using the built-in HTTP server of MMT
• isabelle mmt to run the interactive MMT shell inside the Isabelle system environment, e.g. for experimentation within the Isabelle + MMT package namespace, using the scala sub-shell.

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.

Naproche-SAD is a recent tool by Frerix and Koepke, based on the original System for Automated Deduction (SAD) by Paskevich and others. It processes the Formal Theory Language (ForTheL), which is designed to look like mathematical text, but it is restricted to a small subset of natural language.

The tool is implemented in Haskell as a plain function from input text to output messages. A file is like a chapter of mathematical text, with a nested tree-structure of elements and sub-elements (for signatures, axiomatizations, statements, proofs). Output messages inform about the translation of mathematical text to problems of first-order logic, and indicate success or failure of external proof checking; the latter is delegated to the E Prover by Stephan Schulz and can take several seconds for each proof obligation.

To integrate Naproche-SAD into PIDE, Frerix and Wenzel have reworked the Haskell program over 2 months in 2018, to turn the command-line tool into a service for reactive checking of ForTheL texts. Isabelle integration was done via the new Isabelle/Haskell library and some glue code in Isabelle/Scala to register ForTheL as auxiliary file-format (extension .ftl).

The resulting Isabelle/Naproche application is available as multi-platform download. A running instance is shown in the screenshot: users can directly open ForTheL files (e.g. from Documentation / Examples) and wait briefly to see output messages attached to the text in the usual IDE manner. Further edits produce a new version of the text, which is sent in total to Naproche-SAD again. The back-end is sufficiently smart to avoid redundant checking of unchanged sub-elements: it keeps a global state with results of old versions: this is easy to implement as the program keeps running until shutdown of Isabelle/PIDE.

(Cited from section 1.2 of the paper Interaction with Formal Mathematical Documents in Isabelle/PIDE.)