ci.yaml

name: Viper Roots CI

on:
  push:
    branches: [ main ]
  pull_request:
    branches: [ main ]
  workflow_dispatch:

jobs:
  build:
    strategy:
      matrix:
        os: [ubuntu-latest]
      fail-fast: false
    runs-on: ${{ matrix.os }}
    steps:
      - uses: actions/checkout@v2
        with:
          submodules: 'true'

      - name: Download and install Isabelle
        run: |
          wget --quiet https://isabelle.in.tum.de/website-Isabelle2024/dist/Isabelle2024_linux.tar.gz -O isabelle.tar.gz
          mkdir -p isabelle
          tar -xzf isabelle.tar.gz -C isabelle --strip-components=1
          rm isabelle.tar.gz
          isabelle/bin/isabelle version
          echo isabelle/bin >> $GITHUB_PATH

      - name: Setup Isabelle sessions
        run: |
          isabelle components -u foundational_boogie/BoogieLang
          isabelle components -u vipersemcommon
          isabelle components -u viper-total-heaps
          isabelle components -u vipersemabstract
          isabelle components -u viper-abstract-refines-total
          isabelle components -u simple-frontend

      - name: Check whether Isabelle theories go through successfully
        # viper-total-heaps/paper-results has viper-total-heaps as a parent session
        run: |
          isabelle build -j4 -D viper-total-heaps/paper-results
          isabelle build -j4 -D vipersemabstract
          isabelle build -j4 -D viper-abstract-refines-total
          isabelle build -j4 -D simple-frontend
          isabelle build -j4 -D main-results