26th Git Release

• Core
  • new relational database using rdf4j based on the Upper Library Ontology
• sTeX
  • various quality of life improvements, compatibility with sTeX 3.4
• MathWebSearch: updated MMT's MWS API to new implementation
• improvements to VS code plugin
• libraries: ATP support via TPTP in LATIN, in particular for DHOL

25th Git Release

• Core
  • command archive new FOLDER creates a new archive
  • . in build commands refers to current archive
  • better messages in setup dialog to help avoid common problems
  • removed certain URLDecoder uses that were not supported by all JDKs
• sTeX
  • integrated (upcoming) release for RusTeX with significantly improved optics and CSS styling
• other components
  • new MMT extension for Visual Studio Code: allows syntax highlighting, typechecking, and building MMT formalizations within Visual Studio Code
  • new Aldor importer in collaboration with Stephen Watt

24th Git Release

• Core
  • added support for structures defined by morphisms
  • various bug fixes regarding morphisms
  • further maturation of computation algorithm
• jEdit
  • one-step only normalization function
• sTeX
  • complete redesign
  • automatically keeps RusTeX up to date
  • improvements for LSP and the IDE
  • redesigned presentation of sTeX-originated OMDoc, integrated as OMDoc tab in the preview window of the IDE
  • improved error viewer in the IDE
  • co-release with the IDE and sTeX version 3.3 on CTAN
• other components
  • new Lean importer

23rd Git Release

• Administrative
  • preparation for a future upgrade to Scala 3
  • fixed many deprecation warnings
• Core system
  • new support for imperative computation akin to type-checking
  • experimental support for interactive theorem proving via Sven Wille's MSc thesis
  • extended support for theorem proving via Leo by Colin Rothgang's MSc work building on Luca Wolff's BSc work
• sTeX
  • major extensions
  • integrated improved document viewer (see here)
  • improved sandboxing for RusTeX
  • improvements for LSP and the IDE
  • co-release with the IDE and sTeX version 3.2 on CTAN
• Other components
  • Isabelle: upgrade to Isabelle2021-1
• LATIN2 library (separate repository, co-released)
  • various extensions and improvements
  • monads and collection data types by Moritz Blöcher's BSc thesis
  • new dependently-typed higher-order logic as developed by Colin Rothgang's MSc thesis
  • new support for programming language features by Alexander Mattick's MSc project
  • case study on realms, in particular topology by Franziska Weber's BSc side project

22nd Git Release

• Administrative
  • MMT now co-released with LATIN logic library maintained at https://gl.mathhub.info/MMT/LATIN2
    • master branch of UniFormal/MMT can be used to build master branch of MMT/LATIN2
    • together with MMT/urtheories, this forms MMT's standard library
  • Complete redesign of CI on github: CI now clones and builds MMT/urtheories, MMT/examples, and MMT/LATIN2
  • clean up of committed IntelliJ project files (no more *.iml files, some useful machine-independent files in .idea committed)
  • deleted a few long-deprecated sub-projects
  • deleted lots of deprecated or obsolete code in mmt.api
• Core system
  • new :file command for running a build file and reporting errors as an exit code
  • :setup command now clones and builds the 3 core archives (see CI)
  • major improvements to error handling and processing
  • solver: type checking of function applications now checks return type to make better use of expected type
  • simplifier: properly handles equality of literals
  • many bugfixes, minor improvements regarding all components involved in building, most importantly type-checking
