From 1591bb164051850f18020f130933b159a2ca4ae8 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 8 Sep 2021 16:56:18 -0700
Subject: [PATCH] doc: fix msys text based on code review feedback

---
 doc/make/index.md        | 14 +++++++++++++-
 doc/make/msys2.md        | 35 ++++++++++++++++++++++-------------
 doc/make/ubuntu-16.04.md |  4 +++-
 3 files changed, 38 insertions(+), 15 deletions(-)

diff --git a/doc/make/index.md b/doc/make/index.md
index 2ab06028b1..21679c96d2 100644
--- a/doc/make/index.md
+++ b/doc/make/index.md
@@ -30,6 +30,14 @@ cmake ../..
 make
 ```
 
+Note: that if you have a CPU with lots of cores you will get a faster
+build if you specify the number of parallel jobs using the `-j n`
+option on make.
+
+For example, on an AMD Ryzen 9 `make` takes 00:04:55, whereas `make -j 10`
+takes 00:01:38.  Your results may vary depending on the speed of your hard
+drive.
+
 Setting up a basic debug build:
 
 ```bash
@@ -45,6 +53,10 @@ This will compile the Lean library and binary into the `stage1` subfolder; see
 below for details. Add `-jN` for an appropriate `N` to `make` for a parallel
 build.
 
+To install the build see [Dev setup using
+elan](index.md#dev-setup-using-elan) below.
+
+
 Useful CMake Configuration Settings
 -----------------------------------
 
@@ -179,7 +191,7 @@ affect later stages. This is an issue in two specific cases.
 
   For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
   (from before the flag defaulted to `false`).
-  
+
 To modify either of these flags both for building and editing the stdlib, adjust
 the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
 on the next `update-stage0` when the file is overwritten with the original
diff --git a/doc/make/msys2.md b/doc/make/msys2.md
index 141a94b05a..5a1f86ec95 100644
--- a/doc/make/msys2.md
+++ b/doc/make/msys2.md
@@ -13,19 +13,14 @@ It is easy to install all dependencies, it produces native
 
 [The official webpage of MSYS2][msys2] provides one-click installers.
 Once installed, you should run the "MSYS2 MinGW 64-bit shell" from the start menu.
+(The one that runs `mingw64.exe`)
 Do not run "MSYS2 MSYS" instead!
 MSYS2 has a package management system, [pacman][pacman], which is used in Arch Linux.
 
 Here are the commands to install all dependencies needed to compile Lean on your machine.
 
 ```bash
-pacman -S make mingw-w64-x86_64-cmake mingw-w64-x86_64-ccache mingw-w64-x86_64-gcc git
-```
-
-Then make sure the following is included in your PATH:
-
-```bash
-export PATH=$PATH:/mingw64/bin
+pacman -S make mingw-w64-x86_64-cmake mingw-w64-x86_64-ccache mingw-w64-x86_64-gcc git unzip
 ```
 
 You should now be able to run these commands:
@@ -35,15 +30,21 @@ gcc --version
 cmake --version
 ```
 
-Then follow the [generic build instructions](index.md) in the MSYS2 MinGW shell, using
-`cmake ../.. -G "Unix Makefiles"` instead of `cmake ../..`. This ensures that cmake will call `sh` instead
-of `cmd.exe` for script tasks.
+Then follow the [generic build instructions](index.md) in the MSYS2
+MinGW shell, using `cmake ../.. -G "Unix Makefiles"` instead of `cmake
+../..`. This ensures that cmake will call `sh` instead of `cmd.exe`
+for script tasks.
 
 ## Install lean
 
-You can use the `install` ninja/make target to install Lean into, by default,
-`./build/release/stage1/msys64/lean/`. To change this, add `-DCMAKE_INSTALL_PREFIX=path/you/want`
-to your initial cmake invocation.
+Follow the steps in [Dev setup using
+elan](index.md#dev-setup-using-elan) regarding installation of the
+bits you just built.  Note that in an msys2 environment `elan-init.sh`
+reports you need to add `%USERPROFILE%\.elan\bin` to your path, but of
+course in msys2 that needs to be a valid linux style path, like this:
+```bash
+export PATH="$PATH:/c/users/$USERNAME/.elan/bin"
+```
 
 ## Running
 
@@ -63,3 +64,11 @@ The following linux command will do that:
 ```bash
 cp $(ldd lean.exe | cut -f3 -d' ' | grep mingw) .
 ```
+
+## Trouble shooting
+
+**-bash: gcc: command not found**
+
+Make sure `/mingw64/bin` is in your PATH environment.  If it is not then
+check you launched the MSYS2 MinGW 64-bit shell from the start menu.
+(The one that runs `mingw64.exe`).
diff --git a/doc/make/ubuntu-16.04.md b/doc/make/ubuntu-16.04.md
index b166e32447..6b7c7df681 100644
--- a/doc/make/ubuntu-16.04.md
+++ b/doc/make/ubuntu-16.04.md
@@ -3,4 +3,6 @@ Installing Lean on Ubuntu 16.04
 
 ### Basic packages
 
-    sudo apt-get install git libgmp-dev cmake ccache
+```bash
+sudo apt-get install git libgmp-dev cmake ccache
+```