chore: modernize build instructions

.github/workflows/ci.yml

@@ -94,7 +94,7 @@ jobs:
                 "name": "Linux Debug",
                 "os": "ubuntu-latest",
                 "quick": false,
-                "CMAKE_OPTIONS": "-DCMAKE_BUILD_TYPE=Debug",
+                "CMAKE_PRESET": "debug",
                 // exclude seriously slow tests
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
               },
@@ -104,7 +104,7 @@ jobs:
                 "os": "ubuntu-latest",
                 "quick": false,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
+                "CMAKE_PRESET": "sanitize",
                 // exclude seriously slow/problematic tests (laketests crash)
                 "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
               },*/
@@ -319,6 +319,9 @@ jobs:
           # store in current directory, for easy uploading together with binary
           echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
         if: runner.os == 'Linux'
+      - name: Set up NPROC
+        run: |
+          echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
       - name: Build
         run: |
           mkdir build
@@ -349,8 +352,8 @@ jobs:
             OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }})
           fi
           # contortion to support empty OPTIONS with old macOS bash
-          cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          make -j4
+          cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
+          make -j$NPROC
           make install
       - name: Check Binaries
         run: ${{ matrix.binary-check }} lean-*/bin/* || true
@@ -379,32 +382,29 @@ jobs:
           build/stage1/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
       - name: Test
+        id: test
         run: |
-          cd build/stage1
           ulimit -c unlimited # coredumps
-          # exclude nonreproducible test
-          ctest -j4 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+          ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
         if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
       - name: Test Summary
         uses: test-summary/action@v2
         with:
           paths: build/stage1/test-results.xml
         # prefix `if` above with `always` so it's run even if tests failed
-        if: always() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
+        if: always() && steps.test.conclusion != 'skipped'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
         if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
       - name: Build Stage 2
         run: |
-          cd build
           ulimit -c unlimited # coredumps
-          make -j4 stage2
+          make -C build -j$NPROC stage2
         if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
-          cd build
           ulimit -c unlimited # coredumps
-          make -j4 check-stage3
+          make -C build -j$NPROC stage3
         if: matrix.test-speedcenter
       - name: Test Speedcenter Benchmarks
         run: |
@@ -415,10 +415,9 @@ jobs:
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
-          cd build
           ulimit -c unlimited # coredumps
           # clean rebuild in case of Makefile changes
-          make update-stage0 && rm -rf ./stage* && make -j4
+          make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
         if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
       - name: CCache stats
         run: ccache -s

CMakePresets.json

@@ -0,0 +1,83 @@
+{
+  "version": 2,
+  "cmakeMinimumRequired": {
+    "major": 3,
+    "minor": 10,
+    "patch": 0
+  },
+  "configurePresets": [
+    {
+      "name": "release",
+      "displayName": "Default development optimized build config",
+      "generator": "Unix Makefiles",
+      "binaryDir": "${sourceDir}/build/release"
+    },
+    {
+      "name": "debug",
+      "displayName": "Debug build config",
+      "cacheVariables": {
+        "CMAKE_BUILD_TYPE": "Debug"
+      },
+      "generator": "Unix Makefiles",
+      "binaryDir": "${sourceDir}/build/debug"
+    },
+    {
+      "name": "sanitize",
+      "displayName": "Sanitize build config",
+      "cacheVariables": {
+        "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined",
+        "LEANC_EXTRA_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
+        "SMALL_ALLOCATOR": "OFF",
+        "BSYMBOLIC": "OFF"
+      },
+      "generator": "Unix Makefiles",
+      "binaryDir": "${sourceDir}/build/sanitize"
+    },
+    {
+      "name": "sandebug",
+      "inherits": ["debug", "sanitize"],
+      "displayName": "Sanitize+debug build config",
+      "binaryDir": "${sourceDir}/build/sandebug"
+    }
+  ],
+  "buildPresets": [
+    {
+      "name": "release",
+      "configurePreset": "release"
+    },
+    {
+      "name": "debug",
+      "configurePreset": "debug"
+    },
+    {
+      "name": "sanitize",
+      "configurePreset": "sanitize"
+    },
+    {
+      "name": "sandebug",
+      "configurePreset": "sandebug"
+    }
+  ],
+  "testPresets": [
+    {
+      "name": "release",
+      "configurePreset": "release",
+      "output": {"outputOnFailure": true, "shortProgress": true}
+    },
+    {
+      "name": "debug",
+      "configurePreset": "debug",
+      "inherits": "release"
+    },
+    {
+      "name": "sanitize",
+      "configurePreset": "sanitize",
+      "inherits": "release"
+    },
+    {
+      "name": "sandebug",
+      "configurePreset": "sandebug",
+      "inherits": "release"
+    }
+  ]
+}

doc/make/index.md

@@ -1,3 +1,7 @@
+These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](doc/dev/index.md).
+
+We strongly suggest that new users instead follow the [Quickstart](doc/quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
+
 Requirements
 ------------
 
@@ -17,39 +21,27 @@ Platform-Specific Setup
 Generic Build Instructions
 --------------------------
 
-Setting up a basic release build:
+Setting up a basic parallelized release build:
 
 ```bash
-git clone https://github.com/leanprover/lean4 --recurse-submodules
+git clone https://github.com/leanprover/lean4
 cd lean4
-mkdir -p build/release
-cd build/release
-cmake ../..
-make
-```
-
-For regular development, we recommend running
-```bash
-git config submodule.recurse true
+cmake --preset release
+make -C build/release -j$(nproc)  # see below for macOS
 ```
-in the checkout so that `--recurse-submodules` doesn't have to be
-specified with `git pull/checkout/...`.
+You can replace `$(nproc)`, which is not available on macOS and some alternative shells, with the desired parallelism amount.
 
 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.
-
-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.
+`stage1` subfolder; see below for details.
 
-You should not usually run `make install` after a successful build.
+You should not usually run `cmake --install` after a successful build.
 See [Dev setup using elan](../dev/index.md#dev-setup-using-elan) on how to properly set up your editor to use the correct stage depending on the source directory.
 
 Useful CMake Configuration Settings
 -----------------------------------
 
-Pass these along with the `cmake ../..` command.
+Pass these along with the `cmake --preset release` command.
+There are also two alternative presets that combine some of these options you can use instead of `release`: `debug` and `sandebug` (sanitize + debug).
 
 * `-D CMAKE_BUILD_TYPE=`\
   Select the build type. Valid values are `RELEASE` (default), `DEBUG`,

doc/make/msys2.md

@@ -38,10 +38,9 @@ cmake --version
 Then follow the [generic build instructions](index.md) in the MSYS2
 MinGW shell, using:
 ```
-cmake ../.. -G "Unix Makefiles"  -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
+cmake --preset release -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
 ```
-instead of `cmake ../..`. This ensures that cmake will call `sh` instead of `cmd.exe`
-for script tasks and it will use the clang compiler instead of gcc, which is required.
+instead of `cmake --preset release`. This will use the clang compiler instead of gcc, which is required with msys2.
 
 ## Install lean