diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index da16bd8d17..1a241e0964 100644 --- 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 diff --git a/CMakePresets.json b/CMakePresets.json new file mode 100644 index 0000000000..a7523ac7f2 --- /dev/null +++ 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" + } + ] +} diff --git a/doc/make/index.md b/doc/make/index.md index aae6bac06e..537ae7b8b8 100644 --- 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`, diff --git a/doc/make/msvc.md b/doc/make/msvc.md deleted file mode 100644 index 0fcc87c8d6..0000000000 --- a/doc/make/msvc.md +++ /dev/null @@ -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. diff --git a/doc/make/msys2.md b/doc/make/msys2.md index aacbb18c4e..fa3d28dfde 100644 --- 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