Merge pull request #569 from UniFormal/master

Release 22

.github/workflows/CI.yml

@@ -1,61 +1,113 @@
-name: CI
-
-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
+name: Integration Tests
+
+on: [push, pull_request, workflow_dispatch]
+
+env:
+  SCALA_VERSION: '2.13.4'
+  JAVA_VERSION: '[email protected]'
 
 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
+    name: Integration Tests
     runs-on: ubuntu-latest
     steps:
       - name: Checkout Repository
         uses: actions/checkout@v2
 
-      - name: Install OpenJDK 14 and sbt
-        uses: olafurpg/setup-scala@v10
+      - name: Install Java (${{ env.JAVA_VERSION }}) and Scala (${{ env.SCALA_VERSION }})
+        uses: olafurpg/setup-scala@v11
         with:
-          java-version: [email protected]
+          java-version: ${{ env.JAVA_VERSION }}
 
-      - name: Install Dependencies
+      - name: Download MMT dependencies using 'sbt update'
         run: |
           cd src
-          sbt ++2.13.4 update
+          sbt ++${{ env.SCALA_VERSION }} update
 
-      - name: Build 'mmt.jar'
+      - name: Build 'mmt.jar' using 'sbt deploy'
         run: |
           cd src
-          sbt ++2.13.4 deploy
+          sbt ++${{ env.SCALA_VERSION }} deploy
 
       - name: Store 'mmt.jar' artifact
         uses: actions/upload-artifact@v2
         with:
           name: mmt.jar
           path: ./deploy/mmt.jar
 
-      - name: Unit Tests
+      - name: Run Unit Tests
         run: |
           cd src
-          sbt ++2.13.4 test
+          sbt ++${{ env.SCALA_VERSION }} test
+      
+      - name: Use 'devel' version for MMT Archives
+        run: |
+          echo "MMT_ARCHIVE_VERSION=devel" >> $GITHUB_ENV
+        if: "!startsWith(github.ref, 'refs/heads/master')"
+
+      - name: Use 'master' version for MMT Archives
+        run: |
+          echo "MMT_ARCHIVE_VERSION=master" >> $GITHUB_ENV
+        if: startsWith(github.ref, 'refs/heads/master')
+
+      - name: Run MMT Setup and store root directory
+        id: setup
+        run: |
+          java -jar ./deploy/mmt.jar :setup --auto --auto --no-content --no-jedit
+          echo "MMT_ARCHIVE_ROOT=../MMT-content" >> $GITHUB_ENV
 
-      - name: Integration Tests
-        shell: bash
+      - name: Test '${{ env.MMT_ARCHIVE }}'
+        if: always() && steps.setup.outcome == 'success'
+        env:
+          MMT_ARCHIVE: 'MMT/urtheories'
+        run: |
+          java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }}
+          java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl
+      
+      - name: Test '${{ env.MMT_ARCHIVE }}'
+        if: always() && steps.setup.outcome == 'success'
+        env:
+          MMT_ARCHIVE: 'MMT/examples'
+        run: |
+          java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }}
+          java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl
+      
+      - name: Test '${{ env.MMT_ARCHIVE }}'
+        if: always() && steps.setup.outcome == 'success'
+        env:
+          MMT_ARCHIVE: 'MMT/LATIN2'
+        run: |
+          java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }}
+          java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl
+          
+      - name: Test '${{ env.MMT_ARCHIVE }}'
+        if: always() && steps.setup.outcome == 'success'
+        env:
+          MMT_ARCHIVE: 'MMT/LFX'
+        run: |
+          java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }}
+          java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl
+          
+      - name: Test '${{ env.MMT_ARCHIVE }}'
+        if: always() && steps.setup.outcome == 'success'
+        env:
+          MMT_ARCHIVE: 'Test/General'
+        run: |
+          java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }}
+          java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl
+          
+      - name: Test '${{ env.MMT_ARCHIVE }}'
+        if: always() && steps.setup.outcome == 'success'
+        env:
+          MMT_ARCHIVE: 'MitM/Foundation'
+        run: |
+          java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }}
+          java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl
+          
+      - name: Test '${{ env.MMT_ARCHIVE }}'
+        if: always() && steps.setup.outcome == 'success'
+        env:
+          MMT_ARCHIVE: 'MitM/Core'
         run: |
-          export TEST_USE_BRANCH=${GITHUB_REF#refs/heads/}
-          java -cp deploy/mmt.jar info.kwarc.mmt.test.TestRunner
+          java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }}
+          java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl

.gitignore

@@ -1,27 +1,21 @@
 src/project/project
 src/project/build.properties
 
-# do not commit 
-
 # Do not accidentally commit test files
 test/*.scala
 
 # configuration files
 src/mmt-sbt-settings
 
-# mmtrc --created by installed
+# mmtrc --created by mmt.jar setup routine
 deploy/mmtrc
 
-# compiled MMT Jars
-deploy/mmt.jar
-deploy/main/*.jar
-
-# Compiled dependened projects
-deploy/lfcatalog/lfcatalog.jar
-deploy/lib/tiscaf.jar
-
 # Documentation & Deploy
 apidoc
+deploy/*.jar
+deploy/lfcatalog/lfcatalog.jar
+deploy/lib/tiscaf.jar
+deploy/main/*.jar
 scripts/travis/deploy_key
 
 # IntelliJ Failes
@@ -40,6 +34,7 @@ target
 
 # scala-bin compilation articfacts
 out/
+
 */.DS_Store
 
 # Artifact of https://github.com/coursier/coursier when working with IntelliJ

deploy/lib/version.txt

@@ -10,3 +10,10 @@ Scala modules:
  parallel-collections: 1.0.0
 
 xz: 1.8
+
+
+------------
+
+tested with
+IntelliJ Community edition 2021.2.3
+sbt 1.3.13 (auto-downloaded by IntelliJ)

deploy/run-file

@@ -0,0 +1,6 @@
+#!/bin/bash
+
+# This is like run except that it automatically loads an msl file passed as an argument.
+# You may want to associate the msl file ending with this script.
+dir="$(dirname $0)"
+java -Xmx8192m -cp "$dir/lib/*:$dir/mmt.jar" info.kwarc.mmt.api.frontend.Run :file $1

deploy/run-file.bat

@@ -1,4 +1,5 @@
+@echo off
 rem This is like run.bat except that it automatically loads an msl file passed as an argument.
 rem You may want to associate the msl file ending with this script.
 
-java -Xmx1024m -cp %~dp0/lib/*;%~dp0/main/*;%~dp0/lfcatalog/lfcatalog.jar info.kwarc.mmt.api.frontend.Run --shell file %1
+java -Xmx1024m -cp %~dp0/mmt.jar info.kwarc.mmt.api.frontend.Run :file %1

scripts/docker/entrypoint.sh

@@ -7,7 +7,7 @@ mkdir -p /content/MathHub
 # if the $MMT_ARCHIVES variable is set, install all the archives
 if [ ! -z "$MMT_ARCHIVES" ]; then
     echo "Installing MMT Archives: $MMT_ARCHIVES"
-    mmt --file /install.msl "lmh install $MMT_ARCHIVES"
+    mmt "$@" --file /install.msl "lmh install $MMT_ARCHIVES ; exit"
     echo "Done. "
 fi