• Core language
  • experimental support for diagram operators: major API clean up, lots of new documentation (see Navid Roux's upcoming MSc thesis)
  • type checker: generic support for proof gaps to be solved by external provers (see Luca Wolff's upcoming BSc thesis, which builds such a prover)
  • extended the LaTeX symbol list for editor autocomplete by Fraktur and Hebrew alphabets and various math symbols
  • new excusable errors representing gaps in developments (non-total views, unresolved _s, etc.), which are reported as errors but can be ignored for testing
• Plugins and other non-core components
  • jEdit:
    • support upgraded for jEdit 5.6 and latest versions of all plugins (except ErrorList where 2.4.0 causes an issue)
    • improved syntax highlighting: colors of symbols now set by plugin instead of jEdit mode
  • sTeX:
    • complete reimplementation to accomodate sTeX 3.x
    • sTeX -> xhtml and xhtml -> omdoc importers
    • dedicated sTeX browser and viewer for the generated xhtml
    • First steps towards guided tours
    • LSP Server for sTeX
  • Mizar: full reimplementation of the importer
    • CICM 2021 best system paper award, see https://kwarc.info/people/frabe/Research/RKR_mizar_21.pdf
    • compatible withMizar's new XML files
    • improved maintainability
    • translating some previously untranslated content, like registrations and (partially) proofs
  • ELPI: bugfixes in generator, lowercase variable names now produce proper uppercase Prolog variables
  • MathHub: minor improvements
    • performance and stability improvements for larger archives
    • improved display of STeX Glossary Entries
  • FrameIT
    • fix of a longstanding bug that previously put a limit on how much players (e.g., of the Unity frontend) can interact with FrameIT

21st Git Release

• Scala version increased to 2.13.4
• Syntax Presenter: component in MMT reconstructing MMT surface syntax from in-memory content of MMT knowledge items
  • various fixes to now output well-indented and parsable MMT syntax
  • added SytaxPresenterServer (see the :syntax server extension for screenshots and usage)
• Diagram Operators: operators acting on diagrams of MMT theories and views, and outputting new diagrams
  • based on accepted paper Structure-Preserving Diagram Operators by Navid Roux and Florian Rabe
  • implemented general framework
  • implemented operators:
    • universal algebra: Hom, Sub, and Cong from universal algebra, which take diagrams of SFOL-theories as input (e.g. the algebraic hierarchy consisting of Magma, Monoid, Group, ...) and output the diagram enriched with theories for homomorphisms, substructures, and congruences, respectively, for all input theories, respectively (see output diagram here)
    • an operator to perform theory intersections along (partial) views for refactoring purposes: see here.
• FrameIT Project
  • big performance improvements of the FrameIT MMT Server
  • several minor bug fixeserf improvements

20th Git Release

• administrative
  • sbt version increased to 1.3.13
  • move from Travis CI to GitHub Actions
• core language and API features
  • many improvements for diagram operators
  • parser now supports block notations, within which names are preserved
  • overhaul of parsing
  • misc. bugfixes and improvements in the build system
• integration with sTeX
  • add a standalone localpaths build target.
  • fix spurious sms dependency cycles
• use of MMT in FrameIT
  • almost complete refactoring to make the FrameIT MMT server less dependent on user formalizations
• use of MMT in GLF/GLIF
  • much work on the ELPI generation code
  • various improvements for GLF/GLIF (integer support, elpi generation, ...)

19th Git Release

• language features
  • improvements for diagram operators
    • fixes and extensions to anonymous theories, links, diagrams
    • several new operators including PUSHOUT ?thy ALONG ?view (MMT/urtheories) and logic-specific operators (MMT/LATIN2)
• user interfaces
  • IntelliJ-MMT plugin v19
    reconstruction of MMT surface syntax for in-memory theories, e.g. theories created by diagram operators on-the-fly, docs & screenshots here
• external systems and libraries
  • first proper release of logic library MMT/LATIN2 (master branch builds relative to this release)
  • new release of Isabelle export (Isabelle/b1f3e86a4745 from https://isabelle.sketis.net/repos/isabelle, AFP/429a712d7c4d from https://isabelle.sketis.net/repos/afp-devel)
  • GF: importer project mmt-gf merged into mmt-glf, various small improvements and fixes to GLF functionality
  • sTeX-OMDoc importer partially redesigned and improved

18th Git Release

• new language features
  • defined includes and realizations (akin to implementing interfaces), see the documentation
  • total keyword for structures
  • interpretation instruction declarations in documents allow changing the processing; currently used for namespace/import declarations, fixmeta keyword, document-global rule declarations
  • translation of notations along structures (qualifying the first delimiter with the structure name)
  • structural feature for inductive types and functions
• user interfaces
  • more abbreviations for Unicode characters and LaTeX commands, including ASCII art for Unicode characters (see the translation tables)
  • better display of infered types, implicit arguments, and normalized expressions; try hovering or the normalization action in jEdit
  • smarter name resolution to allow concrete syntax to refer to included constants
• implementation internals
  • completely rewritten handling of implicit morphisms to be more scalable for large highly-interrelated libraries (ideally not user-visible)
  • rewritten totality checking of views, total structures, realizations
• peripheral components and system integration
  • updates to Isabelle importer, now part of official Isabelle release, see Wenzel's blogpost
  • new exporter to ELPI that translates logic definitions into basic automated theorem provers for them, see the code and the example exports of the LATIN2 project
  • new project mmt-glf on merging GF and LF
• to co-released content
  • new reference project: LATIN2 is the most modern form the MMT logic library defined in (extensions of) LF
  • notations for proof rules that mimic declarative proof languages
  • new formalizations of various state-of-the-art logics including CTT_QE, MAM, Sedel
• finished IMPS-importer
• basics of an LSP Language Server
• some improvements for MitM
• Coq import reimplemented

17th Git Release

• Overhaul of mmt-stex machinery
  • Interface is stable
  • Bug fixes & performance improvements
• Minor REPL Server Improvements
• Improvements to GAP support
• mbgen improvements
  • added basic support for datasets that build on other datasets
  • metadata support for sql
• Improvements to Isabelle
• Jupyter Server Bugfixes