ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:

env:
  CARGO_TERM_COLOR: always

jobs:
  # -----------------------------------------------------------------------
  # Primary build & test (default features)
  # -----------------------------------------------------------------------
  test:
    name: Build & Test
    runs-on: ubuntu-latest
    env:
      CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}
    steps:
      - uses: actions/checkout@v4

      - name: Install system dependencies
        run: sudo apt-get update && sudo apt-get install -y python3-dev

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

      - name: Cache cargo
        uses: Swatinem/rust-cache@v2

      - name: Build
        run: cargo build --all-targets

      - name: Test
        run: cargo test

      - name: Install cargo-llvm-cov
        run: cargo install cargo-llvm-cov --locked

      - name: Generate coverage report
        run: cargo llvm-cov --all-features --lcov --output-path lcov.info

      - name: Upload coverage to Codecov
        if: env.CODECOV_TOKEN != ''
        uses: codecov/codecov-action@v5
        with:
          files: lcov.info

      - name: Gate (forbidden patterns + zero warnings)
        run: python3 verify_implementation.py

  # -----------------------------------------------------------------------
  # Release build — catches optimization-only errors
  # -----------------------------------------------------------------------
  release:
    name: Release Build
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install system dependencies
        run: sudo apt-get update && sudo apt-get install -y python3-dev

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

      - name: Cache cargo
        uses: Swatinem/rust-cache@v2

      - name: Build (release)
        run: cargo build --release

      - name: Test (release)
        run: cargo test --release

  # -----------------------------------------------------------------------
  # No-default-features build — proves zero PyO3/SQLite/LSP dependencies
  # -----------------------------------------------------------------------
  minimal-build:
    name: Build without optional features
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

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

      - name: Cache cargo
        uses: Swatinem/rust-cache@v2

      # No python3-dev installed here on purpose: this job proves the
      # no-default-features build has zero PyO3/SQLite/LSP dependencies.
      - name: Build
        run: cargo build --all-targets --no-default-features

      - name: Test
        run: cargo test --no-default-features

      - name: Check zero warnings
        run: cargo check --tests --no-default-features

  # -----------------------------------------------------------------------
  # WASM backend
  # -----------------------------------------------------------------------
  wasm-backend:
    name: Build & Test (wasm-backend feature)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install system dependencies
        run: sudo apt-get update && sudo apt-get install -y python3-dev

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

      - name: Cache cargo
        uses: Swatinem/rust-cache@v2

      - name: Build
        run: cargo build --all-targets --features wasm-backend

      - name: Test
        run: cargo test --features wasm-backend

  # -----------------------------------------------------------------------
  # Lint — format, clippy, audit, docs, all-features check
  # -----------------------------------------------------------------------
  lint:
    name: Format, Clippy & Audit
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install system dependencies
        run: sudo apt-get update && sudo apt-get install -y python3-dev

      - name: Install Rust
        uses: dtolnay/rust-toolchain@stable
        with:
          components: rustfmt, clippy

      - name: Cache cargo
        uses: Swatinem/rust-cache@v2

      # Format check is blocking — the codebase has been rustfmt'd.
      - name: Format check
        run: cargo fmt --check

      # Clippy with default features — correctness lints are blocking.
      - name: Clippy (default features)
        run: cargo clippy --all-targets -- -D clippy::correctness

      # Clippy with all features — catches wasm-backend code paths.
      - name: Clippy (all features)
        run: cargo clippy --all-targets --all-features -- -D clippy::correctness

      # Clippy with no default features — catches minimal-build code paths.
      - name: Clippy (no default features)
        run: cargo clippy --all-targets --no-default-features -- -D clippy::correctness

      # Zero compiler warnings on the main build path.
      - name: Check zero warnings (tests)
        run: cargo check --tests

      # Security audit of dependency tree.
      - name: Audit (cargo-audit)
        run: |
          cargo install cargo-audit --locked
          cargo audit

      # All-features compilation check.
      - name: Check all features
        run: cargo check --all-features

      # Documentation builds without errors.
      - name: Check docs
        run: cargo doc --no-deps

      # Documentation warnings are non-blocking but visible.
      - name: Doc warnings (info only)
        run: RUSTDOCFLAGS="-D warnings" cargo doc --no-deps 2>&1 || true

  # -----------------------------------------------------------------------
  # Lean formalization — verifies the formal specs compile
  # -----------------------------------------------------------------------
  lean:
    name: Lean Formalization
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install elan (Lean toolchain manager)
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:v4.16.0
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Build formal specs
        run: |
          cd spec/formal
          lake build