setup

Setup Z Specification Tools

You are helping the user install and configure the tools needed for Z specification development.

Input

Arguments: $ARGUMENTS

Parse as:

• check - Check what's installed and report status
• fuzz - Install fuzz type-checker
• probcli - Install ProB command-line interface
• lean - Install Lean 4 theorem prover (elan + lean + lake)
• all - Install fuzz, probcli, and lean
• (no argument) - Same as check

Note: /z-spec:setup fuzz installs fuzz.sty and the oxsz Metafont sources into your TeX distribution's home tree (kpsewhich -var-value TEXMFHOME) once, for your user account — not per project. Neither /z-spec:check nor /z-spec:test copies TeX files anywhere; both simply read whatever kpsewhich already resolves. /z-spec:code2model is the one command that copies fuzz.sty and the Metafont sources into a project's docs/ directory; run /z-spec:cleanup to remove what it copied. /z-spec:create does not exist.

Process

1. Detect Platform

uname -s  # Darwin, Linux, etc.
uname -m  # arm64, x86_64, etc.

2. Check Current Status

Always start by checking what's already installed:

# Check fuzz. $FUZZ wins, then PATH — the order resolve_fuzz() uses. Note
# there is no conventional-path fallback for fuzz: a binary sitting outside
# PATH and unnamed by $FUZZ is a binary the engine will not find, however
# well it runs when you type its full path.
if [ -n "${FUZZ:-}" ] && [ -f "$FUZZ" ]; then
  FUZZ_BIN="$FUZZ"
else
  FUZZ_BIN="$(command -v fuzz 2>/dev/null)"
fi

if test -x "$FUZZ_BIN"; then
  echo "fuzz: $FUZZ_BIN"
  # fuzz has no -version flag: passing one lands on the 'e' in "version" and
  # prints the usage banner instead, with exit 2. -Dv is the debug flag that
  # prints the real version banner, and it needs input on stdin because fuzz
  # always reads a file — or, given none, stdin — before doing anything else.
  "$FUZZ_BIN" -Dv < /dev/null
elif test -e "$FUZZ_BIN"; then
  echo "fuzz: NOT EXECUTABLE at $FUZZ_BIN"
else
  echo "fuzz: NOT FOUND (not on PATH, and \$FUZZ does not name it)"
fi

# Check probcli, and report which version. Presence alone is not enough: a
# 1.16.x install answers every check in this section and still fails the
# coverage tier of every specification, so a bare "found" here would send the
# user off to discover that one command later with nothing pointing back.
# $PROBCLI wins, then PATH, then the conventional path — the order
# resolve_probcli() uses. Resolving any other way would make this report
# describe a binary the other commands are not going to run, which is the
# whole failure this section exists to prevent.
if [ -n "${PROBCLI:-}" ] && [ -f "$PROBCLI" ]; then
  PROBCLI_BIN="$PROBCLI"
else
  PROBCLI_BIN="$(command -v probcli 2>/dev/null || echo "$HOME/Applications/ProB/probcli")"
fi

if test -x "$PROBCLI_BIN"; then
  PROB_VER="$("$PROBCLI_BIN" -version 2>/dev/null | grep -oE '[0-9]+\.[0-9]+\.[0-9]+' | head -1)"
  echo "probcli: $PROBCLI_BIN (version ${PROB_VER:-unreadable})"
  test "$PROB_VER" = "1.15.1" || echo "  WARNING: z-spec needs 1.15.1 — see 'Choosing a version' below"
elif test -e "$PROBCLI_BIN"; then
  echo "probcli: NOT EXECUTABLE at $PROBCLI_BIN"
else
  echo "probcli: NOT FOUND"
fi

# Check fuzz.sty in the TeX path. kpsewhich prints nothing and exits nonzero
# when it finds nothing, which is silence where a status line belongs.
if FUZZ_STY="$(kpsewhich fuzz.sty 2>/dev/null)" && [ -n "$FUZZ_STY" ]; then
  echo "fuzz.sty: $FUZZ_STY"
else
  echo "fuzz.sty: NOT FOUND in the TeX path"
fi

# Check Tcl/Tk. probcli needs it on some systems and not others, so absence
# here is a note, not a verdict — the probcli line above is the real test.
if command -v wish >/dev/null 2>&1; then
  echo "tcl/tk: $(command -v wish)"
else
  echo "tcl/tk: no wish on PATH (only matters if probcli reports a missing library)"
fi

# Check the Lean toolchain (optional, for /z-spec:prove). Three states, the
# same three section 6 reports: on PATH, present under ~/.elan/bin but not on
# PATH, or absent. /z-spec:prove looks on PATH and nowhere else, so the middle
# state is a real distinction and not a formality.
for lean_tool in elan lean lake; do
  if command -v "$lean_tool" >/dev/null 2>&1; then
    echo "$lean_tool: $(command -v "$lean_tool")"
    "$lean_tool" --version
  elif [ -x ~/.elan/bin/"$lean_tool" ]; then
    echo "$lean_tool: at ~/.elan/bin but NOT on PATH — /z-spec:prove will not see it"
  else
    echo "$lean_tool: NOT FOUND (optional)"
  fi
done