# Copyright (c) 2026 Ahmad Ali Parr. All rights reserved.
# SPDX-License-Identifier: LicenseRef-Proprietary
# Public source visibility does not grant an open-source license. See LICENSE.

name: Idris proof typecheck

on:
  push:
  pull_request:
  workflow_dispatch:

permissions:
  contents: read

jobs:
  typecheck:
    runs-on: ubuntu-24.04
    timeout-minutes: 35
    steps:
      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
      - name: Install bootstrap dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y chezscheme build-essential libgmp-dev
      - name: Cache pinned Idris installation
        id: idris-cache
        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830
        with:
          path: ~/.idris2
          key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1
      - name: Bootstrap pinned Idris 2
        if: steps.idris-cache.outputs.cache-hit != 'true'
        run: |
          git clone https://github.com/idris-lang/Idris2.git "$RUNNER_TEMP/Idris2"
          cd "$RUNNER_TEMP/Idris2"
          git checkout 15a3e4e70843f7a34100f6470c04b791330788df
          make bootstrap SCHEME=chezscheme
          make install
      - name: Save compiler before checking project proofs
        if: steps.idris-cache.outputs.cache-hit != 'true'
        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830
        with:
          path: ~/.idris2
          key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1
      - name: Check handwritten proof terms and model
        run: |
          export PATH="$HOME/.idris2/bin:$PATH"
          mkdir -p build/reports
          idris2 --version | tee build/reports/idris-version.txt
          set -o pipefail
          cd idris
          idris2 --total --check LambdaProofs.idr 2>&1 | tee ../build/reports/lambda-typecheck.txt
          idris2 --total --check Main.idr 2>&1 | tee ../build/reports/model-typecheck.txt
      - name: Compile and smoke-test the current control model
        run: |
          export PATH="$HOME/.idris2/bin:$PATH"
          set -o pipefail
          cd idris
          idris2 --total -o control-model Main.idr 2>&1 | tee ../build/reports/model-build.txt
          build/exec/control-model | tee ../build/reports/model-smoke.txt
          test "$(cat ../build/reports/model-smoke.txt)" = 'step: advanced'
      - name: Preserve typechecker evidence
        if: always()
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: idris-typecheck-evidence
          path: build/reports/
      - name: Preserve the prototype control-model executable
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: idris-control-model-ubuntu24
          path: idris/build/exec/