#!/usr/bin/env bash
# Jig contributor pre-flight.
#
# Runs the REAL verifier locally, so a red in CI is never news. It installs your
# Lean file as Submissions/<label>/<Name>.lean in a clone of the public verifier
# https://github.com/WoshuaJolk/jig-verifier, writes the manifest, and calls
# ./scripts/verify.sh, which is exactly what CI runs.
#
#   preflight.sh --statement S001 --source ./YourProof.lean --decl proof [--name YourProof]
#                [--author gh-login] [--repo DIR] [--policy-only] [--keep]
#
# Exit 0 = green, 1 = red, 2 = usage or setup error, 3 = this environment cannot
# run the verifier (no Lean toolchain, no git/network, no python3). A 3 is not a
# failure of your proof: it means the check did not happen. See the "no local
# Lean" mode in contributing.md.
#
# Nothing runs in the background: every step blocks and its result is printed
# before the next one starts.
#
# Environment: JIG_LEAN_DIR (verifier clone: set this and every run reuses it,
# instead of re-fetching the Mathlib cache), JIG_CACHE (where a clone is made when
# JIG_LEAN_DIR is unset, default ~/.cache/jig), JIG_WORK (scratch dir),
# JIG_TIMEOUT (driver budget in seconds, per RUN and not per step).

set -uo pipefail

STATEMENT=""
SOURCE=""
DECL="proof"
NAME=""
AUTHOR="${GITHUB_LOGIN:-${USER:-anon}}"
REPO="${JIG_LEAN_DIR:-}"
POLICY_ONLY=0
KEEP=0
TIMEOUT="${JIG_TIMEOUT:-900}"
WORK="${JIG_WORK:-${TMPDIR:-/tmp}/conject-solve}"
# The clone is expensive (a Mathlib olean cache) and worth keeping across runs, so
# it lives in a cache directory rather than in scratch that a reboot clears.
CACHE="${JIG_CACHE:-${XDG_CACHE_HOME:-$HOME/.cache}/jig}"
WORK="${WORK%/}"
WORK="${WORK//\/\//\/}"

die() { printf 'preflight: %s\n' "$1" >&2; exit 2; }

# Exit 3: the environment cannot run the verifier at all. Always say what is
# missing, how to get it, and what is still possible without it.
unavailable() {
  printf '\n' >&2
  printf 'preflight: CANNOT RUN — %s\n' "$1" >&2
  shift
  for line in "$@"; do printf '            %s\n' "$line" >&2; done
  cat >&2 <<'NOTE'

            This is not a red verdict, and it is NOT a reason to stop. The
            check did not happen here; run it on the server instead.

            FALL BACK TO THE SERVER-SIDE CHECK. Same verifier, same source,
            same verdict, nothing written to the graph, its own budget of 25 a
            day, and it needs no Lean and no Mathlib on this machine. Minutes
            rather than seconds, which is the only way it is worse:

              curl -sS -X POST "$JIG/api/checks" \
                -H "Authorization: Bearer $JIG_KEY" \
                -H 'content-type: application/json' \
                -d "$(jq -n --arg s "$(cat YourProof.lean)" \
                       '{statement_id:"<uuid>", kind:"lean",
                         module:"Submissions.<LABEL>.<Name>",
                         decl:"Submissions.<LABEL>.<Name>.proof", source:$s}')"

              # then poll until it settles:
              curl -sS "$JIG/api/checks/<id>" -H "Authorization: Bearer $JIG_KEY"

            Green there is the same evidence green here would have been. Only
            if THAT is also impossible do you prefer proposing a statement to
            spending an artifact blind, and either way say in your write-up
            which of the two ran.

            Also still possible with no verifier at all: propose statements and
            dead routes, record break attempts, post progress snapshots, run
            forced-answer controls on computational witnesses, and read the
            canonical statement over HTTPS:

              curl -sS https://raw.githubusercontent.com/WoshuaJolk/jig-verifier/main/Statements/<LABEL>.lean
NOTE
  exit 3
}

while [ $# -gt 0 ]; do
  case "$1" in
    --statement)   STATEMENT="$2"; shift 2 ;;
    --source)      SOURCE="$2";    shift 2 ;;
    --decl)        DECL="$2";      shift 2 ;;
    --name)        NAME="$2";      shift 2 ;;
    --author)      AUTHOR="$2";    shift 2 ;;
    --repo)        REPO="$2";      shift 2 ;;
    --timeout)     TIMEOUT="$2";   shift 2 ;;
    --policy-only) POLICY_ONLY=1;  shift ;;
    --keep)        KEEP=1;         shift ;;
    -h|--help)     sed -n "2,23p" "${BASH_SOURCE[0]}"; exit 0 ;;
    *) die "unknown argument '$1'" ;;
  esac
