Isabelle/MMT requires a version of Isabelle that fits precisely to it. The
latest stable release is for Isabelle2019 (June 2019), but intermediate
development versions require a later Isabelle repository clone according to
ISABELLE_VERSION -- see also https://isabelle.sketis.net/repos/isabelle and in
particular the file
README_REPOSITORY section Quick start in 30min.
In particular, the following versions from Aug-2019 should fit together:
- Isabelle/7bf683f3672d from https://isabelle.sketis.net/repos/isabelle
- AFP/482f1b8d56ea from https://isabelle.sketis.net/repos/afp-devel
- MMT/7ce4fac80722 from https://github.com/UniFormal/MMT/commits/devel
- MathHub/MMT/urtheories/12cc343c279c from https://gl.mathhub.info/MMT/urtheories/commits/devel
The corresponding OMDoc content is available here (commit messages refer to the underlying versions of Isabelle + AFP):
Isabelle/MMT is a command-line tool within the Isabelle system environment.
Both building and running it requires proper Isabelle component setup, which
results in certain environment variables in the enclosing process. For
general explanations, see the Isabelle system manual (chapter 1), e.g.
available in the Documentation panel of Isabelle/jEdit. The MMT
src/mmt-isabelle already provides suitable component
settings that can be activated e.g. in
.../MMT refers to the full path specification of the MMT source
directory. Note that a standalone
mmt.jar is not sufficient: the Isabelle
component requires some regular files from the MMT source tree.
Here are some example invocations of the main command-line tools:
isabelle mmt_import -B ZF isabelle mmt_import -g main isabelle mmt_import -o record_proofs=2 -B HOL-Proofs
HTTP server to browse the results:
isabelle mmt_server -A isabelle_test
development with IntelliJ IDEA:
isabelle env idea
build.sbthas some tricks on conditional project composition: it requires to re-initialize the IDEA project after dropping in or out of the Isabelle system environment.
Recall that Isabelle consists of two processes:
polyfor the Poly/ML runtime system
javafor the Java Runtime Environment
Big examples require generous heap space for both, typically 30 GB. Note that both platforms have a discontinuity when switching from short 32-bit pointers to full 64-bit ones: 16 GB for Poly/ML and 32 GB for Java. Going beyond that doubles the baseline memory requirements.
The subsequent setup works well for hardware with 64 GB of main memory:
ML_system_64 = true
ML_OPTIONS="--minheap 4G --maxheap 30G" ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xss16m -Xms4g -Xmx30g"
isabelle mmt_import -a -X doc -X no_doc isabelle mmt_import -d '$AFP' -a -X doc -X no_doc -X slow isabelle mmt_import -d '$AFP' -a -X doc -X no_doc -X very_slow
$AFP refers to the Isabelle settings variable provided by the Archive
of Formal Proofs as Isabelle component (using a suitable
$ISABELLE_HOME_USER/etc/settings). Alternatively, it is possible
to refer to the physical AFP directory as
.../AFP/thys (the sub-directory
thys is important here).
Directory layout for MathHub
The MMT MathHub keeps the main Isabelle Distribution separate from the
Archive of Formal Proofs. The
isabelle mmt_import tool can use the chapter
structure of Isabelle sessions to distribute documents into different
archives. Its option
-C provides (multiple) mappings from chapter names to
archive names (according to the base directory name). The chapter name
serves as catch-all pattern.
Since all sessions in AFP are guaranteed to belong to the chapter
following works for Isabelle + AFP as one big import process:
isabelle mmt_import -d '$AFP' -A content/MathHub -C AFP=AFP -C _=Distribution -a -X doc -X no_doc -X very_slow
Note that other Isabelle applications may have their own chapter naming
scheme, or re-use official Isabelle chapter names; if nothing is specified,
the default chapter is
The entry points for Isabelle/MMT tools reside in the MMT directory
src/mmt-isabelle/lib/Tools -- usually some shell scripts that invoke Java
within the Isabelle environment, to pass the control over to some Scala
main() functions. The actual implementation is provided by regular Scala
functions, without assuming a command-line context.
The usage of command-line tools generally follows GNU bash standards: the
Isabelle/Scala library provides an imitation of GNU
getopts for that.
Output and error behavior follows established standards for Isabelle
command-line tools. In particular, internal Java exception traces are not
shown to end-users by default.
This is a thin wrapper for
sbt mmt/deploy within the formal Isabelle
environment and the correct directory in the MMT source tree; it trims the
resulting jar to avoid duplicates of Scala libraries. Furthermore, it
ensures that Isabelle/Scala has been properly bootstrapped beforehand (e.g.
when working from the Isabelle repository).
This is the main Isabelle/MMT importer: it explores Isabelle sessions and loads all resulting theories into an Isabelle/PIDE process. Results are continuously imported into MMT and written to specified math archive directories. Its command-line usage is as follows:
Usage: isabelle mmt_import [OPTIONS] [SESSIONS ...] Options are: -A DIR add archive directory -C CH=AR add mapping of chapter CH to archive AR, or default "_=AR" -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -R operate on requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions -d DIR include session directory -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose mode -x NAME exclude session NAME and all descendants Import specified sessions into MMT archive directories.
-C specify target archives and a mapping from Isabelle
session chapters to MMT archives. Chapter names are provided in Isabelle
ROOT specifications, and archive names are the base directory
names: if it is the same as the chapter name, the directory will be used at
its root; otherwise the chapter becomes a sub-directory of the archive. The
directories given via (multiple)
-A options are recursively searched for
MMT archives. If the result is empty, a fresh archive is initialized
according to Isabelle system options
mmt_archive_dir etc. Thus it is
possible to use
isabelle mmt without any archive options and get results
into a default directory (
isabelle_test), freshly initialized on demand.
-x with remaining
non-option arguments provide the standard Isabelle vocabulary to specify
sessions, e.g. see
isabelle build described in the system manual (with
-o allows to augment the environment of Isabelle system options,
before invoking the main import process; see again the system manual. A
typical example is
-o threads=8 to specify the number of ML threads, or
-o skip_proofs to skip actual proof checking. Note that Isabelle/MMT also
provides its own options in
src/mmt-isabelle/etc/options (with short
-v enables verbose mode, similar to
This is a thin wrapper for the regular MMT web server. It refers to archives
in a similar manner as
isabelle mmt_import; thus it is useful to explore
the results of that tool. The command-line usage is as follows:
Usage: isabelle mmt_server [OPTIONS] Options are: -A DIR add archive directory -p PORT server port (default: 8080) Start MMT HTTP server on localhost, using specified archive directories.
-A refers to archive directories that are recursively explored as
isabelle mmt_build. In order to refer to the default archive of that
-I above), it needs to be included explicitly as
isabelle mmt_server -A isabelle_test.
-p specifies an alternative HTTP server port.
This is a thin wrapper to the standard MMT shell, running within the
Isabelle system environment, with both the
mmt.jar and the Isabelle/Scala
jars in the Java name space. In particular, dropping into its
toplevel allows to explore Isabelle and MMT functionality interactively on
the Scala toplevel.
The command-line usage is the same as for the regular MMT shell.