nixpkgs/pkgs/development/lean-modules/batteries/default.nix
Niklas Halonen a26b66330f
lean4: update leanPackages and lean4 4.29.0/1 -> 4.30.0
As reported on FreeBSD forums, updating lean4 to 4.30.0 fails to a
leantar related issue.  We follow the patch mentioned on the FreeBSD
forums and depend on digama0/leangz (that comes with leantar).
However, there doesn't seem to be a reason to disable installing
leantar, so we don't set INSTALL_LEANTAR=OFF like the patch.

References:
- https://bugs.freebsd.org/bugzilla/show_bug.cgi?id=295656
- https://cgit.freebsd.org/ports/commit/?id=516f8a5764de5c7bdd0e9f7810601a5057bbc650
- https://lean-lang.org/doc/reference/latest/releases/v4.30.0/#release-v4___30___0
- leanprover/lean4#12822
2026-06-01 22:28:05 +03:00

39 lines
890 B
Nix

{
lib,
buildLakePackage,
fetchFromGitHub,
}:
buildLakePackage {
pname = "lean4-batteries";
version = "4.30.0";
src = fetchFromGitHub {
owner = "leanprover-community";
repo = "batteries";
tag = "v4.30.0";
hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
};
leanPackageName = "batteries";
# Pre-build static library for downstream executables.
# TODO: upstream this to batteries
postPatch = ''
substituteInPlace lakefile.toml \
--replace-fail '[[lean_lib]]
name = "Batteries"' '[[lean_lib]]
name = "Batteries"
defaultFacets = ["static"]'
'';
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
niklashh
];
};
}