chore: submodule hints

doc/make/index.md

@@ -23,7 +23,7 @@ Generic Build Instructions
 Setting up a basic release build:
 
 ```bash
-git clone https://github.com/leanprover/lean4
+git clone https://github.com/leanprover/lean4 --recurse-submodules
 cd lean4
 mkdir -p build/release
 cd build/release
@@ -31,6 +31,13 @@ cmake ../..
 make
 ```
 
+For regular development, we recommend running
+```bash
+git config submodule.recurse true
+```
+in the checkout so that `--recurse-submodules` doesn't have to be
+specified with `git pull/checkout/...`.
+
 The above commands will compile the Lean library and binaries into the
 `stage1` subfolder; see below for details. Add `-j N` for an
 appropriate `N` to `make` for a parallel build.

nix/bootstrap.nix

@@ -17,6 +17,10 @@ rec {
   } // args // {
     src = args.realSrc or (lib.sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
     cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
+    preConfigure = args.preConfigure or "" + ''
+      # ignore absence of submodule
+      sed -i 's!lake/Lake.lean!!' CMakeLists.txt
+    '';
   });
   lean-bin-tools-unwrapped = buildCMake {
     name = "lean-bin-tools";

src/CMakeLists.txt

@@ -474,6 +474,10 @@ if(${STAGE} GREATER 0)
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanpkg
     VERBATIM)
 
+  if(NOT EXISTS ${LEAN_SOURCE_DIR}/lake/Lake.lean)
+    message(FATAL_ERROR "src/lake does not exist. Please check out the Lake submodule using `git submodule update --init src/lake`.")
+  endif()
+
   add_custom_target(lake ALL
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS leanshared