Formal-MAS source code

dfe1826 verified about 19 hours ago

1.53 kB

#!/usr/bin/env bash
# Install elan + Lean 4 and build lean_project/ with the pinned Mathlib (~7 GB).
# Works on Linux, macOS and Windows (Git Bash). Run from the repository root.
#
# If lean_project/ already exists (cloned repo), its lean-toolchain and
# lake-manifest.json pin the exact Lean version and Mathlib commit (RNF-2);
# otherwise a new project is created from the Mathlib `math` template.
set -euo pipefail

ROOT="$(cd "$(dirname "$0")/.." && pwd)"
export PATH="$HOME/.elan/bin:$PATH"

if ! command -v elan >/dev/null 2>&1; then
  echo ">> Installing elan (Lean version manager)"
  case "$(uname -s)" in
    MINGW*|MSYS*|CYGWIN*)
      tmp="$(mktemp -d)"
      curl -sSfL -o "$tmp/elan-init.ps1" \
        https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
      powershell -NoProfile -ExecutionPolicy Bypass -Command \
        "& '$(cygpath -w "$tmp/elan-init.ps1")' -NoPrompt \$true -DefaultToolchain none"
      ;;
    *)
      curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
        | sh -s -- -y --default-toolchain none
      ;;
  esac
fi

cd "$ROOT"
if [ ! -f lean_project/lakefile.toml ]; then
  echo ">> Creating lean_project/ from the Mathlib template"
  lake +leanprover-community/mathlib4:lean-toolchain new lean_project math
fi

cd lean_project
echo ">> Downloading precompiled Mathlib cache"
lake exe cache get
echo ">> Building"
lake build

echo ">> Versions"
lean --version
echo "Mathlib commit: $(git -C .lake/packages/mathlib rev-parse HEAD)"

	#!/usr/bin/env bash
	# Install elan + Lean 4 and build lean_project/ with the pinned Mathlib (~7 GB).
	# Works on Linux, macOS and Windows (Git Bash). Run from the repository root.
	#
	# If lean_project/ already exists (cloned repo), its lean-toolchain and
	# lake-manifest.json pin the exact Lean version and Mathlib commit (RNF-2);
	# otherwise a new project is created from the Mathlib `math` template.
	set -euo pipefail

	ROOT="$(cd "$(dirname "$0")/.." && pwd)"
	export PATH="$HOME/.elan/bin:$PATH"

	if ! command -v elan >/dev/null 2>&1; then
	echo ">> Installing elan (Lean version manager)"
	case "$(uname -s)" in
	MINGW\|MSYS\|CYGWIN*)
	tmp="$(mktemp -d)"
	curl -sSfL -o "$tmp/elan-init.ps1" \
	https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
	powershell -NoProfile -ExecutionPolicy Bypass -Command \
	"& '$(cygpath -w "$tmp/elan-init.ps1")' -NoPrompt \$true -DefaultToolchain none"
	;;
	*)
	curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
	\| sh -s -- -y --default-toolchain none
	;;
	esac
	fi

	cd "$ROOT"
	if [ ! -f lean_project/lakefile.toml ]; then
	echo ">> Creating lean_project/ from the Mathlib template"
	lake +leanprover-community/mathlib4:lean-toolchain new lean_project math
	fi

	cd lean_project
	echo ">> Downloading precompiled Mathlib cache"
	lake exe cache get
	echo ">> Building"
	lake build

	echo ">> Versions"
	lean --version
	echo "Mathlib commit: $(git -C .lake/packages/mathlib rev-parse HEAD)"