How to install Lean with mathlib

instructions.txt

This assumes that you have:
1. msys2
2. cmake
3. VSCode with Lean plugin
4. ninja

Run the following commands in order in msys2:

cd /c/
git clone https://github.com/leanprover/lean
cd lean
mkdir -p build/release
cd build/release
cmake -DCMAKE_BUILD_TYPE=RELEASE -G Ninja ../../src
ninja
cd /c/
git clone https://github.com/leanprover/mathlib
cd mathlib
/c/lean/bin/leanpkg build

remark: the core library is loaded by default. One only needs to set the workplace to the folder containing mathlib.

----

update:

cd /c/lean
git pull
cd build/release
ninja clean-olean
ninja
cd /c/mathlib
git pull
/c/lean/bin/leanpkg build