From 84f1bc644121026670fc1483a85fc13a91e5fe28 Mon Sep 17 00:00:00 2001 From: Jason Belt Date: Wed, 6 Nov 2024 13:14:05 -0600 Subject: [PATCH] add ci artifacts --- .ci/docker-setup.cmd | 44 +++++++++++++++++++ .ci/test.cmd | 37 ++++++++++++++++ .github/workflows/CI-camkes.yml | 75 ++++++++++++++++++++++++++++++++ .github/workflows/CI-linux.yml | 16 +++---- .github/workflows/CI-macOS.yml | 18 +++----- .github/workflows/CI-windows.yml | 55 +++++++++++++++++++++++ models/sysml-rts | 2 +- 7 files changed, 225 insertions(+), 22 deletions(-) create mode 100755 .ci/docker-setup.cmd create mode 100755 .ci/test.cmd create mode 100644 .github/workflows/CI-camkes.yml create mode 100644 .github/workflows/CI-windows.yml diff --git a/.ci/docker-setup.cmd b/.ci/docker-setup.cmd new file mode 100755 index 0000000..1b48703 --- /dev/null +++ b/.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() diff --git a/.ci/test.cmd b/.ci/test.cmd new file mode 100755 index 0000000..a0c0bb4 --- /dev/null +++ b/.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) diff --git a/.github/workflows/CI-camkes.yml b/.github/workflows/CI-camkes.yml new file mode 100644 index 0000000..6b8af0a --- /dev/null +++ b/.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 diff --git a/.github/workflows/CI-linux.yml b/.github/workflows/CI-linux.yml index a22b117..0b027fa 100644 --- a/.github/workflows/CI-linux.yml +++ b/.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 diff --git a/.github/workflows/CI-macOS.yml b/.github/workflows/CI-macOS.yml index 5c1d4d5..787bb30 100644 --- a/.github/workflows/CI-macOS.yml +++ b/.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 diff --git a/.github/workflows/CI-windows.yml b/.github/workflows/CI-windows.yml new file mode 100644 index 0000000..842f89f --- /dev/null +++ b/.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% diff --git a/models/sysml-rts b/models/sysml-rts index 1b129df..fe6e8de 160000 --- a/models/sysml-rts +++ b/models/sysml-rts @@ -1 +1 @@ -Subproject commit 1b129df8e38ad4307752cad30806a6b852e921ec +Subproject commit fe6e8dec50606b6f4d4fa05b5205c3afed894c3d