leanPackages: structural reimagining — own toolchain, lake --packages, Hydra visibility
Give leanPackages its own lean4, independent of pkgs.lean4. Binary- patch the toolchain so the language server discovers the wrapped lake despite lake serve deriving LAKE from IO.appPath unconditionally. Supplant Lake's config trace validation for /nix/store/ dependencies, deferring cache coherence to Nix. Migrate Nix-managed dependency injection from package-overrides.json to lake --packages. Patch Cli to pre-build static library for downstream executables. Add recurseIntoAttrs for Hydra. Upstream accepted FetchContent for mimalloc vendoring: https://github.com/leanprover/lean4/commit/a145b9c11a0fe38fd4c921024a7376c99cc34bd2
This commit is contained in:
Nadja Yang
@@ -1,20 +1,11 @@
|
||||
# buildLakePackage: build Lean 4 projects that use the Lake build system.
|
||||
#
|
||||
# Dependencies can be provided in two ways:
|
||||
# - `leanDeps`: already-packaged Lean libraries from leanPackages.
|
||||
# These are injected into LEAN_PATH via setup hooks and propagated
|
||||
# transitively, similar to Haskell's libraryHaskellDepends.
|
||||
# - `leanDeps`: nix-packaged Lean libraries, injected via
|
||||
# `lake --packages` and propagated transitively via LEAN_PATH.
|
||||
# - `lakeHash`: SRI hash for a fetchLakeDeps FOD that clones git
|
||||
# dependencies listed in lake-manifest.json (like buildGoModule's
|
||||
# vendorHash). Not needed when all deps are in `leanDeps`.
|
||||
#
|
||||
# Library output layout:
|
||||
# $out/ Package root (source + build artifacts)
|
||||
# $out/lakefile.{lean,toml} Lake package configuration
|
||||
# $out/lean-toolchain Lean version pin
|
||||
# $out/.lake/build/lib/lean/ Compiled .olean/.ilean files
|
||||
# $out/.lake/build/ir/ Compiled C/object files
|
||||
# $out/nix-support/setup-hook LEAN_PATH propagation hook
|
||||
{
|
||||
lib,
|
||||
stdenv,
|
||||
@@ -22,7 +13,7 @@
|
||||
gitMinimal,
|
||||
cacert,
|
||||
jq,
|
||||
lndir,
|
||||
writeText,
|
||||
stdenvNoCC,
|
||||
}:
|
||||
|
||||
@@ -55,32 +46,19 @@ lib.extendMkDerivation {
|
||||
nativeBuildInputs ? [ ],
|
||||
passthru ? { },
|
||||
|
||||
# SRI hash for the Lake dependencies FOD.
|
||||
# Set to null if the project has no external dependencies
|
||||
# (or all deps are provided via leanDeps).
|
||||
# SRI hash for the Lake dependencies FOD (null = all deps nix-managed).
|
||||
lakeHash ? null,
|
||||
|
||||
# Pre-built Lake dependencies derivation (overrides lakeHash).
|
||||
lakeDeps ? null,
|
||||
|
||||
# Already-packaged Lean libraries from nixpkgs.
|
||||
# These are added to LEAN_PATH (via setup hook) and propagated
|
||||
# transitively. Each must be a buildLakePackage output with
|
||||
# .olean files under $out/.lake/build/lib/lean/.
|
||||
# Nix-packaged Lean libraries, injected via lake --packages.
|
||||
leanDeps ? [ ],
|
||||
|
||||
# Lean package name as declared in lakefile.lean/toml.
|
||||
# Defaults to pname.
|
||||
# Lake package name as declared in lakefile (defaults to pname).
|
||||
leanPackageName ? finalAttrs.pname,
|
||||
|
||||
# Lake build targets. Empty list means the default target.
|
||||
# Lake build targets (empty = default targets).
|
||||
buildTargets ? [ ],
|
||||
|
||||
# Whether this is a library (install full package tree with
|
||||
# .olean/.ilean files) or an executable (install binaries only).
|
||||
# Library (install .olean tree) or executable (install binaries only).
|
||||
isLibrary ? true,
|
||||
|
||||
# Override attributes of the lakeDeps derivation.
|
||||
# Override the FOD derivation attrs.
|
||||
overrideLakeDepsAttrs ? (finalAttrs: previousAttrs: { }),
|
||||
|
||||
meta ? { },
|
||||
@@ -96,6 +74,10 @@ lib.extendMkDerivation {
|
||||
isLibrary = args.isLibrary or true;
|
||||
leanPackageName = args.leanPackageName or finalAttrs.pname;
|
||||
|
||||
allLeanDeps = lib.unique (
|
||||
builtins.concatMap (dep: [ dep ] ++ (dep.passthru.allLeanDeps or [ ])) leanDeps
|
||||
);
|
||||
|
||||
computedLakeDeps =
|
||||
if lakeDeps' != null then
|
||||
lakeDeps'
|
||||
@@ -114,11 +96,18 @@ lib.extendMkDerivation {
|
||||
}).overrideAttrs
|
||||
(lib.toExtension overrideLakeDepsAttrs);
|
||||
|
||||
# Transitively collect all Lean dependencies. Each buildLakePackage
|
||||
# library stores its own transitive closure in passthru.allLeanDeps,
|
||||
# so this flattens the entire dependency DAG.
|
||||
allLeanDeps = lib.unique (
|
||||
builtins.concatMap (dep: [ dep ] ++ (dep.passthru.allLeanDeps or [ ])) leanDeps
|
||||
# Nix-managed dep overrides, generated at eval time.
|
||||
# --packages takes precedence over .lake/package-overrides.json.
|
||||
overridesFile = writeText "lake-overrides.json" (
|
||||
builtins.toJSON {
|
||||
schemaVersion = "1.2.0";
|
||||
packages = map (dep: {
|
||||
type = "path";
|
||||
name = dep.passthru.lakePackageName or dep.pname;
|
||||
inherited = false;
|
||||
dir = "${dep}";
|
||||
}) allLeanDeps;
|
||||
}
|
||||
);
|
||||
in
|
||||
{
|
||||
@@ -128,14 +117,9 @@ lib.extendMkDerivation {
|
||||
lean4
|
||||
gitMinimal
|
||||
jq
|
||||
lndir
|
||||
];
|
||||
|
||||
# Propagate so downstream packages get transitive LEAN_PATH entries
|
||||
# via each dependency's nix-support/setup-hook.
|
||||
propagatedBuildInputs = lib.optionals isLibrary leanDeps;
|
||||
|
||||
# Executables only need deps at build time.
|
||||
buildInputs = lib.optionals (!isLibrary) leanDeps;
|
||||
|
||||
configurePhase =
|
||||
@@ -144,106 +128,34 @@ lib.extendMkDerivation {
|
||||
|
||||
export HOME="$TMPDIR"
|
||||
|
||||
# Disable Lake cloud caching and Reservoir lookups
|
||||
# Disable cloud caching and Reservoir lookups.
|
||||
export LAKE_NO_CACHE=1
|
||||
export RESERVOIR_API_URL=""
|
||||
|
||||
# Point leanc at the nix-provided C compiler
|
||||
export LEAN_CC="${stdenv.cc}/bin/cc"
|
||||
|
||||
# Validate that the lean-toolchain file (if present) matches the
|
||||
# Lean toolchain we are building against. Mismatches between the
|
||||
# toolchain version and the compiler produce confusing errors, so
|
||||
# fail early with a clear message.
|
||||
leanVersion="${lean4.version}"
|
||||
if [ -f lean-toolchain ]; then
|
||||
toolchainVersion=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' lean-toolchain)
|
||||
if [ -n "$toolchainVersion" ] && [ "$toolchainVersion" != "$leanVersion" ]; then
|
||||
echo "buildLakePackage: lean-toolchain requests v$toolchainVersion but lean4 is v$leanVersion" >&2
|
||||
echo "buildLakePackage: update the package or use a matching lean4 version" >&2
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
|
||||
${lib.concatStringsSep "\n" (
|
||||
builtins.map (
|
||||
dep:
|
||||
let
|
||||
name = dep.passthru.lakePackageName or dep.pname;
|
||||
in
|
||||
''
|
||||
# Fail fast if nix-packaged dep "${name}" was built against a
|
||||
# different Lean version. This avoids wasting build time when
|
||||
# the package set is mid-update (e.g. lean4 bumped but a dep
|
||||
# has not been updated yet).
|
||||
if [ -f "${dep}/lean-toolchain" ]; then
|
||||
depToolchain=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' "${dep}/lean-toolchain")
|
||||
if [ -n "$depToolchain" ] && [ "$depToolchain" != "$leanVersion" ]; then
|
||||
echo "buildLakePackage: dependency ${name} was built with Lean v$depToolchain but lean4 is v$leanVersion" >&2
|
||||
echo "buildLakePackage: update ${name} first, or override lean4 in leanPackages" >&2
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
''
|
||||
) allLeanDeps
|
||||
)}
|
||||
|
||||
if [ -n "''${LEAN_PATH:-}" ]; then
|
||||
echo "buildLakePackage: LEAN_PATH=$LEAN_PATH"
|
||||
fi
|
||||
|
||||
mkdir -p .lake/packages
|
||||
|
||||
# Create a minimal empty manifest if none exists. Lake requires
|
||||
# this file, but when all deps come from leanDeps (nix-managed),
|
||||
# the actual dependency entries come from package-overrides.json.
|
||||
if [ ! -f lake-manifest.json ]; then
|
||||
echo '{"version":"1.1.0","packagesDir":".lake/packages","packages":[]}' \
|
||||
> lake-manifest.json
|
||||
fi
|
||||
|
||||
${lib.optionalString (computedLakeDeps != null) ''
|
||||
# Copy fetched (not yet nix-packaged) deps into .lake/packages/
|
||||
mkdir -p .lake/packages
|
||||
for dep in ${computedLakeDeps}/*; do
|
||||
depName="$(basename "$dep")"
|
||||
cp -r "$dep" ".lake/packages/$depName"
|
||||
chmod -R u+w ".lake/packages/$depName"
|
||||
done
|
||||
''}
|
||||
|
||||
${lib.concatStringsSep "\n" (
|
||||
builtins.map (
|
||||
dep:
|
||||
let
|
||||
name = dep.passthru.lakePackageName or dep.pname;
|
||||
in
|
||||
''
|
||||
# Install nix-packaged dep "${name}" into .lake/packages/.
|
||||
# lndir creates a symlink tree so artifacts remain as
|
||||
# zero-copy references to the store; writable dirs let Lake
|
||||
# create metadata during workspace initialization.
|
||||
rm -rf ".lake/packages/${name}"
|
||||
mkdir -p ".lake/packages/${name}"
|
||||
lndir -silent "${dep}" ".lake/packages/${name}"
|
||||
''
|
||||
) allLeanDeps
|
||||
)}
|
||||
|
||||
# Generate package-overrides.json redirecting deps to local
|
||||
# paths. Scans .lake/packages/ so that nix-managed deps work
|
||||
# even without a lake-manifest.json (like Haskell's package DB
|
||||
# approach — nix is the sole dependency provider, Lake just
|
||||
# validates against lakefile.lean at build time).
|
||||
if [ -d .lake/packages ] && [ -n "$(ls -A .lake/packages/ 2>/dev/null)" ]; then
|
||||
# FOD deps use package-overrides.json (the on-disk mechanism).
|
||||
# Nix-managed deps use --packages (the CLI mechanism, takes precedence).
|
||||
jq -n --argjson pkgs "$(
|
||||
for dep in .lake/packages/*/; do
|
||||
[ -d "$dep" ] || continue
|
||||
depName="$(basename "$dep")"
|
||||
printf '{"type":"path","name":"%s","inherited":false,"configFile":"lakefile","dir":".lake/packages/%s"}\n' \
|
||||
"$depName" "$depName"
|
||||
jq -n --arg name "$depName" --arg dir ".lake/packages/$depName" \
|
||||
'{type: "path", name: $name, inherited: false, dir: $dir}'
|
||||
done | jq -s '.'
|
||||
)" '{schemaVersion: "1.1.0", packages: $pkgs}' > .lake/package-overrides.json
|
||||
fi
|
||||
)" '{schemaVersion: "1.2.0", packages: $pkgs}' > .lake/package-overrides.json
|
||||
''}
|
||||
|
||||
runHook postConfigure
|
||||
'';
|
||||
@@ -255,7 +167,7 @@ lib.extendMkDerivation {
|
||||
local targets="${lib.concatStringsSep " " buildTargets}"
|
||||
echo "buildLakePackage: building ''${targets:-default targets}"
|
||||
|
||||
lake build --no-ansi $targets
|
||||
lake build --no-ansi --packages=${overridesFile} $targets
|
||||
|
||||
runHook postBuild
|
||||
'';
|
||||
@@ -266,25 +178,22 @@ lib.extendMkDerivation {
|
||||
''
|
||||
runHook preInstall
|
||||
|
||||
# Install the complete Lake package tree. $out/ IS the
|
||||
# package directory — source, lakefile, and pre-built
|
||||
# artifacts under .lake/build/.
|
||||
# Install the complete Lake package tree.
|
||||
cp -rT . "$out"
|
||||
|
||||
# Remove build-environment artifacts that reference the
|
||||
# build sandbox or dependency store paths.
|
||||
# Remove build-time artifacts.
|
||||
rm -rf "$out/.lake/packages"
|
||||
rm -f "$out/.lake/package-overrides.json"
|
||||
|
||||
# Install the setup hook so that downstream derivations
|
||||
# (and `nix develop` shells) automatically get this
|
||||
# package's oleans in LEAN_PATH.
|
||||
# Reconcile config trace directory naming.
|
||||
if [ -d "$out/.lake/config/[anonymous]" ]; then
|
||||
mv "$out/.lake/config/[anonymous]" "$out/.lake/config/${leanPackageName}"
|
||||
fi
|
||||
|
||||
# Setup hook propagates LEAN_PATH to downstream packages.
|
||||
mkdir -p "$out/nix-support"
|
||||
cp ${./setup-hook.sh} "$out/nix-support/setup-hook"
|
||||
|
||||
# Symlink any built executables into $out/bin/ for
|
||||
# discoverability (e.g. packages that are both libraries
|
||||
# and executables).
|
||||
if [ -d "$out/.lake/build/bin" ]; then
|
||||
mkdir -p "$out/bin"
|
||||
for exe in "$out/.lake/build/bin"/*; do
|
||||
@@ -300,7 +209,6 @@ lib.extendMkDerivation {
|
||||
''
|
||||
runHook preInstall
|
||||
|
||||
# Install executables only.
|
||||
if [ -d .lake/build/bin ]; then
|
||||
mkdir -p "$out/bin"
|
||||
find .lake/build/bin -type f -executable \
|
||||
@@ -314,8 +222,6 @@ lib.extendMkDerivation {
|
||||
passthru = passthru // {
|
||||
inherit computedLakeDeps lean4 allLeanDeps;
|
||||
lakePackageName = leanPackageName;
|
||||
# Canonicalize overrideLakeDepsAttrs as an attribute overlay,
|
||||
# following the same pattern as buildGoModule's overrideModAttrs.
|
||||
overrideLakeDepsAttrs = lib.toExtension overrideLakeDepsAttrs;
|
||||
};
|
||||
|
||||
|
||||
@@ -1,4 +0,0 @@
|
||||
import WeakMinimax
|
||||
|
||||
def main : IO Unit := do
|
||||
IO.println "weak_minimax: verified (maximin <= minimax)"
|
||||
@@ -0,0 +1 @@
|
||||
{"version":"1.1.0","packagesDir":".lake/packages","packages":[]}
|
||||
@@ -6,7 +6,3 @@ package weakMinimax
|
||||
require "leanprover-community" / "mathlib" @ git "main"
|
||||
|
||||
@[default_target] lean_lib WeakMinimax
|
||||
|
||||
@[default_target]
|
||||
lean_exe weakMinimax.run where
|
||||
root := `Main
|
||||
|
||||
@@ -1,12 +1,5 @@
|
||||
# Test that buildLakePackage works with nix-only deps (no lake-manifest.json).
|
||||
# Builds a Lean proof of the weak minimax inequality using mathlib.
|
||||
#
|
||||
# Note: building the executable recompiles .c → .c.o for all transitive
|
||||
# dependency modules because library packages only ship .olean/.ilean/.c
|
||||
# artifacts (the default Lake library facet). Lake's trace system would
|
||||
# reuse pre-built object files if present, but since Lean 4 is rarely
|
||||
# used for application code, we defer shipping .o files in library
|
||||
# packages to keep store footprint minimal.
|
||||
{
|
||||
leanPackages,
|
||||
runCommand,
|
||||
@@ -24,17 +17,10 @@ let
|
||||
};
|
||||
in
|
||||
|
||||
runCommand "buildLakePackage-weak-minimax"
|
||||
{
|
||||
nativeBuildInputs = [ testPackage ];
|
||||
}
|
||||
''
|
||||
mkdir -p $out
|
||||
runCommand "buildLakePackage-weak-minimax" { } ''
|
||||
mkdir -p $out
|
||||
|
||||
# Verify the executable runs (proof was verified at build time).
|
||||
weakMinimax-run | tee $out/result
|
||||
grep -q "weak_minimax" $out/result
|
||||
|
||||
# Verify library output has compiled oleans.
|
||||
test -d "${testPackage}/.lake/build/lib/lean"
|
||||
''
|
||||
# Verify library output has compiled oleans.
|
||||
test -d "${testPackage}/.lake/build/lib/lean"
|
||||
touch $out/success
|
||||
''
|
||||
|
||||
@@ -6,17 +6,27 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-cli";
|
||||
version = "4.28.0";
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover";
|
||||
repo = "lean4-cli";
|
||||
tag = "v4.28.0";
|
||||
hash = "sha256-9nX+dozmDAaVb5uKWL14zbILr7aqbVerTyPcN12Niw4=";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-jCUl4sXVmwtYPuQecEUFH6mwFzPaQY7au4624EOiWjk=";
|
||||
};
|
||||
|
||||
leanPackageName = "Cli";
|
||||
|
||||
# Pre-build static library for downstream executables.
|
||||
# TODO: upstream this to lean4-cli
|
||||
postPatch = ''
|
||||
substituteInPlace lakefile.toml \
|
||||
--replace-fail '[[lean_lib]]
|
||||
name = "Cli"' '[[lean_lib]]
|
||||
name = "Cli"
|
||||
defaultFacets = ["static"]'
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Command-line argument parser for Lean 4";
|
||||
homepage = "https://github.com/leanprover/lean4-cli";
|
||||
|
||||
@@ -18,12 +18,6 @@ buildLakePackage {
|
||||
|
||||
leanPackageName = "LeanSearchClient";
|
||||
|
||||
# Upstream lean-toolchain lags behind; remove it so the
|
||||
# buildLakePackage toolchain check does not reject this package.
|
||||
postPatch = ''
|
||||
rm -f lean-toolchain
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Lean 4 client for LeanSearch and Moogle proof search";
|
||||
homepage = "https://github.com/leanprover-community/LeanSearchClient";
|
||||
|
||||
@@ -6,13 +6,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-Qq";
|
||||
version = "4.28.0";
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "quote4";
|
||||
tag = "v4.28.0";
|
||||
hash = "sha256-BRrSdDJQAsgM/NeSL2FODCez/8zEffjDRWUToGlKDNQ=";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-pNY5hv1nJbreCfU4EewIHCpiryIBv1ghWibrUW8vnQ0=";
|
||||
};
|
||||
|
||||
leanPackageName = "Qq";
|
||||
|
||||
@@ -7,13 +7,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-aesop";
|
||||
version = "4.28.0";
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "aesop";
|
||||
tag = "v4.28.0";
|
||||
hash = "sha256-KeP46qtEf4/lgi4iCVuYIQbazufTR4luTbsuia9JkK4=";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-CNwxNig8OWjtfQRYyRnM/HGBn2oaNX5qP9CVT2eWNlg=";
|
||||
};
|
||||
|
||||
leanPackageName = "aesop";
|
||||
|
||||
@@ -6,13 +6,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-batteries";
|
||||
version = "4.28.0";
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "batteries";
|
||||
tag = "v4.28.0";
|
||||
hash = "sha256-3N1MCFsg5UiwBCMAhDK7WwIowMNnhjlFgAsm0UPtGKc=";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-sEIDi2i2FaLTgKYWt/kzqPrjMdf+bFURfhw6ZZWBawQ=";
|
||||
};
|
||||
|
||||
leanPackageName = "batteries";
|
||||
|
||||
@@ -7,13 +7,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-importGraph";
|
||||
version = "4.28.0";
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "import-graph";
|
||||
tag = "v4.28.0";
|
||||
hash = "sha256-fZS8bFQjV7eLZCJwD+SVRzmCcCthrl+PO8vL8U8AOYs=";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-tqdO2qyWiJzEbK0yuu4+tiOXTEg9XJfGnI7z6Jh/abg=";
|
||||
};
|
||||
|
||||
leanPackageName = "importGraph";
|
||||
|
||||
@@ -0,0 +1,138 @@
|
||||
# Lean 4 toolchain for the leanPackages set (independent of pkgs.lean4).
|
||||
{
|
||||
lib,
|
||||
stdenv,
|
||||
symlinkJoin,
|
||||
cmake,
|
||||
fetchFromGitHub,
|
||||
git,
|
||||
gmp,
|
||||
cadical,
|
||||
pkg-config,
|
||||
libuv,
|
||||
perl,
|
||||
testers,
|
||||
}:
|
||||
|
||||
let
|
||||
lean4 = stdenv.mkDerivation (finalAttrs: {
|
||||
pname = "lean4";
|
||||
version = "4.29.0";
|
||||
|
||||
mimalloc-src = fetchFromGitHub {
|
||||
owner = "microsoft";
|
||||
repo = "mimalloc";
|
||||
tag = "v2.2.3";
|
||||
hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74=";
|
||||
};
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover";
|
||||
repo = "lean4";
|
||||
tag = "v${finalAttrs.version}";
|
||||
hash = "sha256-0v4OTrCLdHBbWJUq7hIjJonqget9SvsG3izGlOwhwyU=";
|
||||
};
|
||||
|
||||
# Vendor mimalloc. Upstream has since partially adopted FetchContent:
|
||||
# https://github.com/leanprover/lean4/commit/a145b9c11a0fe38fd4c921024a7376c99cc34bd2
|
||||
#
|
||||
# Dynamically adjust the source tree to maintain a healthy boundary
|
||||
# with Nix and avoid overstepping on its jurisdiction over cache coherence.
|
||||
postPatch =
|
||||
let
|
||||
pattern = "\${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc";
|
||||
in
|
||||
''
|
||||
substituteInPlace src/CMakeLists.txt \
|
||||
--replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")'
|
||||
|
||||
rm -rf src/lake/examples/git/
|
||||
|
||||
substituteInPlace CMakeLists.txt \
|
||||
--replace-fail 'GIT_REPOSITORY https://github.com/microsoft/mimalloc' \
|
||||
'SOURCE_DIR "${finalAttrs.mimalloc-src}"' \
|
||||
--replace-fail 'GIT_TAG ${finalAttrs.mimalloc-src.tag}' ""
|
||||
for file in stage0/src/CMakeLists.txt stage0/src/runtime/CMakeLists.txt src/CMakeLists.txt src/runtime/CMakeLists.txt; do
|
||||
substituteInPlace "$file" \
|
||||
--replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
|
||||
done
|
||||
|
||||
substituteInPlace src/lake/Lake/Load/Lean/Elab.lean \
|
||||
--replace-fail \
|
||||
'let upToDate := (← olean.pathExists) ∧' \
|
||||
'let upToDate := cfg.pkgDir.toString.startsWith "/nix/store/" ∨ (← olean.pathExists) ∧'
|
||||
'';
|
||||
|
||||
preConfigure = ''
|
||||
patchShebangs stage0/src/bin/ src/bin/
|
||||
'';
|
||||
|
||||
nativeBuildInputs = [
|
||||
cmake
|
||||
pkg-config
|
||||
];
|
||||
|
||||
buildInputs = [
|
||||
gmp
|
||||
libuv
|
||||
cadical
|
||||
];
|
||||
|
||||
nativeCheckInputs = [
|
||||
git
|
||||
perl
|
||||
];
|
||||
|
||||
cmakeFlags = [
|
||||
"-DUSE_GITHASH=OFF"
|
||||
"-DINSTALL_LICENSE=OFF"
|
||||
"-DUSE_MIMALLOC=ON"
|
||||
];
|
||||
|
||||
passthru.tests = {
|
||||
version = testers.testVersion {
|
||||
package = finalAttrs.finalPackage;
|
||||
version = "v${finalAttrs.version}";
|
||||
};
|
||||
};
|
||||
|
||||
meta = {
|
||||
description = "Automatic and interactive theorem prover";
|
||||
homepage = "https://leanprover.github.io/";
|
||||
changelog = "https://github.com/leanprover/lean4/blob/${finalAttrs.src.tag}/RELEASES.md";
|
||||
license = lib.licenses.asl20;
|
||||
platforms = lib.platforms.all;
|
||||
maintainers = with lib.maintainers; [ nadja-y ];
|
||||
mainProgram = "lean";
|
||||
};
|
||||
});
|
||||
|
||||
oldStorePath = builtins.substring 0 43 (toString lean4);
|
||||
in
|
||||
# Binary-patched for correct runtime discovery in wrapped environments.
|
||||
symlinkJoin {
|
||||
inherit (lean4) name pname;
|
||||
paths = [ lean4 ];
|
||||
nativeBuildInputs = [ perl ];
|
||||
postBuild = ''
|
||||
newStorePath=$(echo "$out" | head -c 43)
|
||||
|
||||
# Copy (not symlink) — IO.appPath resolves through symlinks.
|
||||
rm $out/bin/lean $out/bin/lake
|
||||
cp ${lean4}/bin/lean $out/bin/lean
|
||||
cp ${lean4}/bin/lake $out/bin/lake
|
||||
|
||||
for bin in $out/bin/lean $out/bin/lake; do
|
||||
cat "$bin" \
|
||||
| perl -pe "s|\Q${oldStorePath}\E|$newStorePath|g" \
|
||||
> "$bin.tmp"
|
||||
chmod +x "$bin.tmp"
|
||||
mv "$bin.tmp" "$bin"
|
||||
done
|
||||
'';
|
||||
|
||||
inherit (lean4) version src meta;
|
||||
passthru = {
|
||||
inherit (lean4) version src;
|
||||
};
|
||||
}
|
||||
@@ -14,13 +14,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-mathlib";
|
||||
version = "4.28.0";
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "mathlib4";
|
||||
tag = "v4.28.0";
|
||||
hash = "sha256-7kR0WvEDey5kEdqKKVEO/JgQd1VyB6a+zwPvIV5E5Pg=";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-fe+qS7gNxdLnACX3/jqToa9m7r1gbskY6kDJbm1ZefE=";
|
||||
};
|
||||
|
||||
leanPackageName = "mathlib";
|
||||
@@ -34,6 +34,8 @@ buildLakePackage {
|
||||
importGraph
|
||||
];
|
||||
|
||||
requiredSystemFeatures = [ "big-parallel" ];
|
||||
|
||||
passthru.tests = {
|
||||
inherit (tests.lake) weak-minimax;
|
||||
};
|
||||
|
||||
@@ -6,13 +6,13 @@
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-plausible";
|
||||
version = "4.28.0";
|
||||
version = "4.29.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "plausible";
|
||||
tag = "v4.28.0";
|
||||
hash = "sha256-xuOfeoRPt5L0Rk4fEJPIi1A0aoNIkC1fsh5yeIx5bFI=";
|
||||
tag = "v4.29.0";
|
||||
hash = "sha256-08fNB2GK5AqDJ15n5Ol+HYqaSbsznyp4cerDo32bG50=";
|
||||
};
|
||||
|
||||
leanPackageName = "plausible";
|
||||
|
||||
@@ -8,19 +8,18 @@
|
||||
}:
|
||||
|
||||
let
|
||||
version = "0.0.95";
|
||||
src = fetchFromGitHub {
|
||||
owner = "leanprover-community";
|
||||
repo = "ProofWidgets4";
|
||||
tag = "v0.0.87";
|
||||
hash = "sha256-qXEqNfwUBPnxAtLRkBZTBFhrM4JYl43gLo/PM6HOG7o=";
|
||||
tag = "v${version}";
|
||||
hash = "sha256-LETljr+QEU6CxprR3pB4hUzhgCD8PrIuiPOgTIdhHVM=";
|
||||
};
|
||||
in
|
||||
|
||||
buildLakePackage {
|
||||
pname = "lean4-proofwidgets";
|
||||
version = "0.0.87";
|
||||
|
||||
inherit src;
|
||||
inherit version src;
|
||||
|
||||
leanPackageName = "proofwidgets";
|
||||
|
||||
@@ -38,7 +37,7 @@ buildLakePackage {
|
||||
name = "lean4-proofwidgets-npm-deps";
|
||||
inherit src;
|
||||
sourceRoot = "source/widget";
|
||||
hash = "sha256-CzBRrreOSytquZ/xFHPlY8r+lz5Bg9Zk9ienRhc8SiY=";
|
||||
hash = "sha256-ShH6MDr76wzWQrJvhMWCnklaox/uRsfoe+aYVSo/eNA=";
|
||||
};
|
||||
npmRoot = "widget";
|
||||
|
||||
|
||||
@@ -1,33 +1,33 @@
|
||||
#!/usr/bin/env nix-shell
|
||||
#!nix-shell -i bash -p nix-update common-updater-scripts curl jq
|
||||
|
||||
# Update all leanPackages to match the lean4 version in nixpkgs.
|
||||
#
|
||||
# All mathlib-ecosystem packages (batteries, aesop, Qq, plausible,
|
||||
# importGraph, Cli, mathlib) release with the same version tag as
|
||||
# lean4 (lockstep versioning). ProofWidgets and LeanSearchClient
|
||||
# have their own versioning; the correct versions are read from
|
||||
# mathlib's lake-manifest.json at the matching lean4 tag.
|
||||
#
|
||||
# This script only prefetches source hashes — it does not build
|
||||
# anything. Output is a summary suitable for commit messages.
|
||||
# Update the leanPackages set.
|
||||
#
|
||||
# Usage:
|
||||
# ./pkgs/development/lean-modules/update.sh
|
||||
# ./pkgs/development/lean-modules/update.sh [version]
|
||||
|
||||
set -euo pipefail
|
||||
|
||||
lean4_version=$(nix eval --raw .#lean4.version)
|
||||
lean4_version="${1:-$(curl -sL https://api.github.com/repos/leanprover/lean4/releases/latest | jq -r '.tag_name' | sed 's/^v//')}"
|
||||
|
||||
# Snapshot current versions for diffing.
|
||||
# Snapshot before any updates.
|
||||
old_lockstep=$(nix eval --raw .#leanPackages.mathlib.version 2>/dev/null || echo "")
|
||||
old_pw=$(nix eval --raw .#leanPackages.proofwidgets.version 2>/dev/null || echo "")
|
||||
old_lsc=$(nix eval --raw .#leanPackages.LeanSearchClient.version 2>/dev/null || echo "")
|
||||
|
||||
run() { echo " $*"; "$@"; }
|
||||
|
||||
# --- lean4 toolchain ---
|
||||
|
||||
run nix-update leanPackages.lean4 --version="$lean4_version"
|
||||
|
||||
# --- mathlib dependency tree ---
|
||||
# Versions are derived from mathlib's lake-manifest.json at the
|
||||
# matching lean4 tag. Most packages release in lockstep with lean4;
|
||||
# ProofWidgets and LeanSearchClient have their own versioning.
|
||||
|
||||
manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json")
|
||||
|
||||
# Verify that mathlib's dependency set matches what we package.
|
||||
# If mathlib adds or removes a dep, this script needs manual updating.
|
||||
known_deps="Cli LeanSearchClient Qq aesop batteries importGraph plausible proofwidgets"
|
||||
manifest_deps=$(echo "$manifest" | jq -r '[.packages[].name] | sort | join(" ")')
|
||||
if [ "$manifest_deps" != "$known_deps" ]; then
|
||||
@@ -43,41 +43,41 @@ lsc_rev=$(echo "$manifest" | jq -r '.packages[] | select(.name == "LeanSearchCli
|
||||
lsc_date=$(curl -sL "https://api.github.com/repos/leanprover-community/LeanSearchClient/commits/$lsc_rev" | jq -r '.commit.committer.date[:10]')
|
||||
lsc_version="0-unstable-$lsc_date"
|
||||
|
||||
# Leaf packages (no leanDeps).
|
||||
nix-update leanPackages.batteries --version="$lean4_version"
|
||||
nix-update leanPackages.Qq --version="$lean4_version"
|
||||
nix-update leanPackages.plausible --version="$lean4_version"
|
||||
nix-update leanPackages.Cli --version="$lean4_version"
|
||||
nix-update leanPackages.proofwidgets --version="$pw_version"
|
||||
echo "--- mathlib tree ---"
|
||||
|
||||
# LeanSearchClient has no lockstep tags; pin to the exact rev mathlib uses.
|
||||
update-source-version leanPackages.LeanSearchClient "$lsc_version" \
|
||||
--rev="$lsc_rev"
|
||||
# Lockstep version synchronization.
|
||||
dir=pkgs/development/lean-modules
|
||||
for pkg in batteries aesop Qq plausible Cli importGraph mathlib; do
|
||||
sed -i "s|tag = \"v${old_lockstep}\"|tag = \"v${lean4_version}\"|" "$dir/$pkg/default.nix"
|
||||
done
|
||||
|
||||
# Packages with leanDeps.
|
||||
nix-update leanPackages.aesop --version="$lean4_version"
|
||||
nix-update leanPackages.importGraph --version="$lean4_version"
|
||||
run nix-update leanPackages.batteries --version="$lean4_version"
|
||||
run nix-update leanPackages.Qq --version="$lean4_version"
|
||||
run nix-update leanPackages.plausible --version="$lean4_version"
|
||||
run nix-update leanPackages.Cli --version="$lean4_version"
|
||||
run nix-update leanPackages.proofwidgets --version="$pw_version"
|
||||
run update-source-version leanPackages.LeanSearchClient "$lsc_version" --rev="$lsc_rev"
|
||||
run nix-update leanPackages.aesop --version="$lean4_version"
|
||||
run nix-update leanPackages.importGraph --version="$lean4_version"
|
||||
run nix-update leanPackages.mathlib --version="$lean4_version"
|
||||
|
||||
# mathlib (all deps are nix-packaged, no lakeHash needed).
|
||||
nix-update leanPackages.mathlib --version="$lean4_version"
|
||||
# --- summary ---
|
||||
|
||||
# Summary.
|
||||
changes=()
|
||||
if [ "$old_lockstep" != "$lean4_version" ]; then
|
||||
changes+=("lockstep packages: $old_lockstep -> $lean4_version")
|
||||
fi
|
||||
if [ "$old_pw" != "$pw_version" ]; then
|
||||
changes+=("proofwidgets: $old_pw -> $pw_version")
|
||||
fi
|
||||
if [ "$old_lsc" != "$lsc_version" ]; then
|
||||
changes+=("LeanSearchClient: $old_lsc -> $lsc_version")
|
||||
fi
|
||||
[ "$old_lockstep" != "$lean4_version" ] && changes+=("mathlib tree: $old_lockstep -> $lean4_version")
|
||||
[ "$old_pw" != "$pw_version" ] && changes+=("proofwidgets: $old_pw -> $pw_version")
|
||||
[ "$old_lsc" != "$lsc_version" ] && changes+=("LeanSearchClient: $old_lsc -> $lsc_version")
|
||||
|
||||
if [ ${#changes[@]} -eq 0 ]; then
|
||||
echo "leanPackages: already up to date at lean4 $lean4_version"
|
||||
else
|
||||
echo "leanPackages: update to lean4 $lean4_version"
|
||||
for c in "${changes[@]}"; do
|
||||
echo " - $c"
|
||||
done
|
||||
echo "status: up-to-date"
|
||||
exit 0
|
||||
fi
|
||||
|
||||
echo "commit-title: leanPackages: lean4 $old_lockstep -> $lean4_version"
|
||||
echo "---"
|
||||
for c in "${changes[@]}"; do
|
||||
echo " - $c"
|
||||
done
|
||||
echo "---"
|
||||
echo "manifest-source: https://github.com/leanprover-community/mathlib4/blob/v${lean4_version}/lake-manifest.json"
|
||||
echo "lean4-release: https://github.com/leanprover/lean4/releases/tag/v${lean4_version}"
|
||||
|
||||
@@ -2853,7 +2853,7 @@ with pkgs;
|
||||
|
||||
leanblueprint = with python3Packages; toPythonApplication leanblueprint;
|
||||
|
||||
leanPackages = callPackage ../top-level/lean-packages.nix { };
|
||||
leanPackages = recurseIntoAttrs (callPackage ../top-level/lean-packages.nix { });
|
||||
|
||||
inherit (callPackage ../development/tools/lerna { })
|
||||
lerna_6
|
||||
|
||||
@@ -1,45 +1,24 @@
|
||||
# Lean 4 package set.
|
||||
# Lean 4 package set with its own toolchain (independent of pkgs.lean4).
|
||||
#
|
||||
# All packages are built against a single Lean toolchain version.
|
||||
# Dependencies between packages use `leanDeps` which propagates
|
||||
# .olean files via LEAN_PATH (through setup hooks), similar to how
|
||||
# Haskell propagates package.conf.d entries.
|
||||
#
|
||||
# Overriding lean4 propagates to all packages in the set:
|
||||
# Override the toolchain for the entire set:
|
||||
# leanPackages.overrideScope (self: super: { lean4 = lean4-custom; })
|
||||
#
|
||||
# Usage:
|
||||
# leanPackages.batteries
|
||||
# leanPackages.mathlib
|
||||
# leanPackages.callPackage ./my-package.nix { }
|
||||
{
|
||||
lib,
|
||||
newScope,
|
||||
lean4,
|
||||
}:
|
||||
|
||||
lib.makeScope newScope (self: {
|
||||
inherit lean4;
|
||||
lean4 = self.callPackage ../development/lean-modules/lean4 { };
|
||||
|
||||
# Resolve via self.callPackage so overriding lean4 in the scope
|
||||
# propagates to the builder (same pattern as coqPackages).
|
||||
buildLakePackage = self.callPackage ../build-support/lake { };
|
||||
|
||||
batteries = self.callPackage ../development/lean-modules/batteries { };
|
||||
|
||||
aesop = self.callPackage ../development/lean-modules/aesop { };
|
||||
|
||||
Qq = self.callPackage ../development/lean-modules/Qq { };
|
||||
|
||||
proofwidgets = self.callPackage ../development/lean-modules/proofwidgets { };
|
||||
|
||||
plausible = self.callPackage ../development/lean-modules/plausible { };
|
||||
|
||||
LeanSearchClient = self.callPackage ../development/lean-modules/LeanSearchClient { };
|
||||
|
||||
Cli = self.callPackage ../development/lean-modules/Cli { };
|
||||
|
||||
importGraph = self.callPackage ../development/lean-modules/importGraph { };
|
||||
|
||||
mathlib = self.callPackage ../development/lean-modules/mathlib { };
|
||||
})
|
||||
|
||||
Reference in New Issue
Block a user