Skip to content

22nd Git Release
Compare
Choose a tag to compare
@Jazzpirate Jazzpirate released this 04 May 20:13
· 434 commits to master since this release
v22.0.0
bed907f
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
  • 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
    • 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
Assets 3
Loading