check.sh

#!/usr/bin/env bash
# Kernel-check the source modules in a clean, temporary import directory.
set -euo pipefail
package_dir="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)"
lean_bin="${LEAN_BIN:-lean}"
if ! command -v "$lean_bin" >/dev/null 2>&1; then
  echo "Lean not found. Set LEAN_BIN to the Lean 4.30.0 executable." >&2
  exit 2
fi
if [[ -n "${FPRD_LEAN_PRELOAD:-}" ]]; then
  export LD_PRELOAD="${FPRD_LEAN_PRELOAD}${LD_PRELOAD:+:$LD_PRELOAD}"
fi
"$lean_bin" --version
modules=(Fragments Contexts Adaptive Summaries Examples Audit)
python3 - "$package_dir" "${modules[@]}" <<'PY'
import pathlib, re, sys
root = pathlib.Path(sys.argv[1])

def code_only(text):
    # Strip nested Lean block comments, line comments and string literals.
    out, i, depth, string = [], 0, 0, False
    while i < len(text):
        if depth:
            if text.startswith('/-', i): depth += 1; i += 2
            elif text.startswith('-/', i): depth -= 1; i += 2
            else: out.append('\n' if text[i] == '\n' else ' '); i += 1
        elif string:
            if text[i] == '\\': i += 2
            elif text[i] == '"': string = False; i += 1
            else: out.append('\n' if text[i] == '\n' else ' '); i += 1
        elif text.startswith('/-', i): depth = 1; out.append(' '); i += 2
        elif text.startswith('--', i):
            j = text.find('\n', i)
            i = len(text) if j < 0 else j
        elif text[i] == '"': string = True; out.append(' '); i += 1
        else: out.append(text[i]); i += 1
    return ''.join(out)

for name in sys.argv[2:]:
    path = root / (name + '.lean')
    if not path.is_file(): raise SystemExit(f'Missing required module: {path}')
    code = code_only(path.read_text())
    bad = re.search(r'\b(sorry|admit|axiom)\b', code)
    if bad:
        line = code.count('\n', 0, bad.start()) + 1
        raise SystemExit(f'Forbidden proof-hole/axiom token: {path.name}:{line}: {bad[0]}')
print('Source guard: no sorry, admit, or custom axiom declarations.')
PY
build_dir="$(mktemp -d "${TMPDIR:-/tmp}/fprd-boundary-check.XXXXXX")"
trap 'rm -rf -- "$build_dir"' EXIT
export LEAN_PATH="$build_dir${LEAN_PATH:+:$LEAN_PATH}"
cd -- "$package_dir"
for module in "${modules[@]}"; do
  printf 'Checking %s.lean\n' "$module"
  "$lean_bin" -DwarningAsError=true -o "$build_dir/$module.olean" "$module.lean"
done
printf 'All required source modules passed Lean kernel checking.\n'