live-provers.yml

# SPDX-License-Identifier: MPL-2.0
# ECHIDNA — Live-Prover CI
#
# Exercises real prover binaries against canonical micro-goals. Complements
# rust-ci.yml (which runs mock tests on every PR) with live-subprocess coverage.
#
# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md + manifests/live-provers.scm):
#   T1 — trivial    — every PR + push to main
#   T2 — build      — nightly
#   T3 — container  — weekly
#   T4 — niche      — quarterly, allow-fail
#
# Reproducibility paths (both tried; at least one must succeed):
#   1. Guix manifest (PRIMARY, per project CLAUDE.md): manifests/live-provers.scm
#   2. apt-get (expedient bootstrap for T1 only):       jobs below
#
# (Nix flake removed 2026-06-01 per estate-wide nix-deprecation directive;
# Guix is the sole reproducible-build primary.)

name: Live Provers

on:
  push:
    branches: [main]
  pull_request:
    branches: [main]
  schedule:
    - cron: '0 3 * * *'    # Tier-2 nightly at 03:00 UTC
    - cron: '0 5 * * 0'    # Tier-3 weekly  Sunday 05:00 UTC
    - cron: '0 6 1 */3 *'  # Tier-4 quarterly 1st of Jan/Apr/Jul/Oct 06:00 UTC
  workflow_dispatch:
    inputs:
      tier:
        description: 'Which tier to run (1|2|3|4|all)'
        required: false
        default: '1'

# Cause-B mitigation (#77): cancel superseded runs so stacked pushes
# to the same ref don't pile up identical jobs in the queue.
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

permissions:
  contents: read

env:
  CARGO_TERM_COLOR: always
  RUST_BACKTRACE: 1
  ECHIDNA_LIVE_PROVERS: '1'

