Skip to content

Dependencies of MMT and what they're used for

ComFreek edited this page Oct 16, 2020 · 3 revisions

MMT as a Scala/JVM project has several dependencies on external JVM libraries and binaries.

The main dependencies are stored in the repository as unmanaged JARs in deploy/lib. Some other dependencies, notably of the frameit-mmt subproject are given in src/build.sbt (for some specific sample lines from the current commit at time of writing, for instance, see here). And yet some other dependencies are dynamically pulled from MMT archives (e.g. computation or typing rules provided by those archives) or expected to be present in the environment in which mmt.jar is used.

Below is a rough elaboration on the main dependencies of MMT's core (mmt-api and mmt-lf) and what they are used for. It was contributed by Florian on 2020-10-16 (he said "I've never tracked this formally, but the following should be mostly right").

Concerning the scala-* libraries in deploy/lib:

  • scala-parser-combinators: only used for parsing MMT shell commands (and also used by mmt-imps)
  • scala-reflect: probably only a few peripheral features (like parsing PVS XML)
  • scala-compiler: scala-bin target, escaping to Scala shell from within MMT shell
  • scala-xml: any use of XML like the OMDoc
  • scala-library: the Scala standard library, used throughout, mostly for collection datatypes

External libraries:

  • xz: compression of OMDoc files on disk (also in deploy/lib)
  • tiscaf (now treated as a subproject because I once fixed a few bugs in it): HTTP server

Even if they're not called at run time, all libraries may still need to be present during compilation - not sure about that.

Additionally, jEdit-mmt assumes that jEdit and a few plugins (see jEdit-mmt/lib) will be available at run time. They're not part of mmt.jar but must be around at compile time.

Finally, if an archive designates a folder containing JVM binaries, MMT makes them available at run time through a custom class loader for rules and extensions.