File size: 1,681 Bytes
dfe1826 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 | #!/usr/bin/env bash
# Build the Lean REPL (leanprover-community/repl) used by src/formal_mas/lean/runner.py.
# Works on Linux, macOS and Windows (Git Bash). Run from the repository root after
# scripts/setup_lean.sh. Takes ~1 min; the binary lands in lean_repl/.lake/build/bin/.
#
# The tag must match lean_project/lean-toolchain, and the commit is pinned (RNF-2):
# if the tag is ever moved upstream, the build stops instead of using other code.
set -euo pipefail
REPL_URL="https://github.com/leanprover-community/repl"
REPL_TAG="v4.36.0-rc1"
REPL_COMMIT="a85a1d2f4bdeab19c3d34be979ea336c9ee9b3ed"
ROOT="$(cd "$(dirname "$0")/.." && pwd)"
DEST="$ROOT/lean_repl"
export PATH="$HOME/.elan/bin:$PATH"
if [ ! -d "$DEST/.git" ]; then
echo ">> Cloning $REPL_URL at $REPL_TAG"
git clone --quiet --depth 1 --branch "$REPL_TAG" "$REPL_URL" "$DEST"
fi
commit="$(git -C "$DEST" rev-parse HEAD)"
if [ "$commit" != "$REPL_COMMIT" ]; then
echo "ERROR: lean_repl/ is at $commit, expected $REPL_COMMIT ($REPL_TAG)." >&2
echo "Delete lean_repl/ and run this script again." >&2
exit 1
fi
if [ -n "$(git -C "$DEST" status --porcelain --untracked-files=no)" ]; then
echo "ERROR: lean_repl/ has local changes; delete it and run this script again." >&2
exit 1
fi
project_toolchain="$(cat "$ROOT/lean_project/lean-toolchain")"
repl_toolchain="$(cat "$DEST/lean-toolchain")"
if [ "$project_toolchain" != "$repl_toolchain" ]; then
echo "ERROR: REPL toolchain $repl_toolchain != lean_project toolchain $project_toolchain" >&2
exit 1
fi
cd "$DEST"
echo ">> Building the REPL ($repl_toolchain)"
lake build repl
echo ">> REPL $REPL_TAG ($commit) built in lean_repl/.lake/build/bin/"
|