#!/usr/bin/env bash
set -euo pipefail

if [[ $# -ne 1 ]]; then
  echo "usage: $0 LEAN_PROJECT_DIRECTORY" >&2
  exit 2
fi
project=$(realpath "$1")
if [[ ! -f "$project/lakefile.toml" ]]; then
  echo "FAIL: $project has no lakefile.toml" >&2
  exit 2
fi

# Lean accepts `sorry` by inserting sorryAx.  Reject all common source-level
# escape hatches before invoking the kernel-backed build.  Dependency sources
# under .lake/packages are trusted Mathlib and intentionally excluded.
bad=$(find "$project" -path '*/.lake' -prune -o -name '*.lean' -type f -print0 \
  | xargs -0 grep -nE '\b(sorry|admit|axiom|opaque|unsafe)\b' || true)
if [[ -n "$bad" ]]; then
  echo "FAIL: forbidden proof escape hatch found:" >&2
  echo "$bad" >&2
  exit 1
fi

export PATH="$HOME/.elan/bin:$HOME/.cargo/bin:$PATH"
export LEAN_NUM_THREADS="${LEAN_NUM_THREADS:-28}"
(
  cd "$project"
  # A submitted fact must also verify in a fresh sandbox, where Lake's package
  # directory is absent. Resolve the pinned manifest and fetch Mathlib's signed
  # precompiled cache instead of relying on workspace symlinks.
  if [[ ! -d .lake/packages/mathlib ]]; then
    echo "INFO: bootstrapping pinned Lean dependencies"
    lake update
    lake exe cache get
  fi
  lake build
)
echo "PASS: sorry/admit/axiom-free Lean build"
