ci.yml

on:
  push:
  pull_request:

name: Continuous Integration

jobs:
  build:
    strategy:
      matrix:
        toolchain:
          - "leanprover/lean4:4.3.0"
          - "leanprover/lean4:4.4.0"
          - "leanprover/lean4:4.5.0"
          - "leanprover/lean4:4.6.0"
    name: Build and test
    runs-on: ubuntu-latest
    steps:
      - name: Install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
      - uses: actions/checkout@v3

      - name: List all files
        run: |
          find . -name "*.lean" -type f

      - name: Select Lean version
        run: |
          echo "${{ matrix.toolchain }}" > lean-toolchain

      - name: Lean version
        run: |
          lean --version

      - name: Cache .lake
        uses: actions/cache@v3
        with:
          path: .lake
          key: ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lean-toolchain') }}
          
      - name: Build the project
        run: |
          lake build

      - name: Configure demo/test subproject
        run: |
          pushd demo
          lake update
          popd

      - name: Run tests
        run: |
          lake exe subverso-tests