ci.yml

name: Proof

on:
  # Run this action every day
  schedule:
    - cron: '30 18 * * *'
  pull_request:
  push:
    branches: bitvector-rebase-AP-change-new

# cancel in-progress job when a new push is performed
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  build:
    strategy:
      matrix:
        version: [5.2.0]

    runs-on: ubuntu-22.04

    steps:
    - uses: actions/checkout@v4
      with:
        repository: rems-project/cerberus

    - name: System dependencies (ubuntu)
      run: |
        sudo apt install build-essential libgmp-dev z3 opam

    - name: Restore cached opam
      id: cache-opam-restore
      uses: actions/cache/restore@v4
      with:
        path: ~/.opam
        key: ${{ matrix.version }}

    - name: Setup opam
      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
      run: |
        opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }}
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam install --deps-only --yes ./cerberus.opam ./cerberus-lib.opam ./cn.opam
        opam install --yes z3

    - name: Save cached opam
      if: steps.cache-opam-restore.outputs.cache-hit != 'true'
      id: cache-opam-save
      uses: actions/cache/save@v4
      with:
        path: ~/.opam
        key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}

    - name: Install Cerberus
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cerberus-lib .
        opam pin --yes --no-action add cerberus .
        opam install --yes cerberus

    - name: Install CN
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        opam pin --yes --no-action add cn .
        opam install --yes cn

#   - name: Download cvc5 release
#     uses: robinraju/release-downloader@v1
#     with:
#       repository: cvc5/cvc5
#       tag: cvc5-1.1.2
#       fileName: cvc5-Linux-static.zip

#    - name: Unzip and install cvc5
#      run: |
#        unzip cvc5-Linux-static.zip
#        chmod +x cvc5-Linux-static/bin/cvc5
#        sudo cp cvc5-Linux-static/bin/cvc5 /usr/local/bin/

    - name: Checkout this repo
      uses: actions/checkout@v4
      with:
        path: buddy-alloc

    - name: Run CN Proof
      run: |
        opam switch ${{ matrix.version }}
        eval $(opam env --switch=${{ matrix.version }})
        cd buddy-alloc && ./proof.sh