ci.yml

on:
  push:
  pull_request:

name: CI

jobs:
  build:
    strategy:
      matrix:
        toolchain:
          - "4.3.0"
          - "4.4.0"
          - "4.5.0"
          - "4.6.0"
          - "4.7.0"
          - "nightly-2024-04-07"
        platform:
          - os: ubuntu-latest
            installer: |
              curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
        # Mac runners are rare and expensive, so spot-check that the
        # subprocess support seems OK but be less thorough
        include:
          - toolchain: "4.7.0"
            os: macos-latest
            installer: |
              curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
          - toolchain: "4.7.0"
            os: macos-latest
            installer: |
              brew install elan-init
          - toolchain: "4.3.0"
            os: macos-latest
            installer: |
              brew install elan-init
    name: Build and test (${{ matrix.platform.os }}, ${{ matrix.platform.installer}}, ${{ matrix.toolchain}})
    runs-on: ${{ matrix.platform.os }}
    steps:
      - name: Install elan
        run: |
          set -o pipefail
          ${{ matrix.platform.installer }}
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Which lake?
        run: |
          which lake

      - uses: actions/checkout@v3

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

      - name: Select Lean version
        run: |
          echo "leanprover/lean4:${{ 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
          lake build :examples
          popd

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