MMT can be used as a build tool using a special shell command.
build ARCHIVE TARGET [P/A/T/H] runs the build target TARGET on the archive with id ARCHIVE. Optionally, the operation can be restricted to the subfolder P/A/T/H.
The collection of build targets is maintained by the extension manager. New build targets are defined by implementing the archives.BuildTarget class.
Build target modfiers and change management are supported for automatically for every build target.
TARGET* only operates on input files that have been modified since the last build.-TARGET cleans, i.e., deletes the generated files.The file-properties of the operating system are used to detect changes. Timestamps for the previous build are stored in META-INF/timestamps.
Any target may be followed by a modifier. Apart from --force, other supported modifiers are --forceDeps (which also forces building of dependencies), --depsFirst, --onChange, --onError, --dry-run and --clean (as well as --test,--test-add and --test-update). Omitting the modifier defaults to --onChange, i.e. files are only rebuild if they have changed on disk after an earlier build. (--onError rebuilds if the previous build failed with an error.)
Many build targets work with input and/or output dimensions. Those are the top level folders within an archive. The most important build targets (which are available by default) include:
| Target | Input dimension | Output dimension | Provided by | Description |
|---|---|---|---|---|
| index | source | content, narration, relational | api | indexes and prepares OMDoc source files for MMT lookups, the produced dimensions are from where MMT retrieves content, documents, and the ontology, respectively |
| mmt-omdoc | source | as index | api | like index but parses and type-checks MMT source files instead of OMDoc files |
| twelf-omdoc | source | as index | LF plugin | like mmt-omdoc but for Twelf syntax |
| html | narration | html | api | produces html website, which relates to source roughly as JavaDoc does to Java |
| svg | narration | svg | api | produces theory graphs |
| scala | content | scala | api | produces Scala stubs for all MMT theories |
| lf-scala | content | lf-scala | LF plugin | produces LF-aware typed Scala stubs |
| mar | multiple | none, produces file NAME.mar | api | creates a math archive, a zipped collection of the archive |
See Build Queue for detailed information on multi-threaded building.
See Error Viewer for detailed information on seeing the results of building many files.