add ci artifacts

.ci/docker-setup.cmd

@@ -0,0 +1,44 @@
+::/*#! 2> /dev/null                                   #
+@ 2>/dev/null # 2>nul & echo off & goto BOF           #
+if [ -z "${SIREUM_HOME}" ]; then                      #
+  echo "Please set SIREUM_HOME env var"               #
+  exit -1                                             #
+fi                                                    #
+exec "${SIREUM_HOME}/bin/sireum" slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+"%SIREUM_HOME%\bin\sireum.bat" slang run %0 %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val content: ST = 
+  st"""FROM trustworthysystems/camkes
+      |
+      |WORKDIR /root
+      |
+      |ENV SIREUM_HOME=/root/Sireum
+      |ENV PATH="$$SIREUM_HOME/bin:$$PATH"
+      |
+      |RUN git config --global user.email "" &&\
+      |    git config --global user.name "" &&\
+      |    git config --global color.ui false &&\
+      |    mkdir camkes && cd camkes &&\
+      |    repo init -u https://github.com/seL4/camkes-manifest.git &&\
+      |    repo sync &&\
+      |    cd &&\
+      |    (export SIREUM_NO_SETUP=true && DIR=Sireum && export SIREUM_V=master && rm -fR $$DIR && mkdir -p $$DIR/bin && cd $$DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$$SIREUM_V/bin/init.sh && bash init.sh)
+      |"""
+
+
+val dockerDir = Os.tempDir()
+val dockerFile = dockerDir / "Dockerfile"
+dockerFile.write(content.render)
+
+proc"docker build -t camkes.sireum .".at(dockerDir).console.runCheck()

.ci/test.cmd

@@ -0,0 +1,37 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val rootDir = Os.slashDir.up
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
+val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")
+
+var result: Z = 0
+def findCIs(p: Os.Path): Unit = {
+  if(p.isFile && p.name == "ci.cmd") {
+    val r = proc"$sireum slang run $p".console.echo.run()
+    result = result + r.exitCode
+  } else if(p.isDir) {
+    p.list.foreach((m: Os.Path) => findCIs(m))
+  }
+}
+findCIs(rootDir)
+
+Os.exit(result)

.github/workflows/CI-camkes.yml

@@ -0,0 +1,75 @@
+name: CAmkES
+
+on: 
+  push:
+  schedule:
+    - cron: "0 2 * * 6" # every sunday at 2am
+  workflow_dispatch:
+    inputs:
+      docker_image:
+        type: string
+        description: Docker image to fetch
+        default: trustworthysystems/camkes
+      verbose:
+        type: boolean
+        description: Enable verbose testing output
+        default: false
+
+jobs:
+  container:
+    runs-on: ubuntu-latest
+    container:
+      image: ${{ inputs.docker_image != '' && inputs.docker_image || 'trustworthysystems/camkes' }}
+    name: Build
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          path: sysmlv2-models
+          submodules: recursive
+      - name: Test
+        env:
+          # add verbose flag if workflow is restarted with "enable debug logging" checked or if requested
+          # via workflow dispatch
+          VERBOSE_DEBUG: ${{ ( runner.debug == '1' || inputs.verbose == '1' ) && ',verbose' || '' }}
+        run: |
+          export CAMKES=true
+          
+          # github sets HOME to /github/home but some tools (Sireum's Os.home, Haskell) use
+          # the containers /root instead leading to inconsistent installs. Setting HOME
+          # to be root resolves the issue
+          # https://github.com/actions/runner/issues/1474#issuecomment-965805123
+          export HOME=/root
+
+          mv ./sysmlv2-models $HOME/
+          
+          export aptInstall="apt-get install -f -y --no-install-recommends"
+          export DEBIAN_FRONTEND=noninteractive
+          apt-get update
+          ${aptInstall} p7zip-full unzip
+
+          # Installing emacs installs some package(s) that resolve an issue where
+          # the OSATE gumbo parser fails to initialize when used in the docker container.
+          ${aptInstall} emacs
+
+          DISTRO=ive sh -c "$(curl -fsSL https://github.com/sireum/kekinian/releases/download/dev/install.cmd)"
+          export SIREUM_HOME=$HOME/Applications/Sireum/
+          export PATH=$SIREUM_HOME/bin:$PATH
+
+          sireum
+
+          export CASE_DIR=$HOME/CASE
+          
+          mkdir -p $CASE_DIR/camkes
+          cd $CASE_DIR/camkes
+          repo init -u https://github.com/seL4/camkes-manifest.git
+          repo sync
+          
+          mkdir -p $CASE_DIR/camkes-vm-examples
+          cd $CASE_DIR/camkes-vm-examples
+          repo init -u https://github.com/seL4/camkes-vm-examples-manifest.git
+          repo sync
+
+          cd $HOME/sysmlv2-models
+
+          .ci/test.cmd

.github/workflows/CI-linux.yml

@@ -2,6 +2,9 @@ name: Linux
 
 on:
   push:
+  schedule:
+    - cron: "0 2 * * 6" # every sunday at 2am
+  workflow_dispatch:
 
 jobs:
 
@@ -12,19 +15,12 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: recursive
-          path: sysmlv2-models
-      - name: Checkout-Sireum
-        uses: actions/checkout@v4
-        with:
-          repository: sireum/kekinian
-          submodules: recursive
-          path: kekinian
       - name: Tipe
         run: |
-          kekinian/bin/build.cmd
-          export SIREUM_HOME=$(pwd)/kekinian
+          DISTRO=ive sh -c "$(curl -fsSL https://github.com/sireum/kekinian/releases/download/dev/install.cmd)"
+          export SIREUM_HOME=$HOME/Applications/Sireum/
           export PATH=$SIREUM_HOME/bin:$PATH
           
           sireum
           
-          sireum hamr sysml tipe --sourcepath $(pwd)/sysmlv2-models
+          .ci/test.cmd

.github/workflows/CI-macOS.yml

@@ -2,6 +2,9 @@ name: macOS
 
 on:
   push:
+  schedule:
+    - cron: "0 2 * * 6" # every sunday at 2am
+  workflow_dispatch:
 
 jobs:
 
@@ -12,19 +15,12 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: recursive
-          path: sysmlv2-models
-      - name: Checkout-Sireum
-        uses: actions/checkout@v4
-        with:
-          repository: sireum/kekinian
-          submodules: recursive
-          path: kekinian
       - name: Tipe
         run: |
-          kekinian/bin/build.cmd
-          export SIREUM_HOME=$(pwd)/kekinian
+          DISTRO=ive sh -c "$(curl -fsSL https://github.com/sireum/kekinian/releases/download/dev/install.cmd)"
+          export SIREUM_HOME=$HOME/Applications/Sireum/
           export PATH=$SIREUM_HOME/bin:$PATH
           
           sireum
-          
-          sireum hamr sysml tipe --sourcepath $(pwd)/sysmlv2-models
+
+          .ci/test.cmd

.github/workflows/CI-windows.yml

@@ -0,0 +1,55 @@
+name: Windows
+
+on:
+  push:
+  schedule:
+    - cron: "0 2 * * 6" # every sunday at 2am
+  workflow_dispatch:
+
+jobs:
+
+  ci:
+    runs-on: windows-latest
+    steps:
+      - name: Set git to use LF
+        run: |
+          git config -l
+          echo "---"
+          git config --global core.autocrlf false
+          git config --global core.eol lf
+          echo "---"
+          git config -l
+      - name: Support longpaths
+        run: git config --system core.longpaths true
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Install Cygwin
+        shell: cmd
+        run: |
+          choco config get cacheLocation
+          choco install --no-progress cygwin
+          C:\tools\cygwin\cygwinsetup.exe -qgnNdO -R C:/tools/cygwin -s http://mirrors.kernel.org/sourceware/cygwin/ -P gcc-core,gcc-g++,make,cmake
+      - name: Check LongPathsEnabled
+        run: |
+          (Get-ItemProperty "HKLM:System\CurrentControlSet\Control\FileSystem").LongPathsEnabled
+      - name: Test
+        shell: cmd
+        run: |
+          cmd /V/C "set DISTRO=ive&& curl -JLOs https://github.com/sireum/kekinian/releases/download/dev/install.cmd && install.cmd && del /q/f install.cmd"
+          
+          set SIREUM_HOME=%USERPROFILE%\Applications\Sireum
+          set PATH=%SIREUM_HOME%\bin;%PATH%
+
+          set errorlevel=
+
+          call sireum.bat || goto :error
+           
+          dir
+          call .ci\test.cmd || goto :error
+
+          goto :EOF
+          :error
+          echo Exit Codeg %errorlevel%
+          exit /b %errorlevel%