jobs:

  # ============================================================================
  # Tier 1 — every PR.  Apt-installable provers.  Must stay green.
  # ============================================================================
  tier1:
    name: T1 / ${{ matrix.backend }}
    if: github.event_name != 'schedule' || github.event.schedule == '0 3 * * *'
    runs-on: ubuntu-latest
    timeout-minutes: 20
    strategy:
      fail-fast: false
      matrix:
        backend:
          - z3
          - cvc5
          - vampire
          - eprover
          - spass
          - alt-ergo
          - glpk
          - minizinc
          - chuffed
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Install Rust
        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable

      - name: Cache Cargo
        uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2

      - name: Provision prover (${{ matrix.backend }})
        run: |
          set -euo pipefail
          # Retry apt-get update once on mirror failure before proceeding.
          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
          case "${{ matrix.backend }}" in
            z3)         sudo apt-get install -y --fix-missing z3 ;;
            cvc5)       # Since cvc5 1.2.0 releases ship as a zip with the binary at
                        # bin/cvc5; the old bare `cvc5-Linux-static` asset no longer exists.
                        curl -sSL --max-time 120 -o /tmp/cvc5.zip \
                          https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.3/cvc5-Linux-x86_64-static.zip
                        unzip -j -o /tmp/cvc5.zip 'cvc5-Linux-x86_64-static/bin/cvc5' -d /tmp
                        sudo install -m 0755 /tmp/cvc5 /usr/local/bin/cvc5 ;;
            vampire)    # Asset was renamed from vampire-Linux-x86_64.zip to
                        # vampire-Linux-X64.zip starting with v5.x; zip contains
                        # a single file named `vampire` at the root.
                        curl -sSL --max-time 120 -o /tmp/vampire.zip \
                          https://github.com/vprover/vampire/releases/download/v5.0.1/vampire-Linux-X64.zip
                        unzip -j -o /tmp/vampire.zip -d /tmp
                        sudo install -m 0755 /tmp/vampire /usr/local/bin/vampire ;;
            eprover)    sudo apt-get install -y --fix-missing eprover ;;
            spass)      sudo apt-get install -y --fix-missing spass ;;
            alt-ergo)   # alt-ergo is not in the Ubuntu 24.04 (noble) apt repos.
                        # Install the prebuilt musl static binary from OCamlPro's
                        # GitHub releases instead.
                        curl -sSL --max-time 120 -o /tmp/alt-ergo \
                          https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.3/alt-ergo-v2.6.3-x86_64-linux-musl
                        sudo install -m 0755 /tmp/alt-ergo /usr/local/bin/alt-ergo ;;
            glpk)       sudo apt-get install -y --fix-missing glpk-utils ;;
            minizinc)   sudo apt-get install -y --fix-missing minizinc ;;
            chuffed)    sudo apt-get install -y --fix-missing minizinc # chuffed bundled with minizinc-ide on recent ubuntu
                        ;;
          esac
          "${{ matrix.backend }}" --version 2>/dev/null || "${{ matrix.backend }}" --help 2>/dev/null || true

      - name: Run live test for ${{ matrix.backend }}
        run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}

  # ============================================================================
  # Tier 1 reproducibility check — ensure Guix manifest actually resolves.
  # Allow-fail: this is additional proof, not a gate (Guix-on-Ubuntu is flaky
  # without dedicated setup).
  # ============================================================================
  tier1-guix-reproducibility:
    name: T1 Guix manifest check
    if: github.event_name != 'schedule'
    runs-on: ubuntu-latest
    timeout-minutes: 20
    continue-on-error: true
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
      - name: Install Guix
        run: |
          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
          sudo apt-get install -y --fix-missing guix
      - name: Resolve manifest (doesn't run tests — just proves the .scm parses)
        run: |
          guix describe || true
          guix package -m manifests/live-provers.scm --dry-run || \
            echo "NOTE: Guix manifest resolution failed — non-blocking reproducibility signal."

  # ============================================================================
  # Tier 2 — nightly.  Larger build-from-source provers.
  # ============================================================================
  tier2:
    name: T2 / ${{ matrix.backend }}
    if: github.event_name == 'schedule' && github.event.schedule == '0 3 * * *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '2' || inputs.tier == 'all'))
    runs-on: ubuntu-latest
    timeout-minutes: 20
    strategy:
      fail-fast: false
      matrix:
        backend:
          - coq
          - agda
          - idris2
          - lean4
          - isabelle
          - why3
          - dafny
          - fstar
          - hol-light
          - tlaps
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
      - name: Install Rust
        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
      - name: Cache Cargo
        uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2
      - name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
        continue-on-error: true
        run: |
          set -euo pipefail
          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
          case "${{ matrix.backend }}" in
            coq)
              sudo apt-get install -y --fix-missing coq
              ;;
            agda)
              sudo apt-get install -y --fix-missing agda
              ;;
            idris2)
              # Idris2 v0.8.0 has no pre-built Linux release binary (assets array
              # is empty on the GitHub release). Try apt first (available as idris2
              # in Ubuntu 24.04 universe); fall back to building from the source
              # archive.  The old idris2-src-latest.tgz URL is a 404 on releases
              # without assets — use the GitHub archive API instead, which always
              # resolves for any tag.
              sudo apt-get install -y --fix-missing idris2 2>/dev/null || {
                IDRIS2_VER="v0.8.0"
                sudo apt-get install -y --fix-missing chezscheme make libgmp-dev
                curl -fsSL --max-time 300 --retry 2 \
                  -o /tmp/idris2.tar.gz \
                  "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_VER}.tar.gz"
                mkdir -p /tmp/idris2-src
                tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1
                (cd /tmp/idris2-src && make bootstrap SCHEME=scheme && sudo make install PREFIX=/usr/local)
              }
              ;;
            lean4)
              # elan bootstraps the Lean toolchain manager and downloads lean4:stable.
              # --max-time guards the pipe against a stalled download.
              curl -sSL --max-time 120 \
                https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
                | sh -s -- -y --default-toolchain leanprover/lean4:stable
              echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
              ;;
            isabelle)
              # Isabelle2024 tarball (~500MB); nightly only.
              # --retry 3 + --max-time 600 guard the large download.
              # find locates the binary regardless of extracted dir name,
              # so the symlink survives a future Isabelle2025 release.
              curl -fsSL --max-time 600 --retry 3 --retry-delay 15 \
                -o /tmp/isabelle.tar.gz \
                https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
              sudo mkdir -p /opt/isabelle
              sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
              ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)"
              [ -n "$ISABELLE_BIN" ] && sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle
              ;;
            why3)
              sudo apt-get install -y --fix-missing why3
              ;;
            dafny)
              # Dafny 4.x is distributed as a .NET global tool.
              # ubuntu-latest ships dotnet-sdk-8.0 in the default image; install
              # via apt only if absent (--fix-missing guards against mirror lag).
              command -v dotnet >/dev/null 2>&1 || \
                sudo apt-get install -y --fix-missing dotnet-sdk-8.0
              dotnet tool install --global Dafny
              echo "$HOME/.dotnet/tools" >> "$GITHUB_PATH"
              ;;
            fstar)
              # F* ships prebuilt Linux binaries; binary is fstar.exe even on Linux.
              # Asset naming changed in 2025: fstar-linux_x86_64.tar.gz (old) →
              # fstar-v{version}-Linux-x86_64.tar.gz (new). Pinned to v2026.04.17.
              # Update FSTAR_VER when a newer release lands.
              # find locates fstar.exe regardless of extracted directory layout.
              FSTAR_VER="v2026.04.17"
              curl -fsSL --max-time 300 --retry 2 \
                -o /tmp/fstar.tar.gz \
                "https://github.com/FStarLang/FStar/releases/download/${FSTAR_VER}/fstar-${FSTAR_VER}-Linux-x86_64.tar.gz"
              sudo mkdir -p /opt/fstar
              sudo tar xzf /tmp/fstar.tar.gz -C /opt/fstar
              FSTAR_BIN="$(find /opt/fstar -type f -name fstar.exe | head -n 1)"
              [ -n "$FSTAR_BIN" ] && sudo ln -sf "$FSTAR_BIN" /usr/local/bin/fstar.exe
              ;;
            hol-light)
              # No prebuilt binary; opam build is ~20min and pulls camlp5.
              # Deferred to Wave-3 (container-based provisioning) per the
              # production-wiring plan.
              echo "hol-light deferred to Wave-3 container provisioning"
              exit 0
              ;;
            tlaps)
              # tlapm 1.5.0 ships a makeself .bin installer (not .sh).
              # The installer installs to /usr/local/lib/tlaps and links
              # tlapm into /usr/local/bin — no --prefix needed or supported.
              # find is a safety net for any layout variation.
              curl -fsSL --max-time 120 \
                -o /tmp/tlaps.bin \
                "https://github.com/tlaplus/tlapm/releases/download/202210041448/tlaps-1.5.0-x86_64-linux-gnu-inst.bin"
              chmod +x /tmp/tlaps.bin
              sudo /tmp/tlaps.bin
              command -v tlapm >/dev/null 2>&1 || {
                TLAPM_BIN="$(find /usr /opt -type f -name tlapm 2>/dev/null | head -n 1)"
                [ -n "$TLAPM_BIN" ] && sudo ln -sf "$TLAPM_BIN" /usr/local/bin/tlapm
              }
              ;;
          esac
          # Best-effort version probe for the matrix log.
          case "${{ matrix.backend }}" in
            fstar)     fstar.exe --version || true ;;
            tlaps)     tlapm --version || true ;;
            hol-light) true ;;
            *)         "${{ matrix.backend }}" --version 2>/dev/null || true ;;
          esac
      - name: Run live test for ${{ matrix.backend }}
        run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}

  # ============================================================================
  # Tier 3 — weekly.  Heavier upstream provers, best-effort provisioning.
  #
  # Backends grouped as:
  #   A — live-provisioned today via apt / upstream tarball (tamarin, proverif,
  #       metamath, twelf, ortools).  Version-check runs, skip-if-absent.
  #   B — heavy-build deferred (hol4, acl2, scip) and proprietary (imandra).
  #       Provisioning step emits a skip note; test step runs the suite with
  #       continue-on-error so the matrix stays green and the binary's absence
  #       is logged as SKIP by the suite's `which` probe.
  # ============================================================================
  tier3:
    name: T3 / ${{ matrix.backend }}
    if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
    runs-on: ubuntu-latest
    timeout-minutes: 20
    continue-on-error: true
    strategy:
      fail-fast: false
      matrix:
        backend:
          - tamarin
          - proverif
          - metamath
          - twelf
          - ortools
          - hol4
          - acl2
          - scip
          - imandra
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
      - name: Install Rust
        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
      - name: Cache Cargo
        uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2
      - name: Provision ${{ matrix.backend }} (best-effort)
        continue-on-error: true
        run: |
          set -euo pipefail
          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
          case "${{ matrix.backend }}" in
            tamarin)
              # Tamarin publishes prebuilt Linux x86_64 tarballs.
              curl -fsSL -o /tmp/tamarin.tar.gz \
                https://github.com/tamarin-prover/tamarin-prover/releases/latest/download/tamarin-prover-linux64-ubuntu.tar.gz || \
                curl -fsSL -o /tmp/tamarin.tar.gz \
                https://github.com/tamarin-prover/tamarin-prover/releases/download/1.10.0/tamarin-prover-1.10.0-linux64-ubuntu.tar.gz
              sudo mkdir -p /opt/tamarin
              sudo tar xzf /tmp/tamarin.tar.gz -C /opt/tamarin
              # The tarball lays down tamarin-prover directly or in a version dir; link whichever we find.
              TAMARIN_BIN="$(find /opt/tamarin -type f -name tamarin-prover | head -n 1)"
              [ -n "$TAMARIN_BIN" ] && sudo ln -sf "$TAMARIN_BIN" /usr/local/bin/tamarin-prover
              ;;
            proverif)
              # ProVerif is in the Ubuntu/Debian main repos.
              sudo apt-get install -y proverif
              ;;
            metamath)
              # metamath-exe is small; apt-installable on Ubuntu with build fallback.
              sudo apt-get install -y metamath || {
                sudo apt-get install -y build-essential git autoconf automake
                git clone --depth=1 https://github.com/metamath/metamath-exe.git /tmp/mm
                (cd /tmp/mm && ./build.sh) || \
                  (cd /tmp/mm && autoreconf -i && ./configure && make)
                sudo install -m 0755 /tmp/mm/metamath /usr/local/bin/metamath
              }
              ;;
            twelf)
              # Twelf is in Debian with SML/NJ; on Ubuntu it may live in universe.
              sudo apt-get install -y twelf || \
                echo "twelf unavailable via apt on this runner; test will SKIP."
              ;;
            ortools)
              # Google OR-Tools ships prebuilt Linux tarballs.  The binary we
              # expose to echidna is a small wrapper that invokes the solver CLI.
              OR_URL="https://github.com/google/or-tools/releases/latest/download/or-tools_amd64_ubuntu-22.04_cpp_v9.11.4210.tar.gz"
              curl -fsSL -o /tmp/ortools.tar.gz "$OR_URL" || {
                echo "OR-Tools tarball unavailable at expected URL; test will SKIP."
                exit 0
              }
              sudo mkdir -p /opt/ortools
              sudo tar xzf /tmp/ortools.tar.gz -C /opt/ortools --strip-components=1
              # Echidna's ORTools backend invokes `ortools_solve`.  The release
              # ships `bin/solve` or similar; create the expected symlink.
              OR_BIN="$(find /opt/ortools -type f \( -name ortools_solve -o -name solve \) | head -n 1)"
              [ -n "$OR_BIN" ] && sudo ln -sf "$OR_BIN" /usr/local/bin/ortools_solve
              ;;
            hol4)
              # HOL4 requires Poly/ML and a full tree build (~15min+); defer to
              # container provisioning.  Test step will SKIP on this runner.
              echo "hol4: heavy Poly/ML build deferred to Containerfile provisioning."
              ;;
            acl2)
              # ACL2 requires a Common Lisp image (CCL/SBCL) and a 10min+ build;
              # defer to container provisioning.  Test step will SKIP.
              echo "acl2: heavy SBCL+image build deferred to Containerfile."
              ;;
            scip)
              # SCIP Optimization Suite needs a full cmake build (~10min).  The
              # upstream tarball requires a form-gated download, so CI defers to
              # Containerfile provisioning.  Test step will SKIP.
              echo "scip: form-gated upstream tarball; deferred to Containerfile."
              ;;
            imandra)
              # Imandra is proprietary; no public Linux binary.  Handled via
              # vendor-supplied container where a licence is available.
              echo "imandra: proprietary; no public CI provisioning available."
              ;;
          esac
          # Best-effort version probe for the matrix log.
          case "${{ matrix.backend }}" in
            tamarin)    tamarin-prover --version 2>&1 | head -n 1 || true ;;
            proverif)   proverif --version 2>&1 | head -n 1 || true ;;
            metamath)   echo exit | metamath 2>&1 | head -n 1 || true ;;
            twelf)      twelf-server --help 2>&1 | head -n 1 || true ;;
            ortools)    ortools_solve --help 2>&1 | head -n 1 || true ;;
            hol4|acl2|scip|imandra) true ;;
          esac
      - name: Run live test for ${{ matrix.backend }}
        run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}

  # ============================================================================
  # Tier 4 — quarterly, best-effort / allow-fail.
  # ============================================================================
  tier4:
    name: T4 niche provers
    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
    runs-on: ubuntu-latest
    timeout-minutes: 20
    continue-on-error: true
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
      - name: Announce Wave-4 TODO
        run: |
          echo "Tier-4 backends (Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL,"
          echo "ViPER, NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy) are"
          echo "retained as mock-only unless a maintainer volunteers a Containerfile."

  # ============================================================================
  # Tier 4 GPU — quarterly, best-effort / allow-fail.
  # GPUVerify and Faial require CUDA SDK or OpenCL runtime; provisioning is
  # deferred to a developer workstation or GPU-capable CI runner.
  # ============================================================================
  tier4-gpu:
    name: T4 / ${{ matrix.backend }}
    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
    runs-on: ubuntu-latest
    timeout-minutes: 20
    continue-on-error: true
    strategy:
      fail-fast: false
      matrix:
        backend:
          - gpuverify
          - faial
    steps:
      - name: Checkout
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
      - name: Install Rust
        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
      - name: Cache Cargo
        uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2
      - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
        continue-on-error: true
        run: |
          case "${{ matrix.backend }}" in
            gpuverify)
              echo "GPUVerify requires CUDA SDK + .NET; deferred to developer workstation."
              echo "See: https://github.com/mc-imperial/gpuverify"
              ;;
            faial)
              echo "Faial requires CUDA/OpenCL headers; install via: cargo install faial"
              echo "See: https://github.com/elliotttate/faial"
              ;;
          esac
      - name: Run live version check (SKIP if binary absent)
        continue-on-error: true
        run: cargo test --test live_prover_suite --features live-provers -- --nocapture live_${{ matrix.backend }}_version