fix: error on unknown package names in lake update

[sankalpsthakur]

This PR makes lake update <pkg>... fail with a clear error when a specified package name is not known to the current dependency manifest. Previously, unknown or misspelled names (including case mismatches) were silently ignored, which was confusing.

Summary

Selective-update names are validated inside reuseManifest against the already loaded manifest, avoiding a duplicate manifest load. This preserves Lake's ability to update a package that remains recorded in the manifest after its direct require was removed, while rejecting names that are genuinely unknown. Matching is case-sensitive, following Lake's existing package-name semantics.

Unknown names produce a non-zero exit with:

error: unknown package `does-not-exist`

Successful paths are unchanged:

• bare lake update (update all dependencies)
• lake update <valid-dep> (selective update of a known dependency)
• selective update of a package retained in the manifest after its require was removed

Changes

• src/lake/Lake/Load/Resolve.lean: validate toUpdate names in reuseManifest using the manifest that function already loaded; the detailed contract docstring lives there
• tests/lake/tests/updateUnknown/: focused CLI coverage for unknown names, case mismatches, mixed valid/invalid args, successful paths, and a retained manifest package

Validation

• Confirmed stock Lake (v4.32.2) exits 0 with no error for lake update does-not-exist (repro of the bug)

• Full Lean bootstrap / Lake rebuild was not run locally because Lean is unavailable in the execution environment

• The focused test runs under the normal Lake test suite in CI:

  tests/lake/run_test.sh tests/updateUnknown
  

AI disclosure

AI tools assisted with locating the Lake update path, drafting the change, and preparing the PR. I reviewed the logic against reuseManifest, selective-update behavior, and Lake's existing unknown package error style.

Closes #12005
Closes #2772

[sankalpsthakur]

Pushed a fix so selective lake update still accepts packages present in the manifest (restores depTree); could a maintainer please add the changelog-lake label? External contributors cannot add labels.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea9fad0706f0b1da2467195dae75480595640670 --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-01 10:37:08)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ea9fad0706f0b1da2467195dae75480595640670 --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-08-01 10:37:09)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ea9fad0706f0b1da2467195dae75480595640670 --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-01 19:11:28)

[tydeu]

Thanks, I like the check! However, I have some comments on code location (see below).

[sankalpsthakur]

@tydeu The requested relocation is complete: validation now lives in reuseManifest, uses the already-loaded manifest, and the detailed contract is documented there. The retained-manifest-package regression is included and current Lean CI is green. Ready for re-review.

[tydeu]

LGTM! Thank you! 🎉

[sankalpsthakur]

Thanks for the re-review. GitHub still shows the earlier CHANGES_REQUESTED review as the latest formal review state even though the thread is resolved and you confirmed LGTM. Could you please submit an approval or dismiss the stale review when convenient so the PR is no longer blocked administratively?