16th Git Release

• New primitive concept of derived modules (in analogy to derived declarations)
• New declaration objects for diagrams and diagram operators (paper)
• New importer for Coq library, based Sacerdoti Coen's XML export paper
• Improvements to MMTTeX for putting MMT syntax into LaTeX files
• First version of database generator for schemas written as MMT theories MBGen
• First version of theory generalization (see here)
• Improvements to the Jupyter Kernel
• Improvements for TGView, ported to TypeScript in an external repository
• Much improved documentation of package objects in mmt-api (can serve as entry points for reading API doc)
• Lots of minor improvements and bugfixes as well as cleanup of Scala warning including deprecation warnings (now < 100 warnings)

15th Git Release

• IDE Improvements
  • Support for the MMT Plugin for the IntelliJ-IDE
  • added a Scala console to JEdit to interact with MMT’s internal classes from within jEdit
• New examples in MMT/examples
  • resource semantics of linear logic (logic/linear.mmt)
  • prototypical theorem prover (logic/prover.mmt)
  • proof irrelevance as a logical feature (logic/pl.mmt)
  • inductive functions on lists as special cases of rewrite rules (lists.mmt)
  • case study on implicit morphisms: lattice of theories of regular bands
• New Concrete link syntax
  • for includes that include a morphism expression as opposed to an MMT URI
• Added support for right-associative delimiters in mixfix notations
  • Use %Rd for delimiter d that associates to the right
• Cleanups and additions to various internal components
  • first steps towards implicit coercions
  • new class DocumentLevel (e.g., archive, folder, file, theory, etc.); every document now carries it level
  • new elementEnd calls after processing container elements in all MMT components
  • dropped distinction between declared and defined elements, container elements now inherit from ModuleOrLink class
  • re-implemented applicability check of checking rules
  • various cleanups of the MathHub API
• compatible with major reimplementations of archives:
  • LFX
  • MitM/Foundation
  • MitM/smglom

14th Git Release

• MitM infrastructure for using MMT as system integration mediator (as used in the OpenDreamKit project)
• major rewrite of the type checker to allow for head normalization with an arbitrary set of rules
• MMT kernel for Jupyter; import/export of Jupyter notebooks
• complete importer for Isabelle libraries by Makarius Wenzel (see his blog post for details)
• OMDoc files now stored in compressed form using xz (requires clean rebuild of archives to remove old OMDoc files)
• major progress on the IMPS importer
• rework of the MathHub API
• minor lmh cleanup
• stopped using sbt test for integration tests (makes them more reproducible)
• compatible with major reimplementations of archives:
  • LFX
  • MitM/Foundation
  • MitM/smglom
  • All ODK Archives

13th Git Release

• new class AnnotationProvider for providing extra information on MMT declarations these are shown in particular in the jEdit gutter
• first version of structural features for inductive types, record types
• improved statistics generation
• major progress on Isabelle importer
• minor improvements of GAP/Sage-Imports and LMFDB-Plugin

12th git release

• lmh can now handle non-archive repositories
• new MathHub Extension
• Dockerfile improvements
• SBT dependency changes
• Switched the IMPS importer to parser combinators
• added a Python bridge to control MMT from Python (using Py4J), see python-mmt
• started Isabelle importer (see mmt-isabelle)
• MMT tasks now carry progress messages (currently sent by structure parser/checker/elaborator)
• jEdit gutter contains marker indicating checking progress
• stop button in jEdit toolbar to gracefully kill MMT processing of file
• LaTeX-MMT integration works, see self-documenting example.pdf in latex-mmt
• extensions can now add productions to the syntax of the MMT shell
• various technical improvements and fixes

11th Git Release

• implemented a Jupyter Kernel based on MMT
  • updated MMT REPL Extension
• added Viewfinder
• moved Dockerfile into main repository and enabled automatic builds
• updated setup to be able to be run in automated scenarios
• TGView updates
  • Added Redo-Button
  • Allow locking of nodes together
  • Added local graph editing
  • Added show/hide nodes manually
  • Added Show/Hide/Select nodes/edges by node-/edge-type
  • Added Save graph as JSON
• added importer for IMPS files
• minor improvements and bug fixes

10.1 Release

This release is smaller than previous releases and mainly contains various bugfixes for use throughout the semester.

• added an MMT-specific context menu to jEdit
• an MMT Docker Container is now available at kwarc/mmt on DockerHub
• Deprecation of old delimiters and LF Arrows
  • systematic replacement across all existing archives
• TGView minor improvements
• numerous bugfixes and cleanup

10th Git Release

This release is much more substantial than previous releases, including major new features, the promotion of several previously experimental features to official ones, and numerous fixes of minor issues that had accumulated over time.

• complete overhaul of
  • strucuture level elaboration and type checking
  • handling of structure declarations in theories and morphisms
  • handling includes of parametric theories
• support for theory expressions (see MMT/examples)
• smarter type inference for defined, untyped constants
• simplifier now supports definition expansion (optionally)
• new lexing rule for flexible string interpolation (see MMT/examples for strings and quotation)
• TGView improved
  • allow sharing graphs via email, facebook, twitter, etc.
  • allow downloading as json and embedding in HTML
  • can upload custom graphs as json
• jEdit improvements
  • display of elaborated declarations in sidekick
  • display of rendered expressions as tooltips in sidekick
  • more precise highlighting of errors
  • jEdit action for normalization of the selected expression (bound to CS-N by default)
• travis test improvements
  • addition of proper test structure
  • cleaned up tests for API and LF
  • added alignment tests
  • preliminary co-versioning of archives and MMT system
• cleanup of localmh functionality
  • replaces previous oaf shell action
  • now possible to install multiple archives at once
• dependency Updates
  • upgrade sbt to 1.1.1
  • upgrade Scala to 2.12
  • upgrade tiscaf
  • remove non-funcational plugins: GuidedTours, leo
• proper versioning of MMT within sbt
• use the MMT logo within the webserver
• re-styling and documentation cleanup
• lots of bugfixes and cleanup

10beta2 Release

The upcoming release contains a wide range of new functionality as well as mature versions of existing experimental functionality.
Therefore, we're making another beta release to allow for more rigorous testing.

Users working with existing content that we have not fully adapted yet should wait for the proper release.
For everybody else, this version is recommended.

10beta Release

This is the latest release and marked as beta (see below). This is fine for casual users who want to sample MMT. Regular users probably want to wait for the proper release.

It migrates to Scala 2.12 and supports almost all of the recent language features used in the urtheories and examples repositories.

We're marking this as a beta release because we got a bit bogged down by FLoC deadlines last week and haven't had time yet to run the usual tests and fully merge the development branch into master.

This release is fine for casual users, who want to sample MMT.
Regular users may want to wait for the proper release.