Installation

To work with MMT, proceed as follows:

1. Check out MMT and the MMT example documents from the SVN repository

   svn co https://svn.kwarc.info/repos/MMT/src/ mmt
   svn co https://alpha.tntbase.mathweb.org/repos/cds cds
   

Downloading the example documents is optional.

2. Set up content sources. Content is identified by URIs, which are mapped to URLs via a catalog. The catalog is configured by two commands.
   • Catalog entries for directories in the local file system are created with

     catalog FILE
     

     Conceptually, an entry in the file FILE is of the form URIBase:URLBase and translates URIs URIBaseURISuffix to URLBaseURISuffix. For the concrete syntax, see the example file locutor.xml.example.
   • Catalog entries for an MMT-aware database backend are created with the command

     tntbase FILE
     

     Here FILE produces a single entry in the catalog. However, it also provides URL templates to query not only full documents but also document fragments via MMT URIs. Moreover, it can provide additional query templates that (if given) are used by the MMT system to retrieve notations to render documents, and ABoxes that describe MMT documents in the MMT ontoloty. The file ../ombase.xml is preconfigured to communicate with the TNTBase backend maintained by Kwarc.

3. To build mmt-api/mmt-web yourself, run

   cd mmt-api/trunk
   ant
   cd ../../mmt-web/trunk
   ant
   cd ../..
   

If the mmt-api code has changed, it must always be built before building mmt-web.

You can also import the Eclipse project and build or run the projects from within Eclipse. To do that, you need the Scala plugin for Eclipse, and you probably want to use the Run Jetty Run plugin to run mmt-web.

4. You can now run the mmt-api shell using

   cd mmt-api/trunk
   ant
   java -jar build/mmt-api.jar file startup.mmt
   

5. You can run the the web server using

   cp startup.mmt.example startup.mmt
   cd mmt-web/trunk
   ant
   java -jar lib/jetty-runner.jar --port 8080 build/mmt-web.war 2>&1 > jetty.log
   

   This uses the provided jetty-runner as a servlet container. The port is arbitrary. Alternatively, you can deploy mmt-web.war in any other way, e.g., using tomcat or jetty.

Now point your browser to, e.g.,  http://localhost:8080/;?http://cds.omdoc.org/logics/first-order/proof_theory/derived.omdoc???present_http://cds.omdoc.org/foundations/lf/mathml.omdoc?mathml

The server applies the notation definitions and wraps the result in the templates

 https://svn.kwarc.info/repos/MMT/src/mmt-web/trunk/web/templates-hidden/wrapper.html and  https://svn.kwarc.info/repos/MMT/src/mmt-web/trunk/web/templates-hidden/browser.html These include JOBAD javascript and OMDoc css.

Note that the all aspects of the appearance of the served xhtml documents can be changed very easily by editing

• the above templates (with a plain html editor),
• the css files,
• the notations.

You can kill the server using  http://localhost:8080/:admin or by pressing CTRL-C in the shell.

Demo

To see a demo of what MMT can do, run in mmt-api/trunk

java -jar build/mmt-api.jar file examples/demo.mmt

in step 4 above. See the comments in demo.mmt for documentation.