# SPDX-License-Identifier: MPL-2.0
name: Agda

on:
  push:
    branches: [main, master]
  pull_request:
  workflow_dispatch:

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

permissions:
  contents: read

jobs:
  check:
    runs-on: ubuntu-24.04
    timeout-minutes: 30
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          persist-credentials: false
      - name: Kernel certificate and module classification
        run: sh scripts/kernel-guard.sh
      - name: Experimental aggregate coverage
        run: |
          bash scripts/check-experimental-aggregate.sh
          bash scripts/test-experimental-aggregate.sh
      - name: Agda invocation profiles
        run: sh scripts/check-agda-invocations.sh
      - name: Foundation guardrail
        run: bash tools/check-guardrails.sh proofs/agda
      - name: Install checksum-pinned Agda 2.7.0.1 and pinned libraries
        run: bash scripts/setup-agda.sh
      - name: Cache interface files for this compiler and dependency set
        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
        with:
          path: |
            ${{ runner.temp }}/echo-agda/**/*.agdai
            proofs/agda/**/*.agdai
          key: agdai-${{ runner.os }}-2.7.0.1-stdlib8326c747-abszf486c299-${{ hashFiles('proofs/agda/**/*.agda') }}
          restore-keys: |
            agdai-${{ runner.os }}-2.7.0.1-stdlib8326c747-abszf486c299-
      - name: Typecheck shipped closure and headlines
        run: |
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Smoke.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/AuditSmoke.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/characteristic/All.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/examples/All.agda

  cold-check:
    # A separate runner and no restored interfaces: cached success never
    # substitutes for checking the shipped source with the pinned compiler.
    runs-on: ubuntu-24.04
    timeout-minutes: 30
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          persist-credentials: false
      - name: Install checksum-pinned Agda 2.7.0.1 and pinned libraries
        run: bash scripts/setup-agda.sh
      - name: Cold typecheck shipped closure and headlines
        run: |
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/All.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/Smoke.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/AuditSmoke.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/characteristic/All.agda
          agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/examples/All.agda

  experimental:
    name: Experimental echo-additive
    runs-on: ubuntu-24.04
    timeout-minutes: 30
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          persist-credentials: false
      - name: Install checksum-pinned Agda 2.7.0.1 and pinned libraries
        run: bash scripts/setup-agda.sh
      - name: Check experimental aggregate coverage
        run: bash scripts/check-experimental-aggregate.sh
      - name: Typecheck experimental closure on its own signal
        run: agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/experimental/echo-additive/All.agda

  narrowing:
    name: Bit-narrowing exhibit
    runs-on: ubuntu-24.04
    timeout-minutes: 30
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          persist-credentials: false
      - name: Install checksum-pinned Agda 2.7.0.1 and pinned libraries
        run: bash scripts/setup-agda.sh
      - name: Typecheck narrowing closure on its own signal
        run: agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --without-K --cubical-compatible -i proofs/agda proofs/agda/NarrowingSmoke.agda

  cubical:
    name: Cubical epi/mono profile
    runs-on: ubuntu-24.04
    timeout-minutes: 30
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          persist-credentials: false
      - name: Install checksum-pinned Agda 2.7.0.1 and pinned libraries
        run: bash scripts/setup-agda.sh
      - name: Typecheck isolated full-Cubical profile
        run: agda --no-libraries -i "$AGDA_STDLIB" -i "$ABSOLUTE_ZERO_AGDA" --ignore-interfaces --safe --cubical -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda