From bc3900cbb9adda83eed7e6affeaade7cfd07716d Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Tue, 7 Sep 2021 14:43:20 -0700
Subject: [PATCH] doc: small fixes

---
 doc/make/msys2.md | 36 ++++++++++++++++++++++++++++++++++--
 doc/quickstart.md | 22 ++++++++++++++--------
 2 files changed, 48 insertions(+), 10 deletions(-)

diff --git a/doc/make/msys2.md b/doc/make/msys2.md
index b1727b05eb..141a94b05a 100644
--- a/doc/make/msys2.md
+++ b/doc/make/msys2.md
@@ -22,6 +22,19 @@ Here are the commands to install all dependencies needed to compile Lean on your
 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
+```
+
+You should now be able to run these commands:
+
+```bash
+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.
@@ -29,5 +42,24 @@ of `cmd.exe` for script tasks.
 ## Install lean
 
 You can use the `install` ninja/make target to install Lean into, by default,
-`C:\\User Programs (x86)\\LEAN`. To change this, add `-DCMAKE_INSTALL_PREFIX=path/you/want`
-to your cmake invocation.
+`./build/release/stage1/msys64/lean/`. To change this, add `-DCMAKE_INSTALL_PREFIX=path/you/want`
+to your initial cmake invocation.
+
+## Running
+
+You can run `lean --version` to see if your binaries work.
+
+If you want a version that can run independently of your MSYS install
+then you need to copy the following dependent DLL's from where ever
+they are installed in your MSYS setup:
+
+- libgcc_s_seh-1.dll
+- libstdc++-6.dll
+- libgmp-10.dll
+- libwinpthread-1.dll
+
+The following linux command will do that:
+
+```bash
+cp $(ldd lean.exe | cut -f3 -d' ' | grep mingw) .
+```
diff --git a/doc/quickstart.md b/doc/quickstart.md
index f3cbf70a4f..4b19bcaeea 100644
--- a/doc/quickstart.md
+++ b/doc/quickstart.md
@@ -7,19 +7,25 @@ See [Setup](./setup.md) for other ways and more details on setting up Lean.
     ```sh
     $ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly
     ```
-    Alternatively, on Windows, download [the latest release](https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip) and run the contained `elan-init.exe`.  
-    See the `elan` link above for other installation options and details.
+    Alternatively, on Windows, download [the latest release](https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-pc-windows-msvc.zip) and run the contained `elan-init.exe`.
+    See the [elan repo](https://github.com/leanprover/elan) for other installation options and details.
+
 1. Install [VS Code](https://code.visualstudio.com/).
-1. Open VS Code and install the `lean4` extension.  
-![installing the vscode-lean4 extension](images/code-ext.png)
+
+1. Open VS Code and install the `lean4` extension.
+
+    ![installing the vscode-lean4 extension](images/code-ext.png)
+
 1. Create a new file with the extension `.lean` and add the following code:
     ```lean
     import Leanpkg
-    
+
     #eval Leanpkg.leanVersionString
     ```
-    You should get a syntax-highlighted file with a "Lean Infoview" on the right that tells you the installed Lean version when placing your cursor on the last line.  
+    You should get a syntax-highlighted file with a "Lean Infoview" on the right that tells you the installed Lean version when placing your cursor on the last line.
+
     ![successful setup](images/code-success.png)
-1. You are set up! Try opening a Lean package with a `leanpkg.toml`. You can create your own packages using `leanpkg init` on the command line.
+
+1. You are set up! Try opening a Lean folder containing a package file `leanpkg.toml`. You can create your own packages using `leanpkg init` on the command line.
    Packages **have** to be opened using "File > Open Folder..." for imports to work.
-   Saved changes are visibly in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`) in them.
+   Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`).