Spaces:
Running
Running
Rename setup.sh to install_repo.sh
Browse files- setup.sh → install_repo.sh +0 -19
setup.sh → install_repo.sh
RENAMED
|
@@ -1,23 +1,4 @@
|
|
| 1 |
#!/usr/bin/env bash
|
| 2 |
-
set -euxo pipefail
|
| 3 |
-
|
| 4 |
-
LEAN_SERVER_LEAN_VERSION="${LEAN_SERVER_LEAN_VERSION:-v4.15.0}"
|
| 5 |
-
REPL_REPO_URL="${REPL_REPO_URL:-https://github.com/leanprover-community/repl.git}"
|
| 6 |
-
REPL_BRANCH="${REPL_BRANCH:-$LEAN_SERVER_LEAN_VERSION}"
|
| 7 |
-
MATHLIB_REPO_URL="${MATHLIB_REPO_URL:-https://github.com/leanprover-community/mathlib4.git}"
|
| 8 |
-
MATHLIB_BRANCH="${MATHLIB_BRANCH:-$LEAN_SERVER_LEAN_VERSION}"
|
| 9 |
-
|
| 10 |
-
command -v curl >/dev/null 2>&1 || { echo >&2 "curl is required"; exit 1; }
|
| 11 |
-
command -v git >/dev/null 2>&1 || { echo >&2 "git is required"; exit 1; }
|
| 12 |
-
|
| 13 |
-
echo "Installing Elan"
|
| 14 |
-
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
|
| 15 |
-
| sh -s -- --default-toolchain "${LEAN_SERVER_LEAN_VERSION}" -y
|
| 16 |
-
source "$HOME/.elan/env"
|
| 17 |
-
|
| 18 |
-
echo "Installing Lean ${LEAN_SERVER_LEAN_VERSION}"
|
| 19 |
-
lean --version
|
| 20 |
-
|
| 21 |
install_repo() {
|
| 22 |
local name="$1" url="$2" branch="$3" upd_manifest="$4"
|
| 23 |
echo "Installing ${name}@${branch}..."
|
|
|
|
| 1 |
#!/usr/bin/env bash
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2 |
install_repo() {
|
| 3 |
local name="$1" url="$2" branch="$3" upd_manifest="$4"
|
| 4 |
echo "Installing ${name}@${branch}..."
|