CI-camkes.yml

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@v4
        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@v4
        with:
          path: bin/linux/java
          key: ${{ runner.os }}-${{ hashFiles('versions.properties') }}-java
      - name: Cache Scala
        id: cache-scala
        uses: actions/cache@v4
        with:
          path: bin/scala
          key: ${{ runner.os }}-${{ hashFiles('versions.properties') }}-scala
      - name: Cache Coursier
        id: cache-coursier
        uses: actions/cache@v4
        with:
          path: cache/coursier
          key: ${{ runner.os }}-${{ hashFiles('versions.properties') }}-coursier
      - name: Cache OSATE
        id: cache-osate
        uses: actions/cache@v4
        with:
          path: bin/linux/osate
          key: ${{ runner.os }}-${{ hashFiles('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: |
          # 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 ./hamr-codegen /root/
          
          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.
          ${aptInstall} emacs
          
          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}"
          
          $HOME/hamr-codegen/bin/build.cmd test