chore: modernize build instructions (#4032)

Use `cmake --preset`, adjust and document parallelism settings
2026-03-17 18:34:06 +00:00 · 2024-05-23 12:55:07 +02:00
parent 258cc28dfc
commit 73a0c73c7c
5 changed files with 111 additions and 77 deletions
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -102,7 +102,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'"
              },
@@ -112,7 +112,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'"
              },*/
@@ -327,6 +327,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
@@ -357,8 +360,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
@@ -387,32 +390,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: |
@@ -423,10 +423,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
--- a/CMakePresets.json
+++ b/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"
+    }
+  ]
+}
--- a/doc/make/index.md
+++ b/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
+cmake --preset release
+make -C build/release -j$(nproc)  # see below for macOS
 ```
-
-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/...`.
+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.
+`stage1` subfolder; see below for details.

-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.
-
-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`,
--- a/doc/make/msvc.md
+++ b/doc/make/msvc.md
@@ -1,39 +0,0 @@
-# Compiling Lean with Visual Studio
-
-WARNING: Compiling Lean with Visual Studio doesn't currently work.
-There's an ongoing effort to port Lean to Visual Studio.
-The instructions below are for VS 2017.
-
-In the meantime you can use [MSYS2](msys2.md) or [WSL](wsl.md).
-
-## Installing dependencies
-
-First, install `vcpkg` from https://github.com/Microsoft/vcpkg if you haven't
-done so already.
-Then, open a console in the directory you cloned `vcpkg` to, and type:
-`vcpkg install mpir` for the 32-bit library or
-`vcpkg install mpir:x64-windows` for the x64 one.
-
-In Visual Studio, use the "open folder" feature and open the Lean directory.
-Go to the `CMake->Change CMake Settings` menu. File `CMakeSettings.json` opens.
-In each of the targets, add the following snippet (i.e., after every
-`ctestCommandArgs`):
-
-```json
-    "variables": [
-      {
-        "name": "CMAKE_TOOLCHAIN_FILE",
-        "value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake"
-      }
-    ]
-```
-
-## Enable Intellisense
-
-In Visual Studio, press Ctrl+Q and type `CppProperties.json` and press Enter.
-Ensure `includePath` variables include `"${workspaceRoot}\\src"`.
-
-
-## Build Lean
-
-Press F7.
--- a/doc/make/msys2.md
+++ b/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