chore: adapt install scripts from mathlib-tools (leanprover-community…

…#4965)

This takes the installation scripts from `mathlib-tools` and adapts them for `lean4`.

I will use these in the new installation instructions to replace 

* https://leanprover-community.github.io/install/macos.html
* https://leanprover-community.github.io/install/debian.html



Co-authored-by: Scott Morrison <[email protected]>

scripts/install_debian.sh

@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+set -exo pipefail
+
+sudo apt install -y git curl
+
+# Note that we're using `-y` here,
+# unlike the standard `curl [...] -sSf | sh` installation method.
+wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
+bash elan-init.sh -y
+rm elan-init.sh
+
+# The following test is needed in case VScode or VSCodium was installed by other
+# means (e.g. using Ubuntu snap)
+vsc="$(which code || which codium)"
+if [ -z "$vsc" ]; then
+  wget -O code.deb https://go.microsoft.com/fwlink/?LinkID=760868
+  sudo apt install -y ./code.deb
+  rm code.deb
+  vsc=code
+fi
+
+# Install the Lean4 VS Code extension
+"$vsc" --install-extension leanprover.lean4
+
+. ~/.profile

scripts/install_macos.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+set -exo pipefail
+
+# Install Homebrew
+if ! which brew > /dev/null; then
+    # Install Homebrew
+    /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install.sh)"
+else
+    # Update it, in case it has been ages since it's been updated
+    brew update
+fi
+
+brew install elan
+elan toolchain install stable
+elan default stable
+
+# Install and configure VS Code
+if ! which code > /dev/null; then
+    brew install --cask visual-studio-code
+fi
+
+# Install the Lean4 VS Code extension
+code --install-extension leanprover.lean4