ci-deptycheck.yml

---
name: Build and test

on:
  push:
    branches:
      - main
      - master
    tags:
      - '**'
  pull_request:
    branches:
      - main
      - master
  schedule:
    # We want to run in the beginning of the day, right after the `pack` collection is built at the end of the previous day.
    - cron: '0 1 * * *'

concurrency:
  group: ${{ github.workflow }}@${{ github.ref }}
  cancel-in-progress: true

defaults:
  run:
    shell: bash

env:
  PACK_DIR: /root/.pack
  pack_dir_file: pack-dir.tar

# TODO to reduce duplication, e.g. by using https://docs.github.com/en/actions/using-workflows/reusing-workflows

jobs:

  ################
  # Preparations #
  ################

  prepare-pack:
    name: Prepare `pack`
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    steps:
      - uses: actions/checkout@v3

      - run: pack update-db
      - name: Switch to appropriate `pack` collection
        run: pack switch "$( if [[ '${{ github.event_name }}' == 'schedule' ]]; then echo latest; else cat .pack-collection; fi )"

      - name: Tar the `pack` dir
        run: tar -cvf "${{ env.pack_dir_file }}" --exclude=".cache" "${{ env.PACK_DIR }}"
      - name: Save state of `pack`
        uses: actions/upload-artifact@v3
        with:
          name: pack-dir
          path: ${{ env.pack_dir_file }}

  thirdparties-build:
    name: Build thirdparties
    needs: prepare-pack
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    steps:
      - name: Install Git in order to enable checkout with submodules
        run: |
          apt-get update
          apt-get -y install git
      - uses: actions/checkout@v3
        with:
          submodules: true
      - name: Restore state of `pack`
        uses: actions/download-artifact@v3
        with:
          name: pack-dir
      - name: Untar the `pack` dir
        run: tar -xvf "${{ env.pack_dir_file }}" --one-top-level=/ --touch

      - run: pack install elab-util mtl-tuple-impls random-pure sop summary-stat

      - name: Tar the `pack` dir
        run: tar -uvf "${{ env.pack_dir_file }}" --exclude=".cache" "${{ env.PACK_DIR }}"
      - name: Save built thirdparties
        uses: actions/upload-artifact@v3
        with:
          name: built-thirdparties
          path: ${{ env.pack_dir_file }}

  ############################################
  # Build and test deptycheck library itself #
  ############################################

  deptycheck-build-lib:
    name: Build DepTyCheck lib
    needs:
      - prepare-pack
      - thirdparties-build
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    steps:
      - uses: actions/checkout@v3
      - name: Restore built thirdparties
        uses: actions/download-artifact@v3
        with:
          name: built-thirdparties
      - name: Untar the `pack` dir
        run: tar -xvf "${{ env.pack_dir_file }}" --one-top-level=/ --touch

      - run: pack build deptycheck

      - name: Tar the `pack` dir
        run: tar -uvf "${{ env.pack_dir_file }}" --exclude=".cache" "${{ env.PACK_DIR }}"
      - name: Tar built TTC files
        run: find "$(pwd)" -name '*.tt[cm]' | tar -uvf "${{ env.pack_dir_file }}" --files-from /dev/stdin
      - name: Save built DepTyCheck
        uses: actions/upload-artifact@v3
        with:
          name: built-deptycheck
          path: ${{ env.pack_dir_file }}

  deptycheck-test-lib:
    name: Test DepTyCheck lib
    needs:
      - prepare-pack
      - deptycheck-build-lib
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    steps:
      - uses: actions/checkout@v3
      - name: Restore built DepTyCheck
        uses: actions/download-artifact@v3
        with:
          name: built-deptycheck
      - name: Untar the `pack` dir
        run: tar -xvf "${{ env.pack_dir_file }}" --one-top-level=/ --touch

      - run: pack test deptycheck lib/

  ##########################
  # Test deptycheck's docs #
  ##########################

  deptycheck-build-docs:
    name: Build DepTyCheck docs
    runs-on: ubuntu-latest
    container: sphinxdoc/sphinx:latest
    steps:
      - uses: actions/checkout@v3
      - name: Install dependencies
        run: pip3 install -r docs/requirements.txt
      - run: alias sh=bash
      # - run: pack build docs # `pack` is unaccessible here, thus:
      - run: cd docs && eval "$(grep prebuild docs.ipkg | sed 's/.*"\(.*\)"/\1/')"

  deptycheck-test-docs:
    name: Test DepTyCheck docs
    needs:
      - prepare-pack
      - deptycheck-build-lib
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    steps:
      - uses: actions/checkout@v3
      - name: Restore built DepTyCheck
        uses: actions/download-artifact@v3
        with:
          name: built-deptycheck
      - name: Untar the `pack` dir
        run: tar -xvf "${{ env.pack_dir_file }}" --one-top-level=/ --touch

      - run: pack test deptycheck docs/

  ################################
  # Test deptycheck's derivation #
  ################################

  get-derivation-test-sets:
    name: Aquire test sets for derivation
    needs:
      - deptycheck-build-lib
    runs-on: ubuntu-latest
    outputs:
      derivation-test-sets: ${{ steps.get-derivation-test-sets.outputs.derivation-test-sets }}
    steps:
      - name: Checkout
        uses: actions/checkout@v3
      - name: Get derivation test sets
        id: get-derivation-test-sets
        run: |
          (
          echo -n "derivation-test-sets=["
          find tests/derivation/ -type f,l -name run | \
            grep -v '/_' | sed 's|^tests/derivation/|"|' | sed 's|/[^/]*/run$|"|' | \
            sort | uniq | awk 'ORS=", "' | head -c -2
          echo "]"
          ) >> "$GITHUB_OUTPUT"

  deptycheck-test-derivation:
    name: Test DepTyCheck's derivation
    needs:
      - prepare-pack
      - deptycheck-build-lib
      - get-derivation-test-sets
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    strategy:
      fail-fast: false # all test cases are more or less independent
      matrix:
        test_set: ${{ fromJSON(needs.get-derivation-test-sets.outputs.derivation-test-sets) }}
    steps:
      - name: Checkout
        uses: actions/checkout@v3
      - name: Restore built DepTyCheck
        uses: actions/download-artifact@v3
        with:
          name: built-deptycheck
      - name: Untar the `pack` dir
        run: tar -xvf "${{ env.pack_dir_file }}" --one-top-level=/ --touch

      - run: pack test deptycheck "derivation/${{matrix.test_set}}"

  #################
  # Test examples #
  #################

  pil-build:
    name: Build PIL example
    needs:
      - prepare-pack
      - deptycheck-build-lib
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    steps:
      - uses: actions/checkout@v3
      - name: Restore built DepTyCheck
        uses: actions/download-artifact@v3
        with:
          name: built-deptycheck
      - name: Untar the `pack` dir
        run: tar -xvf "${{ env.pack_dir_file }}" --one-top-level=/ --touch

      - run: pack build pil

      - name: Tar the `pack` dir
        run: tar -uvf "${{ env.pack_dir_file }}" --exclude=".cache" "${{ env.PACK_DIR }}"
      - name: Tar built TTC files
        run: find "$(pwd)" -name '*.tt[cm]' | tar -uvf "${{ env.pack_dir_file }}" --files-from /dev/stdin
      - name: Save built PIL
        uses: actions/upload-artifact@v3
        with:
          name: built-pil
          path: ${{ env.pack_dir_file }}

  pil-test:
    name: Test PIL example
    needs:
      - prepare-pack
      - deptycheck-build-lib
      - pil-build
    runs-on: ubuntu-latest
    container: ghcr.io/stefan-hoeck/idris2-pack:latest
    steps:
      - uses: actions/checkout@v3
      - name: Restore built PIL
        uses: actions/download-artifact@v3
        with:
          name: built-pil
      - name: Untar the `pack` dir
        run: tar -xvf "${{ env.pack_dir_file }}" --one-top-level=/ --touch

      - run: pack test pil