feat: lake flag to skip dependency materialization (offline/bundled use) #13101

We're building a tool to create self-contained offline bundles of Lean 4 projects for teaching (https://github.com/leanprover-community/bundle, discussed at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/trylean.20bundle.20for.20lean4). The idea is that students download a zip, unpack it, and have a working Lean setup with no network access and no git.

Currently lake build --no-build always runs materializeDeps, which runs git commands for every git-type dependency in the manifest, even though --no-build implies we believe everything is already in place. This means lake build --no-build can't be used offline if the manifest has git deps.

It would be great to have a flag (e.g. --offline or --no-fetch) that tells Lake to skip all git operations during dependency resolution. The semantics would be: trust that .lake/packages/ already contains the right sources, and just load the workspace from what's on disk.

Workaround

Our current workaround is to rewrite lake-manifest.json in the bundle, converting all "type": "git" entries to "type": "path" pointing at the local .lake/packages/ directories. validateManifest only warns on the source-kind mismatch, so this works, but it's hackish and means the manifest no longer reflects how the project was actually built.

Context

This came up while working on the discussion at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/trylean.20bundle.20for.20lean4. Patrick Massot and other teachers need bundles that work without git, network access, or any installation.

See also #12901 which describes a related problem (Lake deleting packages before verifying fetch succeeds).