gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

buildLakePackage, leanPackages: init (#497946)

Browse Source
This commit is contained in:
Ryan Lahfa
2026-03-24 11:37:56 +00:00
committed by GitHub
parent 104f0c8889 9f1cb0f57c
commit 0aa1bfb82a
23 changed files with 951 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
maintainers/maintainer-list.nix
+6
View File
@@ -18701,6 +18701,12 @@
githubId = 23151917;
name = "nadir-ishiguro";
};
nadja-y = {
email = "git@njy.dev";
github = "nadja-y";
githubId = 255079535;
name = "Nadja Yang";
};
nadrieril = {
email = "nadrieril@gmail.com";
github = "Nadrieril";
pkgs/build-support/lake/default.nix
+326
View File
@@ -0,0 +1,326 @@
# 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.
# - `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,
lean4,
gitMinimal,
cacert,
jq,
lndir,
stdenvNoCC,
}:
let
fetchLakeDeps = import ./fetch-lake-deps.nix {
inherit
lib
stdenvNoCC
gitMinimal
cacert
jq
;
};
in
lib.extendMkDerivation {
constructDrv = stdenv.mkDerivation;
excludeDrvArgNames = [
"lakeHash"
"lakeDeps"
"leanDeps"
"buildTargets"
"isLibrary"
"leanPackageName"
"overrideLakeDepsAttrs"
];
extendDrvArgs =
finalAttrs:
{
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).
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/.
leanDeps ? [ ],
# Lean package name as declared in lakefile.lean/toml.
# Defaults to pname.
leanPackageName ? finalAttrs.pname,
# Lake build targets. Empty list means the default target.
buildTargets ? [ ],
# Whether this is a library (install full package tree with
# .olean/.ilean files) or an executable (install binaries only).
isLibrary ? true,
# Override attributes of the lakeDeps derivation.
overrideLakeDepsAttrs ? (finalAttrs: previousAttrs: { }),
meta ? { },
...
}@args:
let
lakeDeps' = args.lakeDeps or null;
lakeHash = args.lakeHash or null;
leanDeps = args.leanDeps or [ ];
overrideLakeDepsAttrs = args.overrideLakeDepsAttrs or (_: _: { });
buildTargets = args.buildTargets or [ ];
isLibrary = args.isLibrary or true;
leanPackageName = args.leanPackageName or finalAttrs.pname;
computedLakeDeps =
if lakeDeps' != null then
lakeDeps'
else if lakeHash == null then
null
else
(fetchLakeDeps {
name = finalAttrs.name or "${finalAttrs.pname}-${finalAttrs.version}";
inherit (finalAttrs) src;
hash = lakeHash;
sourceRoot = finalAttrs.sourceRoot or "";
patches = finalAttrs.patches or [ ];
prePatch = finalAttrs.prePatch or "";
postPatch = finalAttrs.postPatch or "";
excludePackages = builtins.map (dep: dep.passthru.lakePackageName or dep.pname) allLeanDeps;
}).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
);
in
{
strictDeps = true;
nativeBuildInputs = nativeBuildInputs ++ [
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 =
args.configurePhase or ''
runHook preConfigure
export HOME="$TMPDIR"
# Disable Lake 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/
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
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"
done | jq -s '.'
)" '{schemaVersion: "1.1.0", packages: $pkgs}' > .lake/package-overrides.json
fi
runHook postConfigure
'';
buildPhase =
args.buildPhase or ''
runHook preBuild
local targets="${lib.concatStringsSep " " buildTargets}"
echo "buildLakePackage: building ''${targets:-default targets}"
lake build --no-ansi $targets
runHook postBuild
'';
installPhase =
args.installPhase or (
if isLibrary then
''
runHook preInstall
# Install the complete Lake package tree. $out/ IS the
# package directory — source, lakefile, and pre-built
# artifacts under .lake/build/.
cp -rT . "$out"
# Remove build-environment artifacts that reference the
# build sandbox or dependency store paths.
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.
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
if [ -f "$exe" ] && [ -x "$exe" ]; then
ln -s "../.lake/build/bin/$(basename "$exe")" "$out/bin/$(basename "$exe")"
fi
done
fi
runHook postInstall
''
else
''
runHook preInstall
# Install executables only.
if [ -d .lake/build/bin ]; then
mkdir -p "$out/bin"
find .lake/build/bin -type f -executable \
-exec install -Dm755 {} "$out/bin/" \;
fi
runHook postInstall
''
);
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;
};
meta = meta // {
platforms = meta.platforms or lean4.meta.platforms;
};
};
}
pkgs/build-support/lake/fetch-lake-deps.nix
+95
View File
@@ -0,0 +1,95 @@
# fetchLakeDeps: fixed-output derivation that fetches Lake dependencies.
#
# Reads lake-manifest.json from the source tree, clones each git
# dependency at its pinned revision, and produces a directory of
# package sources. The output is hash-verified via `lakeHash`.
#
# This follows the same pattern as buildGoModule's `goModules` FOD.
{
lib,
stdenvNoCC,
gitMinimal,
cacert,
jq,
}:
{
name,
src,
hash,
sourceRoot ? "",
patches ? [ ],
prePatch ? "",
postPatch ? "",
# Package names to skip (e.g. already packaged in nix).
excludePackages ? [ ],
}:
stdenvNoCC.mkDerivation {
name = "${name}-lake-deps";
inherit
src
sourceRoot
patches
prePatch
postPatch
;
nativeBuildInputs = [
gitMinimal
cacert
jq
];
impureEnvVars = lib.fetchers.proxyImpureEnvVars ++ [
"GIT_PROXY_COMMAND"
"SOCKS_SERVER"
];
dontConfigure = true;
buildPhase = ''
runHook preBuild
if [ ! -f lake-manifest.json ]; then
echo "fetchLakeDeps: lake-manifest.json not found" >&2
exit 1
fi
export HOME="$TMPDIR"
export GIT_SSL_CAINFO="$NIX_SSL_CERT_FILE"
mkdir -p "$TMPDIR/packages"
jq -c --argjson exclude ${lib.escapeShellArg (builtins.toJSON excludePackages)} \
'.packages[] | select(.type == "git") | select(.name as $n | $exclude | index($n) | not)' \
lake-manifest.json | while IFS= read -r pkg; do
name=$(echo "$pkg" | jq -r '.name')
url=$(echo "$pkg" | jq -r '.url')
rev=$(echo "$pkg" | jq -r '.rev')
echo "fetchLakeDeps: cloning $name ($url @ $rev)"
git clone --filter=blob:none --no-checkout "$url" "$TMPDIR/packages/$name"
git -C "$TMPDIR/packages/$name" checkout "$rev" --quiet
# Remove .git to make output deterministic
rm -rf "$TMPDIR/packages/$name/.git"
done
runHook postBuild
'';
installPhase = ''
runHook preInstall
mv "$TMPDIR/packages" "$out"
runHook postInstall
'';
dontFixup = true;
outputHashMode = "recursive";
outputHash = hash;
outputHashAlgo = if hash == "" then "sha256" else null;
}
pkgs/build-support/lake/setup-hook.sh
+8
View File
@@ -0,0 +1,8 @@
addLeanPath() {
local buildLib="$1/.lake/build/lib/lean"
if [ -d "$buildLib" ]; then
addToSearchPath LEAN_PATH "$buildLib"
fi
}
addEnvHooks "$hostOffset" addLeanPath
pkgs/build-support/lake/test/default.nix
+8
View File
@@ -0,0 +1,8 @@
{
lib,
callPackage,
}:
lib.recurseIntoAttrs {
weak-minimax = callPackage ./weak-minimax/package.nix { };
}
pkgs/build-support/lake/test/weak-minimax/Main.lean
+4
View File
@@ -0,0 +1,4 @@
import WeakMinimax
def main : IO Unit := do
IO.println "weak_minimax: verified (maximin <= minimax)"
pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean
+9
View File
@@ -0,0 +1,9 @@
import Mathlib.Order.CompleteLattice.Basic
/-- Weak minimax inequality (weak duality): maximin ≤ minimax.
For any payoff f into a complete lattice, the best worst-case guarantee
for the maximizing player never exceeds the minimax value. -/
theorem weak_minimax {ι κ α : Type*} [CompleteLattice α]
(f : ι → κ → α) :
⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j :=
iSup_iInf_le_iInf_iSup f
pkgs/build-support/lake/test/weak-minimax/lakefile.lean
+12
View File
@@ -0,0 +1,12 @@
import Lake
open Lake DSL
package weakMinimax
require "leanprover-community" / "mathlib" @ git "main"
@[default_target] lean_lib WeakMinimax
@[default_target]
lean_exe weakMinimax.run where
root := `Main
pkgs/build-support/lake/test/weak-minimax/package.nix
+40
View File
@@ -0,0 +1,40 @@
# 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,
}:
let
inherit (leanPackages) buildLakePackage mathlib;
testPackage = buildLakePackage {
pname = "weak-minimax";
version = "0";
src = ./.;
leanDeps = [ mathlib ];
};
in
runCommand "buildLakePackage-weak-minimax"
{
nativeBuildInputs = [ testPackage ];
}
''
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"
''
pkgs/by-name/le/lean4/package.nix
+1
View File
@@ -98,6 +98,7 @@ stdenv.mkDerivation (finalAttrs: {
maintainers = with lib.maintainers; [
danielbritten
jthulhu
nadja-y
];
mainProgram = "lean";
};
pkgs/development/lean-modules/Cli/default.nix
+26
View File
@@ -0,0 +1,26 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
}:
buildLakePackage {
pname = "lean4-cli";
version = "4.28.0";
src = fetchFromGitHub {
owner = "leanprover";
repo = "lean4-cli";
tag = "v4.28.0";
hash = "sha256-9nX+dozmDAaVb5uKWL14zbILr7aqbVerTyPcN12Niw4=";
};
leanPackageName = "Cli";
meta = {
description = "Command-line argument parser for Lean 4";
homepage = "https://github.com/leanprover/lean4-cli";
license = lib.licenses.mit;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/LeanSearchClient/default.nix
+33
View File
@@ -0,0 +1,33 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
}:
buildLakePackage {
pname = "lean4-LeanSearchClient";
# No lockstep tags; version pinned by mathlib's lake-manifest.json.
version = "0-unstable-2026-02-12";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "LeanSearchClient";
rev = "c5d5b8fe6e5158def25cd28eb94e4141ad97c843";
hash = "sha256-L2aAwn3OeRLVt/VccLdBS0ogqmIIKAwnz94PpAOhaRc=";
};
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";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/Qq/default.nix
+26
View File
@@ -0,0 +1,26 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
}:
buildLakePackage {
pname = "lean4-Qq";
version = "4.28.0";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "quote4";
tag = "v4.28.0";
hash = "sha256-BRrSdDJQAsgM/NeSL2FODCez/8zEffjDRWUToGlKDNQ=";
};
leanPackageName = "Qq";
meta = {
description = "Lean 4 compile-time quote and antiquote macros for metaprogramming";
homepage = "https://github.com/leanprover-community/quote4";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/aesop/default.nix
+28
View File
@@ -0,0 +1,28 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
batteries,
}:
buildLakePackage {
pname = "lean4-aesop";
version = "4.28.0";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "aesop";
tag = "v4.28.0";
hash = "sha256-KeP46qtEf4/lgi4iCVuYIQbazufTR4luTbsuia9JkK4=";
};
leanPackageName = "aesop";
leanDeps = [ batteries ];
meta = {
description = "White-box automation for Lean 4";
homepage = "https://github.com/leanprover-community/aesop";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/batteries/default.nix
+26
View File
@@ -0,0 +1,26 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
}:
buildLakePackage {
pname = "lean4-batteries";
version = "4.28.0";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "batteries";
tag = "v4.28.0";
hash = "sha256-3N1MCFsg5UiwBCMAhDK7WwIowMNnhjlFgAsm0UPtGKc=";
};
leanPackageName = "batteries";
meta = {
description = "The batteries-included extended library for Lean 4";
homepage = "https://github.com/leanprover-community/batteries";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/importGraph/default.nix
+28
View File
@@ -0,0 +1,28 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
Cli,
}:
buildLakePackage {
pname = "lean4-importGraph";
version = "4.28.0";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "import-graph";
tag = "v4.28.0";
hash = "sha256-fZS8bFQjV7eLZCJwD+SVRzmCcCthrl+PO8vL8U8AOYs=";
};
leanPackageName = "importGraph";
leanDeps = [ Cli ];
meta = {
description = "Tools to analyse and visualise Lean 4 import structures";
homepage = "https://github.com/leanprover-community/import-graph";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/mathlib/default.nix
+47
View File
@@ -0,0 +1,47 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
batteries,
aesop,
Qq,
proofwidgets,
plausible,
LeanSearchClient,
importGraph,
tests,
}:
buildLakePackage {
pname = "lean4-mathlib";
version = "4.28.0";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "mathlib4";
tag = "v4.28.0";
hash = "sha256-7kR0WvEDey5kEdqKKVEO/JgQd1VyB6a+zwPvIV5E5Pg=";
};
leanPackageName = "mathlib";
leanDeps = [
batteries
aesop
Qq
proofwidgets
plausible
LeanSearchClient
importGraph
];
passthru.tests = {
inherit (tests.lake) weak-minimax;
};
meta = {
description = "Mathematical library for Lean 4";
homepage = "https://github.com/leanprover-community/mathlib4";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/plausible/default.nix
+26
View File
@@ -0,0 +1,26 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
}:
buildLakePackage {
pname = "lean4-plausible";
version = "4.28.0";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "plausible";
tag = "v4.28.0";
hash = "sha256-xuOfeoRPt5L0Rk4fEJPIi1A0aoNIkC1fsh5yeIx5bFI=";
};
leanPackageName = "plausible";
meta = {
description = "Property-based testing framework for Lean 4";
homepage = "https://github.com/leanprover-community/plausible";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/proofwidgets/default.nix
+68
View File
@@ -0,0 +1,68 @@
{
lib,
buildLakePackage,
fetchFromGitHub,
fetchNpmDeps,
npmHooks,
nodejs,
}:
let
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "ProofWidgets4";
tag = "v0.0.87";
hash = "sha256-qXEqNfwUBPnxAtLRkBZTBFhrM4JYl43gLo/PM6HOG7o=";
};
in
buildLakePackage {
pname = "lean4-proofwidgets";
version = "0.0.87";
inherit src;
leanPackageName = "proofwidgets";
# ProofWidgets has no Lean dependencies (lake-manifest.json packages = []).
lakeHash = null;
nativeBuildInputs = [
nodejs
npmHooks.npmConfigHook
];
# Pre-fetched npm dependencies for the TypeScript widget build
# (npm/rollup in widget/). npmConfigHook installs these offline.
npmDeps = fetchNpmDeps {
name = "lean4-proofwidgets-npm-deps";
inherit src;
sourceRoot = "source/widget";
hash = "sha256-CzBRrreOSytquZ/xFHPlY8r+lz5Bg9Zk9ienRhc8SiY=";
};
npmRoot = "widget";
# Lake's widgetJsAll target runs `npm clean-install` which wipes
# node_modules and the patched shebangs that npmConfigHook applied.
# Wrap npm to skip ci/clean-install (deps already installed) while
# passing `npm run build` through — same pattern as llama-cpp/evcc.
postConfigure = ''
local realNpm
realNpm="$(type -P npm)"
mkdir -p "$TMPDIR/npm-wrap"
cat > "$TMPDIR/npm-wrap/npm" <<WRAPPER
#!/bin/sh
case "\$1" in ci|clean-install) exit 0 ;; esac
exec "$realNpm" "\$@"
WRAPPER
chmod +x "$TMPDIR/npm-wrap/npm"
export PATH="$TMPDIR/npm-wrap:$PATH"
'';
meta = {
description = "Interactive UI framework for Lean 4 proof assistants";
homepage = "https://github.com/leanprover-community/ProofWidgets4";
license = lib.licenses.asl20;
maintainers = with lib.maintainers; [ nadja-y ];
};
}
pkgs/development/lean-modules/update.sh
Executable
+83
View File
@@ -0,0 +1,83 @@
#!/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.
#
# Usage:
# ./pkgs/development/lean-modules/update.sh
set -euo pipefail
lean4_version=$(nix eval --raw .#lean4.version)
# Snapshot current versions for diffing.
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 "")
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
echo "ERROR: mathlib dependency set has changed" >&2
echo " expected: $known_deps" >&2
echo " got: $manifest_deps" >&2
exit 1
fi
pw_version=$(echo "$manifest" | jq -r '.packages[] | select(.name == "proofwidgets") | .inputRev' | sed 's/^v//')
lsc_rev=$(echo "$manifest" | jq -r '.packages[] | select(.name == "LeanSearchClient") | .rev')
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"
# LeanSearchClient has no lockstep tags; pin to the exact rev mathlib uses.
update-source-version leanPackages.LeanSearchClient "$lsc_version" \
--rev="$lsc_rev"
# Packages with leanDeps.
nix-update leanPackages.aesop --version="$lean4_version"
nix-update leanPackages.importGraph --version="$lean4_version"
# mathlib (all deps are nix-packaged, no lakeHash needed).
nix-update leanPackages.mathlib --version="$lean4_version"
# 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
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
fi
pkgs/test/default.nix
+2
View File
@@ -172,6 +172,8 @@ in
go = recurseIntoAttrs (callPackage ../build-support/go/tests.nix { });
lake = callPackage ../build-support/lake/test { };
pkg-config = recurseIntoAttrs (callPackage ../top-level/pkg-config/tests.nix { });
buildRustCrate = recurseIntoAttrs (callPackage ../build-support/rust/build-rust-crate/test { });
pkgs/top-level/all-packages.nix
+4
View File
@@ -307,6 +307,8 @@ with pkgs;
buildFHSEnvChroot = callPackage ../build-support/build-fhsenv-chroot { }; # Deprecated; use buildFHSEnv/buildFHSEnvBubblewrap
buildFHSEnvBubblewrap = callPackage ../build-support/build-fhsenv-bubblewrap { };
buildLakePackage = callPackage ../build-support/lake { };
cameractrls-gtk4 = cameractrls.override { withGtk = 4; };
cameractrls-gtk3 = cameractrls.override { withGtk = 3; };
@@ -2845,6 +2847,8 @@ with pkgs;
leanblueprint = with python3Packages; toPythonApplication leanblueprint;
leanPackages = callPackage ../top-level/lean-packages.nix { };
inherit (callPackage ../development/tools/lerna { })
lerna_6
lerna_8
pkgs/top-level/lean-packages.nix
+45
View File
@@ -0,0 +1,45 @@
# Lean 4 package set.
#
# 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:
# 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;
# 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 { };
})