Merge pull request #473 from UniFormal/devel

Release 17

.gitignore

@@ -27,6 +27,8 @@ scripts/travis/deploy_key
 # IntelliJ Failes
 .idea
 .idea_modules
+*.iml
+
 
 # Eclipse Files
 bin

Test/build.sbt

@@ -0,0 +1,12 @@
+import sbt.Keys.libraryDependencies
+
+lazy val mmt = RootProject(file("C:/mmt2/MMT/src"))
+
+lazy val playground = Project(id = "playground", base = file(".")).settings(
+  name := "playground",
+  version := "0.1",
+  scalaVersion := "2.12.8",
+  scalacOptions in ThisBuild ++= Seq("-unchecked", "-deprecation"),
+  // Add further desired libraryDependencies here
+  // e.g. libraryDependencies += "org.jgrapht" % "jgrapht-core" % "1.3.0",
+).dependsOn(mmt).aggregate(mmt)

Test/project/build.properties

@@ -0,0 +1 @@
+sbt.version = 1.2.8

src/Semantic-Computer/Semantic-Computer.iml

@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="true">
+    <exclude-output />
+    <content url="file://$MODULE_DIR$">
+      <sourceFolder url="file://$MODULE_DIR$/src" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="library" name="scala-sdk-2.12.8 (2)" level="application" />
+  </component>
+</module>

src/build.sbt

@@ -41,7 +41,7 @@ lazy val mmtMainClass = "info.kwarc.mmt.api.frontend.Run"
 // =================================
 // GLOBAL SETTINGS
 // =================================
