Files
nixpkgs/pkgs/development/lean-modules/LeanSearchClient/default.nix
Nadja Yang 6987e3afbe leanPackages.lean4: 4.29.0 -> 4.29.1
Strip ephemeral setup.json build artifacts from library outputs.
These are produced per-module during compilation and not included
in upstream cache distributions
(https://github.com/NixOS/nixpkgs/issues/510957).

Disable Hydra builds for mathlib since the output exceeds the NAR
size limit.

Pre-build static library for batteries so downstream executables
can link against it.

Refactor update.sh to pin each dependency to the rev from mathlib's
lake-manifest.json.
2026-06-04 16:48:52 -04:00

28 lines
699 B
Nix

{
lib,
buildLakePackage,
fetchFromGitHub,
}:
buildLakePackage {
pname = "lean4-LeanSearchClient";
# nixpkgs-update: no auto update
version = "4.12.0-unstable-2026-02-12";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "LeanSearchClient";
rev = "c5d5b8fe6e5158def25cd28eb94e4141ad97c843";
hash = "sha256-L2aAwn3OeRLVt/VccLdBS0ogqmIIKAwnz94PpAOhaRc=";
};
leanPackageName = "LeanSearchClient";
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 ];
};
}