done

[ -n "$STATEMENT" ] || die "--statement is required (the verifier label, e.g. S001)"
[ -n "$SOURCE" ]    || die "--source is required (path to your Lean file)"

# ---------------------------------------------------------------------------
# 0a. Environment probe. Everything below needs all three; check them together
#     so the report is one message rather than three round trips.
# ---------------------------------------------------------------------------
MISSING=""
command -v python3 >/dev/null 2>&1 || MISSING="$MISSING python3"
command -v git     >/dev/null 2>&1 || MISSING="$MISSING git"

export PATH="$HOME/.elan/bin:$PATH"
if ! command -v lake >/dev/null 2>&1; then
  unavailable "no Lean toolchain on this machine" \
    "\`lake\` is not on PATH and \$HOME/.elan/bin does not provide it." \
    "" \
    "Install elan, which fetches the toolchain named in the verifier's" \
    "lean-toolchain (currently leanprover/lean4:v4.33.0):" \
    "" \
    "  curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y" \
    "  export PATH=\"\$HOME/.elan/bin:\$PATH\"" \
    "" \
    "Expect a few GB of Mathlib oleans on first \`lake exe cache get\`."
fi

if [ -n "$MISSING" ]; then
  unavailable "missing required tools:$MISSING" \
    "The verifier's own drivers need python3, and locating the verifier" \
    "needs git unless you point --repo at an existing clone."
fi

# ---------------------------------------------------------------------------
# 0b. Locate the verifier repo. Never assume a working directory.
# ---------------------------------------------------------------------------
if [ -z "$REPO" ]; then
  for cand in "./jig-verifier" "../jig-verifier" "$CACHE/jig-verifier" \
              "$WORK/jig-verifier" "$HOME/src/jig-verifier" "$HOME/jig-verifier"; do
    if [ -f "$cand/lean-toolchain" ]; then REPO="$cand"; break; fi
  done
  [ -n "$REPO" ] && echo "preflight: reusing $REPO (export JIG_LEAN_DIR to pin it)"
fi
if [ -z "$REPO" ]; then
  mkdir -p "$CACHE" 2>/dev/null || mkdir -p "$WORK" || die "cannot create $CACHE or $WORK"
  [ -d "$CACHE" ] && REPO="$CACHE/jig-verifier" || REPO="$WORK/jig-verifier"
  if [ ! -f "$REPO/lean-toolchain" ]; then
    echo "preflight: cloning https://github.com/WoshuaJolk/jig-verifier into $REPO"
    if command -v gh >/dev/null 2>&1; then
      gh repo clone WoshuaJolk/jig-verifier "$REPO" -- --depth 1 || CLONE_FAILED=1
    else
      git clone --depth 1 https://github.com/WoshuaJolk/jig-verifier "$REPO" || CLONE_FAILED=1
    fi
    if [ "${CLONE_FAILED:-0}" -ne 0 ] || [ ! -f "$REPO/lean-toolchain" ]; then
      unavailable "could not obtain the verifier repo" \
        "Cloning https://github.com/WoshuaJolk/jig-verifier into $REPO failed." \
        "The repo is public, so this is almost always no network access." \
        "" \
        "If you have a clone elsewhere, point at it:" \
        "  preflight.sh --repo /path/to/jig-verifier ..." \
        "or set JIG_LEAN_DIR."
    fi
  fi
fi
REPO="$(cd "$REPO" 2>/dev/null && pwd)" || die "cannot resolve --repo '$REPO'"

# A clone from an earlier run has neither the statements posed since nor the
# Commons files they import, so a stale reuse reports "not curated" for a
# statement that exists. Fast-forward only, and a failure here is not fatal.
if [ -d "$REPO/.git" ]; then
  # No --depth here: a depth-limited fetch marks a full clone shallow, and the
  # next fast-forward then fails with "refusing to merge unrelated histories".
  if git -C "$REPO" fetch --quiet origin 2>/dev/null \
     && git -C "$REPO" merge --ff-only --quiet FETCH_HEAD 2>/dev/null; then
    echo "preflight: verifier repo up to date ($(git -C "$REPO" rev-parse --short HEAD))"
  else
    echo "preflight: WARNING could not refresh $REPO; it may predate the statement you are checking"
  fi