-scalaVersion in Global := "2.12.3"
+scalaVersion in Global := "2.12.8"
 scalacOptions in Global := Seq(
   "-feature", "-language:postfixOps", "-language:implicitConversions", "-deprecation",
   "-Xmax-classfile-name", "128", // fix long classnames on weird filesystems
@@ -216,7 +216,7 @@ lazy val lf = (project in file("mmt-lf")).
   dependsOn(lfcatalog).
   settings(mmtProjectsSettings("mmt-lf"): _*).
   settings(
-    //    libraryDependencies += "org.scala-lang" % "scala-parser-combinators" % "2.12.3" % "test",
+    //    libraryDependencies += "org.scala-lang" % "scala-parser-combinators" % "2.12.8" % "test",
   )
 
 // =================================

src/frameit-mmt/src/FrameIT.scala

@@ -78,7 +78,6 @@ class FrameViewer extends Extension {
 class FrameitPlugin extends ServerExtension("frameit") with Logger with MMTTask {
 
   override val logPrefix = "frameit"
-  val test : Class[FrameViewer] = classOf[FrameViewer]
   lazy val fv = controller.extman.get(classOf[FrameViewer]).headOption.getOrElse {
     val a = new FrameViewer
     controller.extman.addExtension(a)
@@ -199,7 +198,7 @@ class FrameitPlugin extends ServerExtension("frameit") with Logger with MMTTask
     controller.extman.addExtension(ret)
     ret
   }
-  implicit val ce : CheckingEnvironment = new CheckingEnvironment(controller.simplifier,ErrorThrower,RelationHandler.ignore, this)
+  implicit lazy val ce : CheckingEnvironment = new CheckingEnvironment(controller.simplifier,ErrorThrower,RelationHandler.ignore, this)
 
   val dpath = DPath(URI.http colon "cds.omdoc.org") / "FrameIT"
   val sitpath = dpath ? "situation_theory"

src/latex-mmt/paper/conc.tex

@@ -1,6 +1,6 @@
 We have presented a system that allows embedding formal \mmt content inside \latex documents.
 The formal content is type-checked in a way that does not affect any existing \latex work flows and results in higher quality \latex than could be easily  produced manually.
-Moreover, the formal content may use and be used by any \mmt content formalized elsewhere, which allows the interlinking across document formats.
+Moreover, the formal content may use and be used by any \mmt content formalized elsewhere, which allows interlinking across document formats.
 
 Of course, we are not able to verify the informal parts of a document this way --- only those formulas that are written in \mmt syntax are checked.
 But our design supports both gradual formalization and parallel formal-informal representations.
@@ -11,4 +11,4 @@
 It is intriguing to apply the same technology to formal proofs.
 This is already possible for formal proof terms, but those often bear little resemblance to informal proofs.
 Once \mmt supports a language for structured proofs, that could be used to write formal proofs in \mmttex.
-Morever, future work could apply \mmt as a middleware between \latex and other tools, e.g., \mmt could run a computation through a computer algebra to verify a computation in \latex.
+Morever, future work could apply \mmt as a middleware between \latex and other tools, e.g., \mmt could run a computation through a computer algebra system to verify a computation in \latex.

src/latex-mmt/paper/intro.tex

@@ -3,10 +3,14 @@
 
 A major open problem in mathematical document authoring is to elegantly combine formal and informal mathematical knowledge.
 Multiple proof assistants and controlled natural language systems have developed custom formats for that purpose, e.g., \cite{isabelle_documentoriented,mizar,plato,naproche}.
+Other languages $L$ allow for integrating \latex into $L$-source files in a literate programming style (e.g., lhs2tex\footnote{\url{https://www.andres-loeh.de/lhs2tex/}} for Haskell) or for integrating $L$-source chunks into \latex files (e.g., SageTeX\footnote{\url{https://github.com/sagemath/sagetex}} for SageMath).
+The design of \mmttex is close to the latter, i.e., to combine \mmt and \latex sources.
+
 %Mizar's document format \cite{mizar} has always been designed to closely resemble common narrative mathematical language.
 %Recent work for Isabelle opens up the Isabelle kernel in order to permit better integration with other applications, in particular document-oriented editors\cite{isabelle_documentoriented}.
 %%\cite{largeformalwikis} develops a general Wiki infrastructure that can use Mizar and Coq as verification backends.
-%In the Plato system \cite{plato}, TeXMacs is used as a document-oriented frontend whose documents are parsed and verified by the Omega proof assistant.
+%In the Plato system \cite{plato}, TeXMacs is used as a document-oriented frontend whose documents are parsed and verified by a proof assistant.
+
 %Also, several proof assistants can export a {\LaTeX} version of their native input language (e.g., Isabelle and Mizar).
 %Similarly, most can export documents and libraries as HTML, which provides added-value features like navigation and dynamic display.
 %The exported documents do not fully utilize the narrative flexibility of {\LaTeX} or HTML and are not meant for further editing.
@@ -16,8 +20,7 @@
 %Therefore, the formalization of a mathematical document $D$ in a proof assistant usually requires the -- expensive -- formalization of the background theory that connects $D$ to the foundation.
 %Moreover, the fixed implementation is limited to its input language, which in turn cannot be fully understood by any other system.
 
-The goal of \mmttex is not to introduce a new format but to use \latex documents as the primary user-written documents.
-That makes it most similar to \sTeX \cite{stex}, where authors add content markup that allows converting a \latex to an OMDoc document.
+The goal of \mmttex is very similar to \sTeX \cite{stex}, where authors add content markup that allows converting a \latex to an OMDoc document.
 %Via \latex ML \cite{latexml}, this permits generating \omdoc from the same source code that produces PDF documents.
 %\omdoc itself \cite{omdoc} is an XML format that integrates both content and narration markup.
 %Both \omdoc and sTeX do not define a reference semantics that would permit verifying the documents.

src/latex-mmt/paper/paper.tex

@@ -1,7 +1,7 @@
 \documentclass[orivec]{llncs}
 \pagestyle{plain}
 
-\usepackage{url}
+\usepackage{url,xcolor,paralist}
 \usepackage{wrapfig}
 \usepackage{amsmath,amssymb}
 \usepackage{xspace}
@@ -21,7 +21,6 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % local macros and configurations
-\usepackage[show]{ed}
 \usepackage{basics}
 
 \usepackage{local}
@@ -40,7 +39,7 @@
 
 \maketitle
 \begin{abstract}
-Narrative, presentation-oriented assistant systems for mathematics on the one hand and formal, content-oriented ones on the other hand have so far been developed and used largely independently.
+Narrative, presentation-oriented assistant systems for mathematics such as \latex on the one hand and formal, content-oriented ones such as proof assistants and computer algebra systems on the other hand have so far been developed and used largely independently.
 The former excel at communicating mathematical knowledge and the latter at certifying its correctness.
 
 \mmttex aims at combining the advantages of the two paradigms.

src/latex-mmt/paper/paper.tex.mmt

@@ -18,7 +18,7 @@ constant inv
  # 1 ' prec 60 
 
 
-theory GroupDefs
+theory Division
  : ex:?SFOLEQ
  = 
 include ?Group