#!/bin/sh
# Save the downloaded Proof.lean and PureExpr.lean beside this script. Requires elan/Lean and Git.
set -eu
if [ ! -f Proof.lean ] || [ ! -f PureExpr.lean ]; then
  echo 'Place the downloaded Proof.lean and PureExpr.lean in the current directory first.' >&2
  exit 1
fi
proof_file=$(realpath Proof.lean)
proof_directory=$(dirname "$proof_file")
checkout_directory=$(mktemp -d)
trap 'rm -rf "$checkout_directory"' EXIT INT TERM
git clone https://github.com/hiloopai/silmaril-lean.git "$checkout_directory/silmaril"
cd "$checkout_directory/silmaril"
git checkout --detach 915988226ecd61a4862be0fadfdec89497592306
lake exe cache get
lake build Silmaril.Wasm.Binaryen.Exe.EncodeSound Silmaril.Wasm.Validation.Check.Validate Silmaril.Wasm.Execution.Core.Sim.Context Mathlib.Tactic.Ring
lake env lean -DwarningAsError=true -R "$proof_directory" -o "$proof_directory/PureExpr.olean" "$proof_directory/PureExpr.lean"
lean_path=$(lake env printenv LEAN_PATH)
lean_binary=$(lake env which lean)
LEAN_PATH="$proof_directory:$lean_path" "$lean_binary" -DwarningAsError=true -R "$proof_directory" -o "$proof_directory/Proof.olean" "$proof_file"
lean_path=$(lake env printenv LEAN_PATH)
checker_binary=$(lake env which leanchecker)
toolchain_bin=$(dirname "$checker_binary")
PATH="$toolchain_bin:$PATH" LEAN_PATH="$proof_directory:$lean_path" "$checker_binary" PureExpr Proof