update submodule #795
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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' }} | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| VM_PARTITION: [false, true] | |
| name: 'VM Partition=${{ matrix.VM_PARTITION }}' | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v5 | |
| with: | |
| path: hamr-codegen | |
| submodules: recursive | |
| - name: Retrieve versions.properties | |
| run: | | |
| wget -q https://raw.githubusercontent.com/sireum/kekinian/master/versions.properties | |
| - name: Cache Java | |
| id: cache-java | |
| uses: actions/cache@v5 | |
| with: | |
| path: hamr-codegen/bin/linux/java | |
| key: ${{ runner.os }}-${{ hashFiles('hamr-codegen/versions.properties') }}-java | |
| - name: Cache Scala | |
| id: cache-scala | |
| uses: actions/cache@v5 | |
| with: | |
| path: hamr-codegen/bin/scala | |
| key: ${{ runner.os }}-${{ hashFiles('hamr-codegen/versions.properties') }}-scala | |
| - name: Cache Coursier | |
| id: cache-coursier | |
| uses: actions/cache@v5 | |
| with: | |
| path: hamr-codegen/cache/coursier | |
| key: ${{ runner.os }}-${{ hashFiles('hamr-codegen/versions.properties') }}-coursier | |
| - name: Cache OSATE | |
| id: cache-osate | |
| uses: actions/cache@v5 | |
| with: | |
| path: hamr-codegen/bin/linux/osate | |
| key: ${{ runner.os }}-${{ hashFiles('hamr-codegen/jvm/src/main/resources/phantom_versions.properties') }}-osate | |
| - name: Build | |
| 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: | | |
| # Debian Bullseye is no longer fully available on deb.debian.org or security.debian.org, | |
| # especially for the armel architecture. Packages have been moved to archive.debian.org, | |
| # which no longer supports signed Release files or valid-until metadata. | |
| # This forces us to: | |
| # 1. Use archive.debian.org URLs instead of deb.debian.org. | |
| # 2. Disable APT's date validation with Acquire::Check-Valid-Until "false". | |
| cat > /etc/apt/sources.list <<EOF | |
| deb http://archive.debian.org/debian bullseye main contrib non-free | |
| #deb http://archive.debian.org/debian-security bullseye-security main contrib non-free | |
| deb http://archive.debian.org/debian bullseye-updates main contrib non-free | |
| EOF | |
| echo 'Acquire::Check-Valid-Until "false";' > /etc/apt/apt.conf.d/99no-check-valid-until | |
| export SEL4_CAMKES_ENV=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 | |
| # The container's .bashrc sources /opt/ghcup/.ghcup/env to put 'stack' (Haskell | |
| # build tool) in PATH, but non-interactive shells don't source .bashrc. | |
| # Without this, capDL-tool fails to build: "make: stack: No such file or directory" | |
| export PATH="/opt/ghcup/.ghcup/bin:$PATH" | |
| export STACK_ROOT="/etc/stack" | |
| ln -s $GITHUB_WORKSPACE/hamr-codegen /root/hamr-codegen | |
| export aptInstall="apt-get install -f -y --no-install-recommends" | |
| export DEBIAN_FRONTEND=noninteractive | |
| apt-get update | |
| ${aptInstall} p7zip-full | |
| # Installing emacs installs some package(s) that resolve an issue where | |
| # the OSATE gumbo parser fails to initialize when used in the docker container. | |
| # Use emacs-nox only — the X11-dependent variants (emacs-lucid, emacs-gtk) | |
| # fail due to debianutils/x11-common version conflicts in the container. | |
| ${aptInstall} emacs-nox | |
| mkdir -p $HOME/.ssh | |
| touch $HOME/.ssh/config | |
| chmod 700 $HOME/.ssh/config | |
| (echo "Host gitlab.adventium.com"; echo "StrictHostKeyChecking no") >> $HOME/.ssh/config | |
| 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 | |
| export VM_PARTITION=${{ matrix.VM_PARTITION }} | |
| echo "VM_PARTITION=${VM_PARTITION}" | |
| # see https://github.com/sireum/hamr-codegen-test/blob/master/scala/org/sireum/hamr/codegen/test/util/TestMode.scala | |
| export testmodes=phantom,sergen,slangcheck,tipe,ive,compile,camkes,generated_unit_tests,smt2${VERBOSE_DEBUG} | |
| echo "testmodes=${testmodes}" | |
| export SMT2_TIMEOUT=180000 | |
| echo "SMT2_TIMEOUT=${SMT2_TIMEOUT}" | |
| export ALSO_TRANSPILE_VIA_CALLBACKS=true | |
| echo "ALSO_TRANSPILE_VIA_CALLBACKS=${ALSO_TRANSPILE_VIA_CALLBACKS}" | |
| # Debian Bullseye's ca-certificates bundle does not include the | |
| # "Sectigo Public Server Authentication Root R46" CA used by | |
| # download.bell-sw.com (BellSoft JDK). Download Mozilla's current | |
| # CA bundle via wget (which works because github.com uses ISRG Root X1, | |
| # which IS in Bullseye's bundle), append it to the system CA store, | |
| # and also point curl at it via CURL_CA_BUNDLE. | |
| wget -qO /tmp/cacert.pem https://curl.se/ca/cacert.pem | |
| cat /tmp/cacert.pem >> /etc/ssl/certs/ca-certificates.crt | |
| export CURL_CA_BUNDLE=/tmp/cacert.pem | |
| export COURSIER_CACHE=$GITHUB_WORKSPACE/hamr-codegen/cache/coursier | |
| $HOME/hamr-codegen/bin/build.cmd test |