From 60789d815b2b9af6a541e4fa279ada5a4359ffe2 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:20 +0200 Subject: [PATCH 01/31] Update index.md --- doc/applications/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/applications/index.md b/doc/applications/index.md index f6a4110..7435c7d 100644 --- a/doc/applications/index.md +++ b/doc/applications/index.md @@ -18,7 +18,7 @@ In particular, these include The [MMT API](../api) based on MMT provides a number of knowledge management services including * notation-based presentation, -* interactive web-browisng, +* interactive web-browsing, * MMT-aware databases with custom indexing and retrieval, * project-based abstraction and work flows for building, distribution, and sharing, * management of change, From e0818203e5de43bd761b8d01222a3262a96fced1 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:22 +0200 Subject: [PATCH 02/31] Update index.md --- doc/applications/intellij/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/applications/intellij/index.md b/doc/applications/intellij/index.md index e183591..ad39f5f 100644 --- a/doc/applications/intellij/index.md +++ b/doc/applications/intellij/index.md @@ -3,7 +3,7 @@ layout: doc title: IntelliJ-MMT Plugin --- -[IntelliJ IDEA](https://www.jetbrains.com/idea/) is a multi-purpose Java-based IDE. An **MMT plugin** adds functionality to deal with MMT sourecs. It serves the usual features of "language plugins": +[IntelliJ IDEA](https://www.jetbrains.com/idea/) is a multi-purpose Java-based IDE. An **MMT plugin** adds functionality to deal with MMT sources. It serves the usual features of "language plugins": - syntax highlighting - type checking From a1a1f6720d9766419b1baedc4b850e72781b233a Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:24 +0200 Subject: [PATCH 03/31] Update installation.md --- doc/applications/intellij/installation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/applications/intellij/installation.md b/doc/applications/intellij/installation.md index b615a7c..e9c7af5 100644 --- a/doc/applications/intellij/installation.md +++ b/doc/applications/intellij/installation.md @@ -48,5 +48,5 @@ Since MMT files make heavy use of Unicode math charcters, be sure to have a font ### Notes on automatic type checking -- By default, the Plugin does **not** type check the terms of an open *mmt*-file, since doing so is computationally expensive and inconvenvient for the user. Type checking can be easily activated and deactivated in the *Errors* panel of the MMT tool window (View -> Tool Windows -> MMT) +- By default, the Plugin does **not** type check the terms of an open *mmt*-file, since doing so is computationally expensive and inconvenient for the user. Type checking can be easily activated and deactivated in the *Errors* panel of the MMT tool window (View -> Tool Windows -> MMT) - The *Document Tree* (on the left border of the IntelliJ-Window) only shows the syntax tree of the document that has been type checked last. To see the tree for the currently opened document, check the *Type Checking* checkbox in the *Errors* panel. Automatically navigating the syntax tree by caret position in the document can be turned on and off with the corresponding check box at the top of the *Document Tree* panel. From 4d9e172e710821e527f119592266d9fde1641c11 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:26 +0200 Subject: [PATCH 04/31] Update jedit.md --- doc/applications/jedit.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/applications/jedit.md b/doc/applications/jedit.md index 8628c9f..4410eed 100644 --- a/doc/applications/jedit.md +++ b/doc/applications/jedit.md @@ -52,7 +52,7 @@ This turns the system into a (very simple) interactive theorem prover. The type checker treats any occurrence of _ in MMT terms as a fresh unknown and tries to infer its value. This includes calling the (experimental and very weak) automated theorem prover of MMT. -If successful, the term is inserted into the internal syntax (as shown by Sidekick) but the _ remains in the soruce. +If successful, the term is inserted into the internal syntax (as shown by Sidekick) but the _ remains in the source. If the prove fails but the expected type of the subterm is found, a hole-term is introduced. In the latter case, the command introduce-hole can be used to replace _ with the hole-term in the source (e.g., in order to use auto-completion). From e5d5b1822ed740bfad8dff8f7aa3287be6ab3eeb Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:27 +0200 Subject: [PATCH 05/31] Update server.md --- doc/applications/server.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/applications/server.md b/doc/applications/server.md index 2028563..50f82cb 100644 --- a/doc/applications/server.md +++ b/doc/applications/server.md @@ -52,7 +52,7 @@ Some features are: * a *symbol* shows its full MMT URI as a tooltip. * a *variable* selects its declaration. * The *right-click menu* permits setting visibility options for the selected subexpression. - These show/hide parts of the expression that were infered by the system: + These show/hide parts of the expression that were inferred by the system: * *reconstructed types*: the omitted types of bound variables * *implicit arguments*: the omitted arguments to operator applications * *redundant brackets*: brackets that are not needed due to operator precedences From e56c636cd986c50d957de2b0e4a77c11cefd01c8 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:29 +0200 Subject: [PATCH 06/31] Update shell.md --- doc/applications/shell.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/applications/shell.md b/doc/applications/shell.md index e91b9f3..01bac86 100644 --- a/doc/applications/shell.md +++ b/doc/applications/shell.md @@ -12,7 +12,7 @@ Each subclass comes with scaladoc and can be best understood by browsing the kno The up-to-date context-free grammar for shell commands is part of the constructor parser in the companion object `Action` and can be best understood by reading the source code. ### ANSI Formatting in the MMT Shell -Some shell output uses [ANSI escapes](https://en.wikipedia.org/wiki/ANSI_escape_code) for highlighting. To display the formating, you can use [ansicon](https://github.com/adoxa/ansicon) for the windows console or [ansi console](https://web.archive.org/web/20200816075948/http://mihai-nita.net/2013/06/03/eclipse-plugin-ansi-in-console/) for the eclipse console. (Both are optional and very easy to install and use.) Unix shells should understand it natively. +Some shell output uses [ANSI escapes](https://en.wikipedia.org/wiki/ANSI_escape_code) for highlighting. To display the formatting, you can use [ansicon](https://github.com/adoxa/ansicon) for the windows console or [ansi console](https://web.archive.org/web/20200816075948/http://mihai-nita.net/2013/06/03/eclipse-plugin-ansi-in-console/) for the eclipse console. (Both are optional and very easy to install and use.) Unix shells should understand it natively. ### MMT Scripts An MMT script is a text file containing one shell command per line. (Empty lines are allowed, lines starting with // are ignored.) From fa8183bafed66d3c7d5266d3f5d1c06c659d46f5 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:30 +0200 Subject: [PATCH 07/31] Update tgview.md --- doc/applications/tgview.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/applications/tgview.md b/doc/applications/tgview.md index 8eb2a1e..cfc29ff 100644 --- a/doc/applications/tgview.md +++ b/doc/applications/tgview.md @@ -2,7 +2,7 @@ layout: doc title: TGView (the MMT Theory Graph viewer) --- -TGView is a brower-based theory graph viewer based on the [VisJS](http://visjs.org/) +TGView is a browser-based theory graph viewer based on the [VisJS](http://visjs.org/) network library. The code is [available on GitHub](https://github.com/UniFormal/TGView), and a [MathHub instance](http://mmt.mathhub.info/graphs/tgview) gives visual access to the MathHub archives as interactive theory graphs. From 262958a5c1ad45f0fab32443264c7905db650579 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:32 +0200 Subject: [PATCH 08/31] Update building.md --- doc/archives/building.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/archives/building.md b/doc/archives/building.md index 86ac99d..693b1fa 100644 --- a/doc/archives/building.md +++ b/doc/archives/building.md @@ -10,7 +10,7 @@ MMT can be used as a build tool using a special [shell command](../applications/ ### Defining Build Targets The collection of build targets is maintained by the [extension manager](../api/extensions/). New build targets are defined by implementing the [`archives.BuildTarget`](apidoc://info.kwarc.mmt.api.archives.BuildTarget) class. -Build target modfiers and change management are supported for automatically for every build target. +Build target modifiers and change management are supported for automatically for every build target. ### Build Target Modifiers From ffae533f50d18bf74aa16fae7ab2be72a5c5140a Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:33 +0200 Subject: [PATCH 09/31] Update lmh.md --- doc/archives/Mathhub/lmh.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/archives/Mathhub/lmh.md b/doc/archives/Mathhub/lmh.md index f37f8ee..6ea1795 100644 --- a/doc/archives/Mathhub/lmh.md +++ b/doc/archives/Mathhub/lmh.md @@ -35,7 +35,7 @@ LMH also allows installing a specific branch of an archive. The syntax for this lmh install @ -Archvies are versioned using git. +Archives are versioned using git. A version of an archive can be a branch name or a git commit hash (Technically anything that is a ref in git). When a non-existing version of the archive is specified, lmh will display a warning message and then fall back to the default version. If `lmh install` with a specific version is called on an archive that is already installed, it will make sure to update to the specified version. From f1ee3bd5819cf108cc1831240bd828d1ee845810 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:35 +0200 Subject: [PATCH 10/31] Update meta_inf.md --- doc/archives/meta_inf.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/archives/meta_inf.md b/doc/archives/meta_inf.md index a54592e..e4b6b7c 100644 --- a/doc/archives/meta_inf.md +++ b/doc/archives/meta_inf.md @@ -20,5 +20,5 @@ narration-base | the URI prefix prepended to the file paths inside the archives source, content, narration, relational | custom folder names for specific dimensions (see the [build tool](building) for details) ns | the default namespace of the archive used for all files that do not declare a namespace ns-PREFIX | a namespace binding for PREFIX that is in effect for all files in the archives (unless a file redefines the prefix) -dependencies | comma-seperated dependencies for the archive in question. Every archive implicitly has an additional dependency on the 'meta-inf' archive of its group even if it is not listed. For example on MathHub (to which the concepts also apply to), the archive [MitM/Foundation](https://gl.mathhub.info/MitM/Foundation) has the implicit dependency [MitM/meta-inf](https://gl.mathhub.info/MitM/meta-inf). +dependencies | comma-separated dependencies for the archive in question. Every archive implicitly has an additional dependency on the 'meta-inf' archive of its group even if it is not listed. For example on MathHub (to which the concepts also apply to), the archive [MitM/Foundation](https://gl.mathhub.info/MitM/Foundation) has the implicit dependency [MitM/meta-inf](https://gl.mathhub.info/MitM/meta-inf). foundation | the (assumed to be common) **meta theory** for all modules in the archive. From 92d864e3b50444c92daaf7c452526827deb3067b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:37 +0200 Subject: [PATCH 11/31] Update contributing.md --- doc/development/contributing.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/development/contributing.md b/doc/development/contributing.md index 9882f7e..dab588f 100644 --- a/doc/development/contributing.md +++ b/doc/development/contributing.md @@ -73,7 +73,7 @@ There are two essential workflows: #### Updating the release branch -Before a release is made the version string stored in [src/mmt-api/resources/versioning/system.txt](https://github.com/UniFormal/MMT/blob/master/src/mmt-api/resources/versioning/system.txt) should be increased appropriatly. +Before a release is made the version string stored in [src/mmt-api/resources/versioning/system.txt](https://github.com/UniFormal/MMT/blob/master/src/mmt-api/resources/versioning/system.txt) should be increased appropriately. Once such a change has landed on master, when then again use pull requests to mark a version of MMT as a release. This time we merge from ```master``` onto ```release```. From d0dcf1784e1578fd5493554e835dbe67ac3f0722 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:39 +0200 Subject: [PATCH 12/31] Update releases.md --- doc/development/releases.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/development/releases.md b/doc/development/releases.md index 72d2241..04b278e 100644 --- a/doc/development/releases.md +++ b/doc/development/releases.md @@ -461,7 +461,7 @@ Released on [22nd February 2017](https://github.com/UniFormal/MMT/releases/tag/v * Initial version of Active Computation Extension * Improvements: * Update to Travis Build Scripts - * Webserver Improvements, including CORS support, hostname support, and client side libarary updates] + * Webserver Improvements, including CORS support, hostname support, and client side library updates] #### Release 4 From fac1e8952c60c32df73e0ad4f2cc053ea685f644 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:43 +0200 Subject: [PATCH 13/31] Update scala.md --- doc/development/scala.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/development/scala.md b/doc/development/scala.md index 9c9af0e..cf9297f 100644 --- a/doc/development/scala.md +++ b/doc/development/scala.md @@ -18,7 +18,7 @@ Configure your IDEs accordingly and do not change styling recklessly. All indentation must be by spaces (no tabs). The depth of indentation is not fixed. It is typically 2-4 spaces. -It does not have to be consistent throughtout a file. +It does not have to be consistent throughout a file. #### Imports From dcb4727060b4852d1b5054066f103ebd103840b2 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:47 +0200 Subject: [PATCH 14/31] Update declarations.md --- doc/language/declarations.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/language/declarations.md b/doc/language/declarations.md index 310590f..472008c 100644 --- a/doc/language/declarations.md +++ b/doc/language/declarations.md @@ -120,7 +120,7 @@ The syntax for structures is * Even though structures are declarations, they have a [module](modules) body and are thus delimited by the module [delimiter](delimiters) ![`\GS`](../img/GS.png) instead of the declaration delimiter ![`\RS`](../img/RS.png). * Simple includes are still delimited with ![`\RS`](../img/RS.png). * The name of each declaration in a structure has to correspond to the name of a declaration in the ``. -* Components (aliases, types, definitions etc.) explicitely given in a structure *override* the corresponding component of the declaration in the ``, all other components are inherited from the latter. In particular, structures can introduce definitions for (not necessarily) previously undefined constants, in which case the (new) definition has to have the (induced/old) type of the constant. It is recommended to *never override the type* of a symbol in a structure. If no component of a declaration is to be modified, it can be left implicit. In this case a fresh copy of the declaration is inherited. If such multiplication is not desired for some declarations, they can be assigned to a previously inherited version of the declaration. +* Components (aliases, types, definitions etc.) explicitly given in a structure *override* the corresponding component of the declaration in the ``, all other components are inherited from the latter. In particular, structures can introduce definitions for (not necessarily) previously undefined constants, in which case the (new) definition has to have the (induced/old) type of the constant. It is recommended to *never override the type* of a symbol in a structure. If no component of a declaration is to be modified, it can be left implicit. In this case a fresh copy of the declaration is inherited. If such multiplication is not desired for some declarations, they can be assigned to a previously inherited version of the declaration. * The full [URI](uris) of an induced declaration `` in a structure `` in a module `` is ` ? / `. It is this declaration, that is visible from the outside and can be used in subsequent (to the structure) declarations. In contrast, the URI ` / ? ` refers to the plain declaration as declared *directly in the structure*, i.e. without inheritance. The latter should never be used outside of the [API](../api) and is invisible to declarations outside of the structure. * Unlike simple includes, multiple *named structures* with the same `` are **not** redundant. Each structure introduces fresh (possibly modified) copies of the declarations in the domain. * The limit of the previous point is the [*meta theory*](modules.html#theories) of the domain. If two structures `s1`,`s2` have corresponding domains `dom1`,`dom2` with the same meta theory `meta`, then *everything in the dependency closure of `meta`* will be included exactly once. From 9e3529651f1f0c226c9bd3e7b35b3a2518ac48cd Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:52 +0200 Subject: [PATCH 15/31] Update implicit.md --- doc/language/implicit.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/language/implicit.md b/doc/language/implicit.md index 737ca3f..5870185 100644 --- a/doc/language/implicit.md +++ b/doc/language/implicit.md @@ -23,7 +23,7 @@ If there is an implicit morphism m from S to T, all names c of S can be used in Similarly, every morphism out of T can be treated as a morphism out of S by composing with m. This happens automatically, i.e., the user does not have to refer to m, hence the name *implicit* morphisms. -Of course, this only works if m is uniuqe, i.e., there may at most 1 implicit morphism between any two theories. +Of course, this only works if m is unique, i.e., there may at most 1 implicit morphism between any two theories. In other words, the subgraph of implicit morphisms must commute. A number of examples are given in the research paper on implicit morphisms. @@ -177,7 +177,7 @@ MMT flattens every include i of S in T and by composing it with every include in The order is relevant because the declarations included by i can already be used in the declarations between i and a later include with the same domain. There is one relaxation though. -If the later include i2 of R is primitve, it can often be dropped even if an earlier include i1 of R has a different kind or a definition. +If the later include i2 of R is primitive, it can often be dropped even if an earlier include i1 of R has a different kind or a definition. This is justified because: * If i2 is a realization, the promise of i2 is trivial because it has already been fulfilled by i1. * If i2 is a plain include and i1 already provides a definition m, dropping i2 amounts to implicitly instantiating all R-constants in the domain of i2 via m. From 0234c0fe2fad4f512f8b3ec061cea7bd178a20ef Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:53 +0200 Subject: [PATCH 16/31] Update index.md --- doc/language/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/language/index.md b/doc/language/index.md index 1fb63c0..b62a58e 100644 --- a/doc/language/index.md +++ b/doc/language/index.md @@ -5,7 +5,7 @@ title: The MMT Language This sections gives an overview of the **general language structure** of MMT. To be more concrete, it also explains one specific **concrete syntax**, which is the main syntax used to write MMT content natively. -A description of MMT's **abstract syntax** and the corrseponding internal data structures can be found [here](../api/syntax) +A description of MMT's **abstract syntax** and the corresponding internal data structures can be found [here](../api/syntax) MMT is a language for formal mathematics that pays special attention to [*foundation-independence*](../philosophy/independence), scalability, and modularity. MMT follows the [OMDoc](http://www.omdoc.org/) philosophy and will be integrated into the upcoming OMDoc 2 format. From f780acc0fbf7f6be96146605f3cc426b65dce060 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:56:56 +0200 Subject: [PATCH 17/31] Update inductive.md --- doc/language/inductive.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/language/inductive.md b/doc/language/inductive.md index 596df54..f6a81c0 100644 --- a/doc/language/inductive.md +++ b/doc/language/inductive.md @@ -5,7 +5,7 @@ title: Inductive Types ### Declaraing an inductive type -The structural feature **inductive** for inductive types can be used to elaborate to define (mutally) inductive types. A derived declaration for this features consists of: +The structural feature **inductive** for inductive types can be used to elaborate to define (mutually) inductive types. A derived declaration for this features consists of: * A name of the derived declaration * A list of parameters of the derived declaration (similar to theory parameters) @@ -13,7 +13,7 @@ The structural feature **inductive** for inductive types can be used to elaborat There are three types of internal declarations: -* Type-Level internal declarations declaring the (mutaully) inductively-defined types we want to define +* Type-Level internal declarations declaring the (mutually) inductively-defined types we want to define * The constructors of those types * Further outgoing termlevel declarations, i.e. for declaring additional properties of the inductive type @@ -34,8 +34,8 @@ Here we have a typelevel `` (of type ``), a constructor `` of ` Date: Sun, 16 Jun 2024 18:57:00 +0200 Subject: [PATCH 18/31] Update inductivedefinitions.md --- doc/language/inductivedefinitions.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/language/inductivedefinitions.md b/doc/language/inductivedefinitions.md index 732fc74..43a6682 100644 --- a/doc/language/inductivedefinitions.md +++ b/doc/language/inductivedefinitions.md @@ -24,7 +24,7 @@ The types of the internal declarations given here can also be automatically infe #### Elaboration of inductive definitions -Inductive definitions are elaborated to the following delarations: +Inductive definitions are elaborated to the following delirations: * A declaration of the specified inductively-defined function for each type inductively-defined by `` * A declaration axiomatizing the definition for each constructor case From d56197d80bd40dd107a08192bddabd55eb9ac195 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:03 +0200 Subject: [PATCH 19/31] Update informal.md --- doc/language/informal.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/language/informal.md b/doc/language/informal.md index 96a6254..8c6361d 100644 --- a/doc/language/informal.md +++ b/doc/language/informal.md @@ -2,6 +2,6 @@ layout: doc title: Flexiformal Knowledge --- -Currently, MMT concentrates on the formal subset of the [OMDoc](../philosophy/omdoc), which postulates that mathematatical knowledge should be represented [flexiformally](http://kwarc.info/kohlhase/papers/synasc13.pdf), i.e. with flexible formality. Foundational steps towards extending the structural core of MMT were taken in [Mihnea Iancu's PhD thesis](https://opus.jacobs-university.de/frontdoor/index/index/docId/721). The implementation is already very mature (and heavily used in our production workflows), but documentation has not been written yet. +Currently, MMT concentrates on the formal subset of the [OMDoc](../philosophy/omdoc), which postulates that mathematical knowledge should be represented [flexiformally](http://kwarc.info/kohlhase/papers/synasc13.pdf), i.e. with flexible formality. Foundational steps towards extending the structural core of MMT were taken in [Mihnea Iancu's PhD thesis](https://opus.jacobs-university.de/frontdoor/index/index/docId/721). The implementation is already very mature (and heavily used in our production workflows), but documentation has not been written yet. The bulk of flexiformalizations in the MMT world are generated from [sTeX](http://github.com/KWARC/sTeX), a semantics-enhanced version of LaTeX which can be [converted to](https://uniformal.github.io/doc/applications/stex) flexiformal MMT. Much of this content is hosted on [MathHub](http://mathhub.info). From 0cf1115e157c7ea056c25c7e7060c3c25e934f9b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:06 +0200 Subject: [PATCH 20/31] Update applications.tex --- doc/tutorials/slides/applications.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tutorials/slides/applications.tex b/doc/tutorials/slides/applications.tex index 4208f31..6e4d330 100644 --- a/doc/tutorials/slides/applications.tex +++ b/doc/tutorials/slides/applications.tex @@ -119,7 +119,7 @@ \section{Breadth of Possible Applications} Design: MMT as p MMT and jEdit \begin{itemize} - \item Plugin for jEdit that wraps arond MMT + \item Plugin for jEdit that wraps around MMT \item MMT and jEdit large projects \item But only little glue code needed \lec{mostly forwarding to MMT API functions} From e1e867fbb11d0a87e98836f8f8ebfa2ddb12b2b9 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:07 +0200 Subject: [PATCH 21/31] Update index.md --- doc/tutorials/prototyping/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tutorials/prototyping/index.md b/doc/tutorials/prototyping/index.md index 5dff0d8..e44093d 100644 --- a/doc/tutorials/prototyping/index.md +++ b/doc/tutorials/prototyping/index.md @@ -9,7 +9,7 @@ The complete files built interactively in this tutorial can be found at https:// It assumes that * MMT has been [installed](../../setup), -* archives are placed in some folder, which is refered to as `CONTENT`,The MMT installer should take care of this +* archives are placed in some folder, which is referred to as `CONTENT`,The MMT installer should take care of this * [jEdit](../../applications/jedit) is used for editing mmt files.Other editors will work but might make editing awkward. ### Define a Meta-Logic From ab2b71354003be758b75e399852e42af4618b6a9 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:09 +0200 Subject: [PATCH 22/31] Update 4natded.md --- doc/tutorials/jedit/4natded.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/tutorials/jedit/4natded.md b/doc/tutorials/jedit/4natded.md index f26e15a..5f872e3 100644 --- a/doc/tutorials/jedit/4natded.md +++ b/doc/tutorials/jedit/4natded.md @@ -29,19 +29,19 @@ Since we use judgments-as-types, these three rules correspond to the following t ![`\vdash A \wedge B \to \vdash A`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20A) ![`\vdash A \wedge B \to \vdash B`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20B) -Noticably, the function arrows in these types lend themselves to be interpreted just like implications: We can read e.g. the first rule as +Noticeably, the function arrows in these types lend themselves to be interpreted just like implications: We can read e.g. the first rule as > If `A` is provable, then (if `B` is provable, then `A∧B` is provable). This is no coincidence - this correspondence between a logical connective and a type constructor is known as *Curry-Howard-Isomorphism* (or *propositions-as-types*), and we will (rather trivially) prove this isomorphism later in MMT using [views](../../language/modules.html#views). -However, the types above don't quite work in LF, for the simple reason, that `A` and `B` are free variables. The proof rules are valid for *any* propositions `A`, `B`, so to avoid them being free variables, we can instead declare a *function* that takes two proposition `A`,`B` and returns the functions corresponding to the rules. For that, we finally need the dependend function types: +However, the types above don't quite work in LF, for the simple reason, that `A` and `B` are free variables. The proof rules are valid for *any* propositions `A`, `B`, so to avoid them being free variables, we can instead declare a *function* that takes two proposition `A`,`B` and returns the functions corresponding to the rules. For that, we finally need the dependent function types: ![`\prod_{A:prop}\prod_{B:prop}\vdash A \to \vdash B \to \vdash A\wedge B`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cprod_%7BA%3Aprop%7D%5Cprod_%7BB%3Aprop%7D%5Cvdash%20A%5C%3B%20%5Cto%5C%3B%20%5Cvdash%20B%5C%3B%5Cto%5C%3B%5Cvdash%20A%5Cwedge%20B) ![`\prod_{A:prop}\prod_{B:prop}\vdash A \wedge B \to \vdash A`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cprod_%7BA%3Aprop%7D%5Cprod_%7BB%3Aprop%7D%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20A) ![`\prod_{A:prop}\prod_{B:prop}\vdash A \wedge B \to \vdash B`](https://latex.codecogs.com/gif.latex?%5Cinline%20%5Cprod_%7BA%3Aprop%7D%5Cprod_%7BB%3Aprop%7D%5Cvdash%20A%5Cwedge%20B%5C%3B%20%5Cto%5C%3B%5Cvdash%20B) -Again, noticably, the dependent functions here lend themselves to be read like a "for all" - e.g. we can read the first rule as +Again, noticeably, the dependent functions here lend themselves to be read like a "for all" - e.g. we can read the first rule as > For all `A:prop`, for all `B:prop`: If `A` is provable, then (if `B` is provable, then `A∧B` is provable). From ca820e96c165c396f08340b3696bc49dbc90f0ac Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:10 +0200 Subject: [PATCH 23/31] Update 3LF.md --- doc/tutorials/jedit/3LF.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tutorials/jedit/3LF.md b/doc/tutorials/jedit/3LF.md index a434550..fffa987 100644 --- a/doc/tutorials/jedit/3LF.md +++ b/doc/tutorials/jedit/3LF.md @@ -64,7 +64,7 @@ The last point is worth looking at more closely: Usually, proof rules are denote In the case of propositional logic, we have a single judgment for every proposition `φ:prop`, namely the judgment `⊦ φ` that `φ` holds. Correspondingly, we declared the function `proof`, that maps a proposition `φ` to the associated type of proofs `⊦ φ`. The syntax we have already taken care of, by declaring the connectives as functions on the type `prop`. -In the next section we will use dependend function types to implement the rules of the *natural deduction* calculus as functions, that yield elements of the proof types `⊦ φ`. +In the next section we will use dependent function types to implement the rules of the *natural deduction* calculus as functions, that yield elements of the proof types `⊦ φ`. ------------------------------- From 8bfa1956bcdbf1916dcb45a50c3e627faec0cf54 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:11 +0200 Subject: [PATCH 24/31] Update running.md --- doc/setup/running.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/setup/running.md b/doc/setup/running.md index 13a93cb..c1fb22a 100644 --- a/doc/setup/running.md +++ b/doc/setup/running.md @@ -62,7 +62,7 @@ The `deploy` folder contains shell scripts that automate running from these smal * `mmt` (for Unix) and `mmt.bat` (for Windows): executes MMT commands and/or opens an [MMT shell](../applications/shell), `mmt -help` displays the available options * `run-file.bat`: a convenience script for Windows that can be associated with MMT shell scripts. -Users may wish to add the deploy folder to the PATH enviroment variable. +Users may wish to add the deploy folder to the PATH environment variable. #### Running from Classes From b14ec1db82f029363286d459ffd13b4e93a017b1 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:13 +0200 Subject: [PATCH 25/31] Update repo.md --- doc/setup/repo.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/setup/repo.md b/doc/setup/repo.md index 59e3659..d51b04a 100644 --- a/doc/setup/repo.md +++ b/doc/setup/repo.md @@ -11,7 +11,7 @@ The content of the subdirectories is as follows: Their status is somewhat between release and nightly build: I commit new builts frequently, and they are usually stable. The subfolders are * `main`: all jar files of MMT projects - * `lib`: all jar files that MMT depends on, including the Scala library The only extenal dependency is the JVM itself. For most parts, Java 6 is fine; occassionally Java 7 is needed. The run scripts automatically put all necessary jars on the Java classpath. + * `lib`: all jar files that MMT depends on, including the Scala library The only extenal dependency is the JVM itself. For most parts, Java 6 is fine; occasionally Java 7 is needed. The run scripts automatically put all necessary jars on the Java classpath. * `lfcatalog`: the jar files of the LF catalog, to be used with Twelf * `jedit-plugin`: all jar and other files needed for the plugin for jEdit * `src/`: All sources. From 4a427d04be3b08c87b1d81f2fec4d945f3e8c431 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:16 +0200 Subject: [PATCH 26/31] Update docker.md --- doc/setup/docker.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/setup/docker.md b/doc/setup/docker.md index 673e2b4..447714d 100644 --- a/doc/setup/docker.md +++ b/doc/setup/docker.md @@ -15,7 +15,7 @@ To start a temporary container with permanent volume for MMT content, use: ``` This will run the newest MMT.jar and store all archives inside a new volume called mmt mounted under `/content/`. -The command can be run multiple times to (re-)start the container if neccessary. +The command can be run multiple times to (re-)start the container if necessary. ### Storage From 39bb6d8f7046a1f2cfeffbc448457564f882b938 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:18 +0200 Subject: [PATCH 27/31] Update devel.md --- doc/setup/devel.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/setup/devel.md b/doc/setup/devel.md index 5629185..3ef3409 100644 --- a/doc/setup/devel.md +++ b/doc/setup/devel.md @@ -3,7 +3,7 @@ layout: doc title: Developing MMT --- -For developing and building MMT, it is recommened to use IntelliJ IDEA or Eclipse. +For developing and building MMT, it is recommended to use IntelliJ IDEA or Eclipse. Furthermore, a working installation of `sbt` is required. ### Using IntelliJ IDEA From 06c326bbf72fa42b66534b1c494a0a8741fd27fb Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:20 +0200 Subject: [PATCH 28/31] Update configure.md --- doc/setup/configure.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/setup/configure.md b/doc/setup/configure.md index c22c430..02d81ee 100644 --- a/doc/setup/configure.md +++ b/doc/setup/configure.md @@ -11,7 +11,7 @@ When started, MMT looks for a configuration file called `mmtrc` in the following Later configuration entries overwrite earlier ones. -During setup a defaut configuration file is generated and placed in the `deploy` folder. +During setup a default configuration file is generated and placed in the `deploy` folder. That file also includes some example configuration entries. ### Configuration File Syntax From 4af0422ceee5e95da06241fd192928dc81694f0c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:21 +0200 Subject: [PATCH 29/31] Update papers.md --- doc/philosophy/papers.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/philosophy/papers.md b/doc/philosophy/papers.md index b168fda..a315bb8 100644 --- a/doc/philosophy/papers.md +++ b/doc/philosophy/papers.md @@ -18,7 +18,7 @@ Most relevant papers can be found in Florian Rabe's [publication list](https://k There is also an [entry](http://swmath.org/software/7136) for MMT in the swMath catalog of mathematical software. -* M. Kohlhase, F. Mance, F. Rabe, [A Universal Machine for Biform Theory Graphs](http://kwarc.info/frabe/Research/KMR_uom_13.pdf) - biform theories (deduction and computatiton) in MMT with a practical integration of MMT and Scala (published at CICM 2013) +* M. Kohlhase, F. Mance, F. Rabe, [A Universal Machine for Biform Theory Graphs](http://kwarc.info/frabe/Research/KMR_uom_13.pdf) - biform theories (deduction and computation) in MMT with a practical integration of MMT and Scala (published at CICM 2013) * D. Ginev, M. Iancu, F. Rabe, [Integrating Content and Narration-Oriented Document Formats](http://kwarc.info/frabe/Research/GIR_mmtlatex_13.pdf) - an integration between MMT and LaTeX * M. Iancu, M. Kohlhase, [Searching the Space of Mathematical Knowledge](http://www.cicm-conference.org/2012/mir/mir2012_submission_5.pdf) - this application uses MMT to generate smart search indices that include inherited and computed knowledge (published at MIR 2012) * M. Iancu, F. Rabe, [Work-in-progress: An MMT-Based User-Interface](http://kwarc.info/frabe/Research/IR_ui_12.pdf) - a summary of the state of editing in MMT (published at UITP 2012) From 5c7dd6ba48c46747b9954ea3533deee1f1abf5f2 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:25 +0200 Subject: [PATCH 30/31] Update independence.md --- doc/philosophy/independence.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/philosophy/independence.md b/doc/philosophy/independence.md index e975fc7..1700667 100644 --- a/doc/philosophy/independence.md +++ b/doc/philosophy/independence.md @@ -12,6 +12,6 @@ MMT is an API and as such not committed to particular applications. The MMT system includes several [MMT-based applications](../applications/) that yield, e.g., [build tools](../archives/building) for [MMT archives](../archives), a [jEdit-based text editor](../applications/jedit), or a [web server](../applications/server) for MMT content. ### Logic Independence -MMT is logic-independent, i.e., it is not commited to a particular logic. +MMT is logic-independent, i.e., it is not committed to a particular logic. Therefore, MMT users have to define their logic in MMT or import a logic defined by someone else. MMT beginners should check out the [MMT archive](../archives) [urtheories](https://gl.mathhub.info/MMT/urtheories). This archive defines several basic languages, in particular the logical framework [**LF**](https://en.wikipedia.org/wiki/Logical_framework#LF). Other archives can be found at [OAF](../archives/oaf) From 0ceb988f6d9dbff6ae09c1bdee12e98f6dd78b89 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 16 Jun 2024 18:57:26 +0200 Subject: [PATCH 31/31] Update modules.md --- doc/language/modules.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/language/modules.md b/doc/language/modules.md index 78e40d0..401242c 100644 --- a/doc/language/modules.md +++ b/doc/language/modules.md @@ -20,13 +20,13 @@ Theories can be *nested*, like this: ![`theory : = theory : = \GS \GS`](../img/nestedtheory.png) -in which case the visible context of both the inner theory as well as `` is ``, i.e. the inner theory can see all previous declarations of the outer theory, but at no point can the outer theory see inside the inner theory (unless explicitely [included](declarations.html#structures)). +in which case the visible context of both the inner theory as well as `` is ``, i.e. the inner theory can see all previous declarations of the outer theory, but at no point can the outer theory see inside the inner theory (unless explicitly [included](declarations.html#structures)). ### Views Given two theories `A` and `B`, a **view** from `A` to `B` maps all [declarations](declarations) in `A` to expressions over symbols in `B`, while preserving *typing judgments*. i.e. if `|- a : tpA` in `A` and `v:A->B` is a view, then `|- v(a) : v(tpA)`. Hence, views are *truth preserving*. `A` is the *domain* of `v` and `B` is the *codomain*. -Their conrete syntax is +Their concrete syntax is ![`view : -> = \GS`](../img/view.png)