RFC: lake new project depending on std by default

[AdrienChampion]

Proposal

It is expected that most Lean users want to depend on std as it gives access to many more basic lemmas on very common types (Nat, List, Array, ...) and provides a whole lot of types not found in core.

As such, the proposal (originally pushed by @digama0 and @tydeu on zulip) is to have the dependency to std in the default lakefile.lean typically generated on lake new.

A minor side-effect is that it would display how to depend on a repository (and would probably be completed with a link to lake's manual), as opposed to the current version which does not mention dependencies at all.

Community Feedback

• zulip thread

The main points from the thread to highlight are

• currently, this change would mean that lake new proj ; cd proj ; lake build would fail as a lake update is required to generate the manifest needed by lake build

  This is not great (new) user experience, however according to @tydeu starting in v4.3.0-rc1 lake build no longer requires the lake update ---at least in the case of a new project.

• a bigger problem is that, according to @tydeu again:

  The only significant wrinkle with turning the current suggestion into a PR is that the tests in the Lean core are not suppose to download packages and thus this change will break all the init tests. Therefore, it may be necessary to some option (like an LAKE_INIT_NO_DEPS environment variable) for new/init uses in core.

  The problem is slightly more general than this however as pointed out by @digama0 (and confirmed by @tydeu):

  I think you have a similar need for that for the lake init foo math tests, which currently use sed to delete the mathlib import IIRC

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.