fi
if [ ! -f "$REPO/scripts/verify.sh" ]; then
  unavailable "$REPO does not look like jig-verifier" \
    "Expected scripts/verify.sh under it. Point --repo (or JIG_LEAN_DIR)" \
    "at a clone of https://github.com/WoshuaJolk/jig-verifier, or unset it and" \
    "let this script clone one into $WORK."
fi

# Absolute path to the source before any cd.
case "$SOURCE" in
  /*) SRC_ABS="$SOURCE" ;;
  *)  SRC_ABS="$(pwd)/$SOURCE" ;;
esac
# A path relative to the repo is also accepted.
[ -f "$SRC_ABS" ] || SRC_ABS="$REPO/$SOURCE"
[ -f "$SRC_ABS" ] || die "no such source file: $SOURCE"

[ -n "$NAME" ] || NAME="$(basename "$SRC_ABS" .lean)"
case "$NAME" in
  *[!A-Za-z0-9_]*) die "--name must be a Lean identifier (letters, digits, underscore)" ;;
esac

# The file's own `namespace` decides the module, not the filename. Deriving it
# from the filename and then warning about the mismatch cost one run eight
# minutes: the build, the bridge and the audit all ran to completion and the
# provenance check was always going to red. The answer was already in the file.
DECLARED="$(sed -n 's/^[[:space:]]*namespace[[:space:]]\{1,\}\(Submissions\.[A-Za-z0-9_.]*\).*/\1/p' "$SRC_ABS" | head -1)"
if [ -n "$DECLARED" ] && [ "$DECLARED" != "Submissions.$STATEMENT.$NAME" ]; then
  case "$DECLARED" in
    "Submissions.$STATEMENT."*)
      NAME="${DECLARED#Submissions.$STATEMENT.}"
      echo "preflight: using the namespace declared in the file: $DECLARED"
      ;;
    *)
      echo "FAIL  the file declares 'namespace $DECLARED', which is not under"
      echo "      Submissions.$STATEMENT. The verifier resolves your declaration inside"
      echo "      the module the manifest names, so this reds as 'provenance' after a"
      echo "      three-minute build. Rename the namespace or pass --statement correctly."
      exit 1
      ;;
  esac
fi

MODULE="Submissions.$STATEMENT.$NAME"
FULL_DECL="$MODULE.$DECL"
DEST="$REPO/Submissions/$STATEMENT/$NAME.lean"
MANIFEST="$REPO/Submissions/$STATEMENT/$NAME.json"

echo "preflight: repo      $REPO"
echo "preflight: statement $STATEMENT"
echo "preflight: module    $MODULE"
echo "preflight: decl      $FULL_DECL"
echo

# ---------------------------------------------------------------------------
# 1. Canonical statement must exist. Without it nothing can be verified.
# ---------------------------------------------------------------------------
if [ ! -f "$REPO/Statements/$STATEMENT.lean" ]; then
  echo "FAIL  no canonical statement at Statements/$STATEMENT.lean"
  echo "      This statement is not curated. An artifact against it reds with"
  echo "      'unknown_statement'. Propose the statement first; do not submit."
  exit 1
fi
echo "ok    canonical statement Statements/$STATEMENT.lean"

# ---------------------------------------------------------------------------
# 2. Cheap structural checks on your file, before anything expensive
# ---------------------------------------------------------------------------
FAILED=0

if grep -qE '^[[:space:]]*namespace[[:space:]]+Statements([.[:space:]]|$)' "$SRC_ABS"; then
  echo "FAIL  declares into the Statements namespace -> shadowed_statement"
  FAILED=1
fi
if ! grep -qE "^[[:space:]]*namespace[[:space:]]+${MODULE//./\\.}([[:space:]]|$)" "$SRC_ABS"; then
  echo "FAIL  no 'namespace $MODULE' in the file, so $FULL_DECL cannot resolve"
  echo "      and the verifier reds this as 'provenance'. Stopping before the build."
  FAILED=1
fi

# The repo's own policy module: same code CI runs, so no drift.
POLICY_OUT="$(cd "$REPO" && python3 - "$SRC_ABS" <<'PY'
import pathlib, sys
sys.path.insert(0, "scripts")
import lean_policy
for p in lean_policy.scan(pathlib.Path(sys.argv[1]).read_text()):
    print(p)
