Merge pull request #558 from UniFormal/master

Release 21.0.0

.github/workflows/CI.yml

@@ -1,40 +1,58 @@
 name: CI
 
-on: [push, pull_request]
+on:
+  push:
+    branches:
+      - master
+      - devel
+  pull_request:
+    branches:
+      - master
+      - devel
+
+  # Also trigger on page_build, as well as release created events
+  page_build:
+  release:
+    types: # This configuration does not affect the page_build event above
+      - created
 
 jobs:
   ci:
+    # Skip CI if the commit message of the head commit of a push
+    # contains "skip ci" or "ci skip"
+    if: "!contains(github.event.head_commit.message, 'skip ci') && !contains(github.event.head_commit.message, 'ci skip')"
+
     name: Continuous Integration
     runs-on: ubuntu-latest
     steps:
       - name: Checkout Repository
         uses: actions/checkout@v2
 
       - name: Install OpenJDK 14 and sbt
-        uses: olafurpg/setup-scala@v5
+        uses: olafurpg/setup-scala@v10
         with:
           java-version: [email protected]
 
       - name: Install Dependencies
         run: |
           cd src
-          sbt ++2.12.9 update
+          sbt ++2.13.4 update
 
       - name: Build 'mmt.jar'
         run: |
           cd src
-          sbt ++2.12.9 deploy
+          sbt ++2.13.4 deploy
 
       - name: Store 'mmt.jar' artifact
         uses: actions/upload-artifact@v2
         with:
           name: mmt.jar
-          path: deploy/mmt.jar
+          path: ./deploy/mmt.jar
 
       - name: Unit Tests
         run: |
           cd src
-          sbt ++2.12.9 test
+          sbt ++2.13.4 test
 
       - name: Integration Tests
         shell: bash

COPYING.txt

@@ -6,7 +6,7 @@ See http://uniformal.github.io/doc/setup/license.html for the rationale behind t
 
 ----------------------------------------------------------------------------------------
 
-Copyright (c) 2016-18, Florian Rabe and contributors
+Copyright (c) 2016-20, Florian Rabe and contributors
 All rights reserved.
 
 By contributing to this repository, contributors make their contribution subject to

Dockerfile

@@ -6,7 +6,7 @@ ADD src/ /build/MMT/src
 ADD deploy/ /build/MMT/deploy
 
 WORKDIR /build/MMT/src
-RUN sbt ++2.12.8 deploy
+RUN sbt ++2.13.4 deploy
 
 # Runtime dependencies
 FROM openjdk:jre-alpine
@@ -34,4 +34,4 @@ RUN mmt :setup "/mmt/" "/content/" ":" "--no-content"
 
 ADD scripts/docker/install.msl /install.msl
 ADD scripts/docker/entrypoint.sh /entrypoint.sh
-ENTRYPOINT ["/entrypoint.sh"]
+ENTRYPOINT ["/entrypoint.sh"]

deploy/lib/version.txt

@@ -2,10 +2,11 @@ Don't put version numbers into file names here.
 It messes up references every time we upgrade to a new version.
 Instead, track the versions here.
 
-Scala language: 2.12.9
+Scala language: 2.13.4
 Scala modules:
- xml: 1.0.6
- parser-combinators: 1.0.7
- reflect: 2.12.9
+ xml: 2.0.0-M3
+ parser-combinators: 1.2.0-M1
+ reflect: 2.13.4
+ parallel-collections: 1.0.0
 
-xz: 1.8
+xz: 1.8

src/build.sbt

@@ -48,10 +48,10 @@ lazy val mmtMainClass = "info.kwarc.mmt.api.frontend.Run"
 //   (2) verify whether there is a Scala paradise plugin available on Maven central for the new Scala version
 //       Search for "paradise" way to below to find the dependency "org.scalamacros" % "paradise_****" in this build.sbt file.
 //
