diff --git a/flake.lock b/flake.lock index f3046deb986b..d5681f4051b1 100644 --- a/flake.lock +++ b/flake.lock @@ -2,48 +2,23 @@ "nodes": { "nixpkgs": { "locked": { - "lastModified": 1769018530, - "narHash": "sha256-S/5RU76BdQ32bbE99a+G9gMuatpVWEvIfeSjEqyoFS4=", - "rev": "88d3861acdd3d2f0e361767018218e51810df8a1", - "type": "tarball", - "url": "https://releases.nixos.org/nixos/unstable/nixos-26.05pre931542.88d3861acdd3/nixexprs.tar.xz" + "lastModified": 1770843696, + "narHash": "sha256-LovWTGDwXhkfCOmbgLVA10bvsi/P8eDDpRudgk68HA8=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2343bbb58f99267223bc2aac4fc9ea301a155a16", + "type": "github" }, "original": { - "type": "tarball", - "url": "https://channels.nixos.org/nixos-unstable/nixexprs.tar.xz" - } - }, - "nixpkgs-old": { - "flake": false, - "locked": { - "lastModified": 1582018169, - "narHash": "sha256-qv1iK1IchpZKSeWL3NEs4U5Jl5QVyNHDdiMJvLOI4Yc=", - "type": "tarball", - "url": "https://releases.nixos.org/nixos/19.03/nixos-19.03.173691.34c7eb7545d/nixexprs.tar.xz" - }, - "original": { - "type": "tarball", - "url": "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz" - } - }, - "nixpkgs-older": { - "flake": false, - "locked": { - "lastModified": 1550657948, - "narHash": "sha256-BE0XqzNfzvhhtTXv37LyySyq4moL7z1i1hMvwbFNL/I=", - "type": "tarball", - "url": "https://releases.nixos.org/nixos/18.03/nixos-18.03.133402.cb0e20d6db9/nixexprs.tar.xz" - }, - "original": { - "type": "tarball", - "url": "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz" + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" } }, "root": { "inputs": { - "nixpkgs": "nixpkgs", - "nixpkgs-old": "nixpkgs-old", - "nixpkgs-older": "nixpkgs-older" + "nixpkgs": "nixpkgs" } } }, diff --git a/flake.nix b/flake.nix index e3ecb6b2435b..011e3de96ace 100644 --- a/flake.nix +++ b/flake.nix @@ -1,71 +1,301 @@ { - description = "Lean development flake. Not intended for end users."; - - # We use channels so we're not affected by GitHub's rate limits - inputs.nixpkgs.url = "https://channels.nixos.org/nixos-unstable/nixexprs.tar.xz"; - # old nixpkgs used for portable release with older glibc (2.27) - inputs.nixpkgs-old.url = "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz"; - inputs.nixpkgs-old.flake = false; - # old nixpkgs used for portable release with older glibc (2.26) - inputs.nixpkgs-older.url = "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz"; - inputs.nixpkgs-older.flake = false; - - outputs = inputs: builtins.foldl' inputs.nixpkgs.lib.attrsets.recursiveUpdate {} (builtins.map (system: + description = "Lean 4 theorem prover and programming language"; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable"; + }; + + outputs = + { nixpkgs, ... }: let - pkgs = import inputs.nixpkgs { inherit system; }; - # An old nixpkgs for creating releases with an old glibc - pkgsDist-old = import inputs.nixpkgs-older { inherit system; }; - # An old nixpkgs for creating releases with an old glibc - pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; }; - - llvmPackages = pkgs.llvmPackages_19; - - devShellWithDist = pkgsDist: pkgs.mkShell.override { - stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang; - } ({ - buildInputs = with pkgs; [ - cmake gmp libuv ccache pkg-config - llvmPackages.bintools # wrapped lld - llvmPackages.llvm # llvm-symbolizer for asan/lsan - gdb - tree # for CI + systems = [ + "x86_64-linux" + "aarch64-linux" + ]; + + # Keep in sync with src/CMakeLists.txt LEAN_VERSION_* + version = "4.31.0-nix"; + + eachSystem = nixpkgs.lib.genAttrs systems; + + perSystem = eachSystem ( + system: + let + pkgs = nixpkgs.legacyPackages.${system}; + inherit (pkgs) lib stdenv; + + setupMimalloc = '' + mkdir -p mimalloc/src + cp -r ${pkgs.mimalloc.src} mimalloc/src/mimalloc + chmod -R u+w mimalloc + ''; + + commonCmakeFlags = [ + "-DCMAKE_BUILD_TYPE=Release" + "-DUSE_MIMALLOC=ON" + "-DLEAN_SPECIAL_VERSION_DESC=nix" + "-DLEAN_EXTRA_CXX_FLAGS=-Wno-array-bounds" ]; - # https://github.com/NixOS/nixpkgs/issues/60919 - hardeningDisable = [ "all" ]; - # more convenient `ctest` output - CTEST_OUTPUT_ON_FAILURE = 1; - } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux { - GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs: - pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") { - # would need additional linking setup on Linux aarch64, we don't use it anywhere else either - hardeningDisable = [ "stackprotector" ]; - }); - LIBUV = pkgsDist.libuv.overrideAttrs (attrs: { - configureFlags = ["--enable-static"]; - hardeningDisable = [ "stackprotector" ]; - # Sync version with CMakeLists.txt - version = "1.48.0"; - src = pkgs.fetchFromGitHub { - owner = "libuv"; - repo = "libuv"; - rev = "v1.48.0"; - sha256 = "100nj16fg8922qg4m2hdjh62zv4p32wyrllsvqr659hdhjc03bsk"; + + mkLeanDerivation = + attrs: + stdenv.mkDerivation ( + { + nativeBuildInputs = [ + pkgs.cmake + pkgs.git + pkgs.pkg-config + ]; + buildInputs = [ + pkgs.gmp + pkgs.libuv + ]; + preBuild = "patchShebangs ."; + preInstall = "rm -f src/lean"; + } + // attrs + ); + + srcFiles = lib.fileset.toSource { + root = ./.; + fileset = lib.fileset.unions [ + ./src + ./LICENSE + ./LICENSES + ]; + }; + + # Assert that the Nix-side version matches what CMake configured. + checkVersion = '' + cmake_version=$(sed -n 's/.*LEAN_VERSION_STRING "\(.*\)"/\1/p' include/lean/version.h) + if [ "$cmake_version" != "${version}" ]; then + echo "error: flake.nix version (${version}) != CMake version ($cmake_version)" + echo "Update the 'version' variable in flake.nix to match src/CMakeLists.txt" + exit 1 + fi + ''; + + # Same derivation as stage1 but with a different mainProgram for `nix run`. + mkToolAlias = + name: + stage1 + // { + meta = stage1.meta // { + mainProgram = name; + }; + }; + + stage0 = mkLeanDerivation { + pname = "lean-stage0"; + inherit version; + src = lib.fileset.toSource { + root = ./.; + fileset = ./stage0; + }; + sourceRoot = "source/stage0/src"; + preConfigure = setupMimalloc; + cmakeFlags = commonCmakeFlags ++ [ + "-DSTAGE=0" + "-DUSE_GITHASH=OFF" + ]; + meta.license = lib.licenses.asl20; + meta.platforms = lib.platforms.linux; + }; + + stage1 = mkLeanDerivation { + pname = "lean"; + inherit version; + src = srcFiles; + sourceRoot = "source/src"; + preConfigure = setupMimalloc; + postConfigure = checkVersion; + # Stage2 needs these from PREV_STAGE; default install rules exclude them. + postInstall = '' + mkdir -p $out/runtime $out/lib/temp + cp runtime/libleanrt_initial-exec.a $out/runtime/ + cp lib/temp/libleancpp_1.a $out/lib/temp/ + ''; + cmakeFlags = commonCmakeFlags ++ [ + "-DSTAGE=1" + "-DPREV_STAGE=${stage0}" + "-DUSE_GITHASH=OFF" + "-DINSTALL_LICENSE=ON" + "-DINSTALL_CADICAL=ON" + "-DUSE_LAKE=ON" + "-DLEAN_BUILD_TESTS=OFF" + ]; + meta = { + description = "Lean 4 theorem prover and programming language"; + homepage = "https://lean-lang.org"; + license = lib.licenses.asl20; + platforms = lib.platforms.linux; + mainProgram = "lean"; }; - doCheck = false; - }); - GLIBC = pkgsDist.glibc; - GLIBC_DEV = pkgsDist.glibc.dev; - GCC_LIB = pkgsDist.gcc.cc.lib; - ZLIB = pkgsDist.zlib; - # for CI coredumps - GDB = pkgsDist.gdb; - }); - in { - devShells.${system} = { - # The default development shell for working on lean itself - default = devShellWithDist pkgs; - oldGlibc = devShellWithDist pkgsDist-old; - oldGlibcAArch = devShellWithDist pkgsDist-old-aarch; - }; - }) ["x86_64-linux" "aarch64-linux" "aarch64-darwin"]); + }; + + stage2 = mkLeanDerivation { + pname = "lean-stage2"; + inherit version; + src = srcFiles; + sourceRoot = "source/src"; + preConfigure = setupMimalloc; + cmakeFlags = commonCmakeFlags ++ [ + "-DSTAGE=2" + "-DPREV_STAGE=${stage1}" + "-DUSE_GITHASH=OFF" + "-DINSTALL_LICENSE=ON" + "-DINSTALL_CADICAL=ON" + "-DUSE_LAKE=ON" + "-DLEAN_BUILD_TESTS=OFF" + ]; + meta = { + description = "Lean 4 stage2 self-hosted toolchain"; + license = lib.licenses.asl20; + platforms = lib.platforms.linux; + mainProgram = "lean"; + }; + }; + + # Shared between the dev shell and the configure/build apps so a + # standalone `nix run` finds gmp/libuv via CMAKE_PREFIX_PATH and the + # dev shell pulls in the same toolchain. Both the `dev` (headers) and + # default (lib) outputs are needed: cmake's find_path/find_library + # searches each prefix's include/ and lib/ directories. + cmakeBuildDeps = [ + pkgs.gmp + pkgs.gmp.dev + pkgs.libuv + pkgs.libuv.dev + ]; + + cmakeBuildTools = [ + pkgs.cmake + pkgs.pkg-config + pkgs.llvmPackages.bintools + pkgs.llvmPackages.clang + pkgs.llvmPackages.llvm + ]; + + cmakePrefixPath = lib.concatStringsSep ":" (map toString cmakeBuildDeps); + + # cmake's include_directories() silently drops paths that are + # already in CMAKE_PREFIX_PATH (treated as implicit). The Nix + # stdenv would normally set NIX_CFLAGS_COMPILE/NIX_LDFLAGS so the + # clang wrapper injects -isystem/-L; we replicate that here for + # standalone use outside a derivation. + nixCflagsCompile = lib.concatStringsSep " " ( + map (dep: "-isystem ${dep}/include") [ + pkgs.gmp.dev + pkgs.libuv.dev + ] + ); + nixLdflags = lib.concatStringsSep " " ( + map (dep: "-L${dep}/lib") [ + pkgs.gmp + pkgs.libuv + ] + ); + + # Env exports shared by configure and build scripts: prefix path + # for find_package, plus the wrapper-bound NIX_* flags. + commonShellEnv = '' + export CMAKE_PREFIX_PATH="${cmakePrefixPath}''${CMAKE_PREFIX_PATH:+:$CMAKE_PREFIX_PATH}" + export NIX_CFLAGS_COMPILE="${nixCflagsCompile}''${NIX_CFLAGS_COMPILE:+ $NIX_CFLAGS_COMPILE}" + export NIX_LDFLAGS="${nixLdflags}''${NIX_LDFLAGS:+ $NIX_LDFLAGS}" + export CC=clang + export CXX=clang++ + export CMAKE_C_COMPILER_LAUNCHER=ccache + export CMAKE_CXX_COMPILER_LAUNCHER=ccache + ''; + + # Mimalloc is staged at build/mimalloc/src/mimalloc so cmake's + # ${LEAN_BINARY_DIR}/../mimalloc reference (LEAN_BINARY_DIR is + # build/release here) resolves correctly. + configureScript = pkgs.writeShellApplication { + name = "lean-configure"; + runtimeInputs = cmakeBuildTools ++ cmakeBuildDeps ++ [ pkgs.ccache ]; + text = '' + ${commonShellEnv} + mkdir -p build/mimalloc/src + cp -r ${pkgs.mimalloc.src} build/mimalloc/src/mimalloc + chmod -R u+w build/mimalloc + rm -f build/release/CMakeCache.txt + cmake -S src -B build/release ${ + lib.concatMapStringsSep " " lib.escapeShellArg commonCmakeFlags + } -DSTAGE=1 -DPREV_STAGE=${stage0} -DUSE_GITHASH=OFF + ''; + }; + + buildScript = pkgs.writeShellApplication { + name = "lean-build"; + runtimeInputs = cmakeBuildTools ++ cmakeBuildDeps ++ [ pkgs.ccache ]; + text = '' + ${commonShellEnv} + cmake --build build/release -- -j"$(nproc)" + ''; + }; + + in + { + packages = { + inherit stage0 stage1 stage2; + default = stage1; + lean = mkToolAlias "lean"; + lake = mkToolAlias "lake"; + leanc = mkToolAlias "leanc"; + leanchecker = mkToolAlias "leanchecker"; + leanmake = mkToolAlias "leanmake"; + }; + + apps = { + configure = { + type = "app"; + program = lib.getExe configureScript; + }; + buildCMake = { + type = "app"; + program = lib.getExe buildScript; + }; + }; + + devShells.default = + (pkgs.mkShell.override { + stdenv = pkgs.overrideCC stdenv pkgs.llvmPackages.clang; + }) + { + buildInputs = + cmakeBuildTools + ++ cmakeBuildDeps + ++ [ + pkgs.ccache + pkgs.gdb + pkgs.tree + ]; + hardeningDisable = [ "all" ]; + MAKEFLAGS = "-j$(nproc)"; + CTEST_OUTPUT_ON_FAILURE = 1; + STAGE0 = stage0; + # Disable elan so Lake uses the local stage1 binaries directly. + # Without this, elan intercepts `lake`/`lean` and tries to resolve + # the `lean4-stage0` toolchain from src/lean-toolchain, which fails. + ELAN = ""; + # Use ccache by name so cmake doesn't cache absolute nix store paths + CMAKE_C_COMPILER_LAUNCHER = "ccache"; + CMAKE_CXX_COMPILER_LAUNCHER = "ccache"; + shellHook = '' + export PATH="$PWD/build/release/stage1/bin:$PATH" + if [ -f build/release/CMakeCache.txt ] && \ + ! grep -q "$STAGE0" build/release/CMakeCache.txt 2>/dev/null; then + echo "warning: CMakeCache.txt has stale STAGE0 path. Run: nix run .#configure" + fi + ''; + }; + } + ); + in + { + packages = nixpkgs.lib.mapAttrs (_: s: s.packages) perSystem; + devShells = nixpkgs.lib.mapAttrs (_: s: s.devShells) perSystem; + apps = nixpkgs.lib.mapAttrs (_: s: s.apps) perSystem; + }; } diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 372be2b36bc0..1cb98ba18624 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -386,12 +386,18 @@ endif() # ccache if(CCACHE AND NOT CMAKE_CXX_COMPILER_LAUNCHER AND NOT CMAKE_C_COMPILER_LAUNCHER) - find_program(CCACHE_PATH ccache) - if(CCACHE_PATH) - set(CMAKE_CXX_COMPILER_LAUNCHER "${CCACHE_PATH}") - set(CMAKE_C_COMPILER_LAUNCHER "${CCACHE_PATH}") + if(DEFINED ENV{CMAKE_CXX_COMPILER_LAUNCHER}) + # Prefer env vars (set by nix devShell) to avoid caching absolute store paths + set(CMAKE_CXX_COMPILER_LAUNCHER "$ENV{CMAKE_CXX_COMPILER_LAUNCHER}") + set(CMAKE_C_COMPILER_LAUNCHER "$ENV{CMAKE_C_COMPILER_LAUNCHER}") else() - message(WARNING "Failed to find ccache, prepare for longer and redundant builds...") + find_program(CCACHE_PATH ccache) + if(CCACHE_PATH) + set(CMAKE_CXX_COMPILER_LAUNCHER "${CCACHE_PATH}") + set(CMAKE_C_COMPILER_LAUNCHER "${CCACHE_PATH}") + else() + message(WARNING "Failed to find ccache, prepare for longer and redundant builds...") + endif() endif() endif() @@ -721,9 +727,11 @@ endif() add_subdirectory(initialize) add_subdirectory(shell) +option(LEAN_BUILD_TESTS "Configure the test suite. Disable for packaging builds that exclude tests/." ON) + # The relative path doesn't work once the CMakeLists.txt files have been copied into the stage0 dir. # Since stage0 needs no tests, we just ignore them instead of fixing the path. -if(NOT STAGE EQUAL 0) +if(NOT STAGE EQUAL 0 AND LEAN_BUILD_TESTS) add_subdirectory(../tests "${CMAKE_CURRENT_BINARY_DIR}/tests") endif()