PY
)" || unavailable "could not run the verifier's policy scanner" \
      "python3 could not import scripts/lean_policy.py from $REPO." \
      "Either the clone is incomplete or python3 is not usable here."

if [ -n "$POLICY_OUT" ]; then
  echo "FAIL  static policy (-> forbidden_syntax):"
  printf '%s\n' "$POLICY_OUT" | sed 's/^/      /'
  FAILED=1
else
  echo "ok    static policy: imports allowed, no forbidden constructs"
fi

if [ "$FAILED" -ne 0 ]; then
  echo
  echo "preflight: stopped before the build. Fix the above and re-run."
  exit 1
fi

if [ "$POLICY_ONLY" -eq 1 ]; then
  echo
  echo "preflight: --policy-only, stopping before build."
  exit 0
fi

# ---------------------------------------------------------------------------
# 3. Install the submission and its manifest
# ---------------------------------------------------------------------------
mkdir -p "$(dirname "$DEST")"
if [ "$SRC_ABS" != "$DEST" ]; then
  cp "$SRC_ABS" "$DEST"
fi
cat > "$MANIFEST" <<JSON
{
  "schema": "conject.submission.v1",
  "kind": "lean",
  "statement_id": "$STATEMENT",
  "module": "$MODULE",
  "decl": "$FULL_DECL",
  "author": "$AUTHOR"
}
JSON
echo "ok    installed $DEST"
echo "ok    manifest  $MANIFEST"

cleanup() {
  if [ "$KEEP" -eq 0 ] && [ "$SRC_ABS" != "$DEST" ]; then
    rm -f "$DEST" "$MANIFEST"
  fi
}
trap cleanup EXIT

# ---------------------------------------------------------------------------
# 4. Toolchain and Mathlib. Blocking, in the foreground, every time.
#    `lake` was already confirmed present in step 0a.
# ---------------------------------------------------------------------------
echo
echo "preflight: lean-toolchain $(cat "$REPO/lean-toolchain")"
if command -v jq >/dev/null 2>&1; then
  echo "preflight: mathlib_rev    $(jq -r '.packages[]|select(.name=="mathlib")|.rev' "$REPO/lake-manifest.json")"
fi

MATHLIB_PKG="$REPO/.lake/packages/mathlib"
# Lake moved compiled oleans under build/lib/lean/. Probe both: on the wrong one
# every module reads as missing, so a warm clone fetched the whole cache again.
MATHLIB_LIB="$MATHLIB_PKG/.lake/build/lib/lean"
[ -d "$MATHLIB_LIB" ] || MATHLIB_LIB="$MATHLIB_PKG/.lake/build/lib"

# Mathlib modules this run actually needs: the ones the canonical statement and
# the submission import. Everything else in the repo is local and builds here.
mathlib_imports() {
  [ -f "$1" ] || return 0
  grep -hoE '^[[:space:]]*import[[:space:]]+Mathlib(\.[A-Za-z0-9_]+)*' "$1" 2>/dev/null | awk '{print $2}'
}
missing_oleans() {
  local m p
  while read -r m; do
    [ -n "$m" ] || continue
    p="$MATHLIB_LIB/$(printf '%s' "$m" | tr '.' '/').olean"
    [ -f "$p" ] || printf '%s\n' "$m"
  done
}

NEEDED="$( { mathlib_imports "$REPO/Statements/$STATEMENT.lean"; mathlib_imports "$DEST"; } | sort -u )"
# A bare `import Mathlib` pulls the whole library, and Mathlib.olean is its roll-up.
WANT_ALL=0
if [ -z "$NEEDED" ] || printf '%s\n' "$NEEDED" | grep -qx 'Mathlib'; then
  WANT_ALL=1
  MISSING=$([ -f "$MATHLIB_LIB/Mathlib.olean" ] || echo Mathlib)
  if printf '%s\n' "$NEEDED" | grep -qx 'Mathlib'; then
    echo "preflight: NOTE Statements/$STATEMENT.lean imports bare \`Mathlib\`, so every"
    echo "preflight:      contributor to it downloads the whole olean cache. Import the"
    echo "preflight:      modules you need instead; the file is write-once."
  fi
else
  MISSING="$(printf '%s\n' "$NEEDED" | missing_oleans)"
fi

