Skip to content

leanPackages.lean4: 4.29.0 -> 4.29.1#511524

Open
nadja-y wants to merge 1 commit intoNixOS:masterfrom
nadja-y:pr-lean-429-1
Open

leanPackages.lean4: 4.29.0 -> 4.29.1#511524
nadja-y wants to merge 1 commit intoNixOS:masterfrom
nadja-y:pr-lean-429-1

Conversation

@nadja-y
Copy link
Copy Markdown
Contributor

@nadja-y nadja-y commented Apr 19, 2026 •
edited
Loading

Strip setup.json build artifacts from library outputs. These are produced per-module during compilation and not included in upstream cache distributions (#510957).

Disable Hydra builds for mathlib since the output still 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.

@nixpkgs-ci nixpkgs-ci Bot requested a review from philiptaron April 19, 2026 19:28
@nixpkgs-ci nixpkgs-ci Bot added 10.rebuild-linux: 1-10 This PR causes between 1 and 10 packages to rebuild on Linux. 10.rebuild-darwin: 1-10 This PR causes between 1 and 10 packages to rebuild on Darwin. 11.by: package-maintainer This PR was created by a maintainer of all the package it changes. labels Apr 19, 2026
@nadja-y
Copy link
Copy Markdown
Contributor Author

nadja-y commented Apr 19, 2026

@xhalo32 re: #497946 (comment) — this PR fixes the batteries link error. The manual section covers buildLakePackage usage. The lean.nix overlay is no longer needed; leanPackages.lean4 includes the patched toolchain that enables LSP integration.

@nadja-y nadja-y changed the title leanPackages: lean4 4.29.0 -> 4.29.1 leanPackages.lean4: 4.29.0 -> 4.29.1 Apr 19, 2026
@nadja-y nadja-y mentioned this pull request Apr 19, 2026
Closed
@nixpkgs-ci nixpkgs-ci Bot added the 8.has: package (update) This PR updates a package to a newer version label Apr 19, 2026
@nadja-y nadja-y requested a review from RaitoBezarius April 20, 2026 12:04
@nadja-y nadja-y requested a review from drupol April 20, 2026 21:36
@nadja-y nadja-y marked this pull request as draft April 21, 2026 18:42
@nadja-y
leanPackages.lean4: 4.29.0 -> 4.29.1
1366bc3 
Strip setup.json build artifacts from library outputs. These are
produced per-module during compilation and not included in upstream
cache distributions (NixOS#510957).

Disable Hydra builds for mathlib since the output still 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.
@nadja-y nadja-y marked this pull request as ready for review April 22, 2026 02:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@philiptaron philiptaron Awaiting requested review from philiptaron

@RaitoBezarius RaitoBezarius Awaiting requested review from RaitoBezarius

@drupol drupol Awaiting requested review from drupol

Assignees

No one assigned

Labels

8.has: package (update) This PR updates a package to a newer version 10.rebuild-darwin: 1-10 This PR causes between 1 and 10 packages to rebuild on Darwin. 10.rebuild-linux: 1-10 This PR causes between 1 and 10 packages to rebuild on Linux. 11.by: package-maintainer This PR was created by a maintainer of all the package it changes.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@nadja-y