From 5679a17603b2b6a8b80da73e9bec70eb0bab2a15 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Mar 2019 14:57:57 -0700
Subject: [PATCH] doc(doc/make/index): add instructions for invoking makefile
 manually

---
 doc/make/index.md | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/doc/make/index.md b/doc/make/index.md
index fa8ac7da21..4644cab212 100644
--- a/doc/make/index.md
+++ b/doc/make/index.md
@@ -49,9 +49,9 @@ Pass these along with the `cmake ../../src` command.
   [Some people report][ninja_work] that using
   Ninja can reduce the build time, esp when a build is
   incremental. Call `ninja` instead of `make` to build the project.
-  
+
   [ninja_work]: https://plus.google.com/108996039294665965197/posts/SfhrFAhRyyd
-  
+
 * `-D CMAKE_BUILD_TYPE=`
   Select the build type. Valid values are `RELEASE` (default), `DEBUG`,
   `RELWITHDEBINFO`, and `MINSIZEREL`.
@@ -109,6 +109,22 @@ Development Workflows
   `update-stage0` to copy stage1 to stage0 - this is the re-bootstrapping step.
   Reactivate `REBUILD_STAGE0` and stage0 should compile again.
 
+Troubleshooting
+---------------
+
+* The `Makefile` at `library/` does not need to be invoked directly. However,
+  we may want to do it while investigating problems, e.g., Lean is looping while
+  compiling a file. To manually invoke this `Makefile`, we should use:
+```bash
+cd library/
+STAGE1_OUT=<build_dir_path>/stage1 make <build_dir_path>/stage1/libleanstdlib.a
+```
+For example, if our build directory is located at `build/release/`, the command above should be
+```bash
+cd library/
+STAGE1_OUT=../build/release/stage1 make ../build/release/stage1/libleanstdlib.a
+```
+
 Further Information
 -------------------