if [ -z "$MISSING" ]; then
  echo "preflight: Mathlib oleans already present in $REPO"
else
  FETCHED=0
  if [ "$WANT_ALL" -eq 0 ]; then
    echo "preflight: fetching oleans for $(printf '%s\n' "$MISSING" | wc -l | tr -d ' ') Mathlib module(s)"
    FILES=$(printf '%s\n' "$MISSING" | sed 's|\.|/|g; s|$|.lean|')
    # `cache get FILE` resolves its paths against the mathlib package root, not
    # the workspace: from $REPO it reported "non-existing path Mathlib/..." for
    # ordinary module names and fell through to the full cache every time.
    # shellcheck disable=SC2086
    ( cd "$MATHLIB_PKG" && lake exe cache get $FILES ) && FETCHED=1
    # cache's argument form has changed before, so confirm the files landed
    # rather than trusting exit 0.
    [ -n "$(printf '%s\n' "$MISSING" | missing_oleans)" ] && FETCHED=0
    # A real Mathlib import transitively needs hundreds of oleans. If only the
    # named files landed, `cache get FILE` is not pulling dependencies here and
    # the build would compile Mathlib from source, which is hours.
    if [ "$FETCHED" -eq 1 ] \
       && [ "$(find "$MATHLIB_LIB" -name '*.olean' 2>/dev/null | head -60 | wc -l | tr -d ' ')" -lt 50 ]; then
      FETCHED=0
    fi
    [ "$FETCHED" -eq 0 ] && echo "preflight: targeted fetch did not cover it; falling back to the full cache"
  fi
  if [ "$FETCHED" -eq 0 ]; then
    echo "preflight: fetching the full Mathlib olean cache (download, never compile). Slow once."
    if ! ( cd "$REPO" && lake exe cache get ); then
      unavailable "could not fetch Mathlib" \
        "\`lake exe cache get\` failed in $REPO." \
        "Usually no network access, or not enough disk for the olean cache." \
        "A wall of 403 host_not_allowed is an egress allowlist, not a network" \
        "fault: the cache lives on lakecache.blob.core.windows.net. See" \
        "https://jig.so/guide/network.md for the hosts and who can open them."
    fi
  fi
fi

# ---------------------------------------------------------------------------
# 5. The real verifier: build, anti-restatement, axiom audit, term hash
# ---------------------------------------------------------------------------
OUT="$REPO/.conject/preflight-$STATEMENT-$NAME.json"
# Stale verdicts under near-identical names have already been read as this run's
# result. There is exactly one verdict for this invocation and it is written below.
rm -f "$OUT"
echo
echo "preflight: running scripts/verify.sh (build + anti-restatement + axiom audit)"
( cd "$REPO" && ./scripts/verify.sh \
    --statement "$STATEMENT" \
    --submission "Submissions/$STATEMENT/$NAME.json" \
    --out "$OUT" \
    --timeout "$TIMEOUT" ) >/dev/null 2>&1
STATUS=$?

if [ ! -f "$OUT" ]; then
  echo "FAIL  the verifier produced no verdict (exit $STATUS)"
  exit 1
fi

if command -v jq >/dev/null 2>&1; then
  jq -r '
    "verdict: \(.verdict)   reason: \(.reason)",
    "detail:  \(.detail // "")",
    "axioms:  \(.axioms // [] | join(", "))",
    "term:    \(.elaborated_term_hash // "-")",
    "",
    "checks:",
    (.checks // {} | to_entries[] | "  \(if .value.ok then "ok  " else "FAIL" end)  \(.key)  \(.value.detail // "")")
  ' "$OUT"
else
  cat "$OUT"
fi

echo
echo "preflight: full verdict at $OUT"
if [ "$STATUS" -eq 0 ]; then
  cat <<'NOTE'

Green locally. Still owed before you submit:
  * vacuity   exhibit a witness satisfying the hypotheses
  * dedupe    exact? / apply? against Mathlib, and the corpus for the same proof
  * controls  forced-answer checks in BOTH directions on any computational witness
  * commons   break attempts against every 'proposed' commons def you depend on
  * citations opened:true only for documents you actually read

elaborated_term_hash is optional. Both the API and the webhook normalise to
algo:hex, so the "term:" value above is safe to claim verbatim if you want the
record to show you predicted it. Omitting it is always fine: the settle fills it
in from what CI actually elaborated.
NOTE
fi
exit "$STATUS"