feat: commit lake-manifest.json

[tydeu]

This is needed for Lake & Reservoir to correctly identify the name of the package (since its name is std despite the repository being named std4). Without this, either Lake will fail to look up the package on require leanprover/std (because no leanprover/std package exists on Reservoir) or require leanprover/std4 will succeed but Lake will error when the package's name does not match std4. This is currently blocking leanprover/lean4#3174.

[tydeu]

awaiting-review

[joehendrix]

I did an experiment on main and with this manifest I get the following messages when building with documentation on:

> lake build -R -Kdoc=on
error: missing manifest; use `lake update` to generate one
> lake update           
> lake build -R -Kdoc=on
[0/4] Building Std.Classes.BEq
..

Does leanprover/lean4#3174 fix the error message above? It seems like lake should regenerate the manifest automatically when reconfiguring since the requirements may change.

We may also want the manifest generated with -Kdoc=on if we include a manifest.

[tydeu]

@joehendrix Oops! Sorry, I forgot to include doc-gen4 in the manifest. With current Lake, you need to run lake -R -Kdoc=on update to generate a complete manifest for std4. leanprover/lean4#3174 will resolve this by automatically including all conditional dependencies in the manifest.

[digama0]

I think we should remove the doc-gen4 pins from this manifest. Std does not build with doc-gen4, and having a doc-gen pin is misleading. See also the discussion on Zulip.