-scalaVersion in Global := "2.12.9"
+scalaVersion in Global := "2.13.4"
 scalacOptions in Global := Seq(
   "-feature", "-language:postfixOps", "-language:implicitConversions", "-deprecation",
-  "-Xmax-classfile-name", "128", // fix long classnames on weird filesystems
+  // "-Xmax-classfile-name", "128", // fix long classnames on weird filesystems // does not exist anymore since scala 2.13.*
   "-sourcepath", baseDirectory.value.getAbsolutePath // make sure that all scaladoc source paths are relative
 )
 
@@ -99,7 +99,7 @@ def commonSettings(nameStr: String) = Seq(
   sourcesInBase := false,
   autoAPIMappings := true,
   exportJars := true,
-  libraryDependencies += "org.scalatest" % "scalatest_2.12" % "3.0.4" % "test",
+  libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.3" % "test",
   fork := true,
   test in assembly := {},
   assemblyMergeStrategy in assembly := {
@@ -167,7 +167,7 @@ lazy val src = (project in file(".")).
 // This is the main project. 'mmt/deploy' compiles all relevants subprojects, builds a self-contained jar file, and puts into the deploy folder, from where it can be run.
 lazy val mmt = (project in file("mmt")).
   exclusions(excludedProjects).
-  dependsOn(tptp, stex, pvs, specware, oeis, odk, jedit, latex, openmath, imps, isabelle, repl, concepts, interviews, mathhub, python, intellij, coq, glf, lsp).
+  dependsOn(tptp, stex, pvs, specware, oeis, odk, jedit, latex, openmath, mizar, imps, isabelle, repl, concepts, interviews, mathhub, python, intellij, coq, glf, lsp).
   settings(mmtProjectsSettings("mmt"): _*).
   settings(
     exportJars := false,
@@ -201,6 +201,7 @@ def apiJars(u: Utils) = Seq(
   "scala-parser-combinators.jar",
   "scala-xml.jar",
   "xz.jar",
+  "scala-parallel-collections.jar"
 ).map(u.lib.toJava / _)
 
 // The kernel upon which everything else depends. Maintainer: Florian
@@ -223,7 +224,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.8" % "test",
+    //    libraryDependencies += "org.scala-lang" % "scala-parser-combinators" % "1.2.0-M1" % "test",
   )
 
 // =================================
@@ -379,7 +380,7 @@ val finchVersion = "0.32.1"
 // Circe is a JSON library (https://circe.github.io/circe/), a FrameIT dependency
 val circeVersion = "0.13.0"
 lazy val frameit = (project in file("frameit-mmt"))
-  .dependsOn(api, lf)
+  .dependsOn(api, lf, odk)
   .settings(mmtProjectsSettings("frameit-mmt"): _*)
   .settings(
     libraryDependencies ++= Seq(
@@ -406,12 +407,14 @@ lazy val frameit = (project in file("frameit-mmt"))
     ),
 
     scalacOptions in Compile ++= Seq(
-      "-Xplugin-require:macroparadise"
+     // "-Xplugin-require:macroparadise"
+      "-Ymacro-annotations"
     ),
 
     // in order for @ConfiguredJsonCodec from circe-generic-extras (a FrameIT dependency above) to work
-    resolvers += Resolver.sonatypeRepo("releases"),
-    addCompilerPlugin("org.scalamacros" % "paradise" % "2.1.1" cross CrossVersion.full)
+    // resolvers += Resolver.sonatypeRepo("releases"),
+    // addCompilerPlugin("org.scalamacros" % "paradise" % "2.1.1" cross CrossVersion.full)
+
   )
 
 // plugin for mathscheme-related functionality. Obsolete

src/frameit-mmt/DEV.md

@@ -0,0 +1,3 @@
+# frameit-mmt: Developer's Notes
+
+- read <https://github.com/UniFormal/uniformal.github.io/wiki/Programmatically-creating-MMT-content-(checklist)>