name: spec check

# Builds the Lean semantic master spec under spec/.
# This is an INTERNAL well-formedness gate (does the contract type-check?),
# NOT a spec-to-implementation conformance gate — implementations align to the
# contract by human review, not by CI. See repo README.

on:
  push:
  pull_request:
  workflow_dispatch:

jobs:
  spec-check:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5
      - uses: leanprover/lean-action@v1
        with:
          lake-package-directory: spec