RFC: std dependency in default lakefile

Stream: lean4

[Adrien Champion]

EDIT: this thread is a discussion related to (RFC) issue 2988. The original topic was documenting the syntax for lakefile-dependencies in the default lakefile (from lake new/lake init), until Mac Malone brought up that the default lakefile should probably depend on std, as that's what most people want.

I think it'd be nice if the default lakefile gave basic information about adding dependencies, especially for newcomers. Something like this maybe, which adds

-- add dependencies here, for instance
--
-- ```lean
-- require mathlib from git
--   "https://github.com/leanprover-community/mathlib4.git" @ "main"
-- ```
--
-- for more see <https://github.com/leanprover/lean4/tree/master/src/lake#adding-dependencies>.

Probably a bit overkill, the link might be enough.
Would the team welcome a PR on this?

[Adrien Champion]

Also, the link I added points directly to lake's readme on the lean4 repo, if there is a more polished version somewhere that would be more appropriate do let me know

[Scott Morrison]

I'd be in favour. I like configuration files containing nothing but comments. :-)

[Scott Morrison]

(Be careful of your example though; mathlib4 uses master not main.)

[Adam Topaz]

Can you also include an example illustrating a local dependency?

[Adrien Champion]

I can and kinda wanted to honestly, but I was trying to keep the size under control

[Adrien Champion]

Though, if we put this doc at the very end of the file (I'm assuming we can put deps there, can we?) then it's probably fine if it's a bit long for the sake of clarity

[Eric Wieser]

I'd suggest /- comments so that it's a bit easier for the user to copy working code

[Eric Wieser]

I also don't think we usually wrap the command in that style, which might be relevant for anyone doing dumb string parsing of the lakefile

[Adrien Champion]

Eric Wieser said:

I'd suggest /- comments so that it's a bit easier for the user to copy working code

Well the current doc uses -- even for multiline (see below), and also -- comments are how Cmd+/ (de)comments bits of code, so I'm not sure one would really copy/paste the commented code, just select both lines and Cmd+/ (and then copy/paste if they want)

lean_exe «bf» where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  supportInterpreter := true

[Adrien Champion]

Eric Wieser said:

I also don't think we usually wrap the command in that style, which might be relevant for anyone doing dumb string parsing of the lakefile

I'm not sure what the usual way is, but core sure features triple-backtick blocks (though not always with the lean language specifier). Quite a bit of them

Markdown does allow to 4-space-indent blocks of code to avoid triple-backtick I think, is that what the "usual way" is?

[Adrien Champion]

I'm fine with changing either of the things you pointed by the way, I was just explaining the rationale behind my version

[Adrien Champion]

Adam Topaz said:

Can you also include an example illustrating a local dependency?

I added one, fixed @Scott Morrison's note on master/main, and move the whole thing to the end of the file. Seems to me like it flows better that way

• link

[Mac Malone]

Adrien Champion said:

Eric Wieser said:

I'd suggest /- comments so that it's a bit easier for the user to copy working code

Well the current doc uses -- even for multiline (see below), and also -- comments are how Cmd+/ (de)comments bits of code, so I'm not sure one would really copy/paste the commented code, just select both lines and Cmd+/ (and then copy/paste if they want)

lean_exe «bf» where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  supportInterpreter := true

For my two cents, I agree with Eric. When it comes to -- and /- ... -/, there is threshold were it feels appropriate to switch from one to the other (for me, generally ~3 lines). This comment happens to just be under it, so it uses --. Inversely, the suggested comment is much longer, so it should use /- ... -/.

[Adrien Champion]

Makes sense, thanks @Mac Malone :smile:

Do you have thoughts on examples being in triple-backtick blocks?

[Mac Malone]

Another comment that has popped up is that it is likely we likely want to add a std dependency to the default template, which may solve this issue. That is, the addition could be this instead:

/-
Specify package dependencies here.
For more information, see [Adding Dependencies][1] in the Lake README.

[1]:  https://github.com/leanprover/lean4/tree/master/src/lake#adding-dependencies
-/
require std from git
  "https://github.com/leanprover/std4.git" @ s!"v{Lean.versionString}"

[Adrien Champion]

I would like that myself, though for beginner it means the default lake project does not lake build as you have to lake update first, right?

Do you think there is a good enough consensus on this for us to go straight to this version?

[Mac Malone]

Adrien Champion said:

Do you have thoughts on examples being in triple-backtick blocks?

The style looks good to me. One caveat is that docstrings should not generally have the lean specifier), as the highlighting only occurs in hovers if it does not have one (at least currently). However, that does not really relevant here, since this documentation will not appear in a hover.

[Mac Malone]

Adrien Champion said:

I would like that myself, though for beginner it means the default lake project does not lake build as you have to lake update first, right?

Not anymore, Lake will not perform an update if the manifest is missing (e.g.., for a new project).

[Adrien Champion]

Oh right, forgot I actually noticed this!

[Adrien Champion]

So we should probably just go for the version you propose then

[Adrien Champion]

(Though std is on leanprover not leanprover-community

[Adrien Champion]

I still get an error that the manifest's missing, am I doing something wrong?

problem

❯ elan which lake
[...]/.elan/toolchains/stable/bin/lake

❯ lake --version
Lake version 5.0.0-0d70514 (Lean version 4.2.0)

❯ lake build
error: missing manifest; use `lake update` to generate one

❯ bat lean-toolchain
───────┬─────────────────────────
       │ File: lean-toolchain
───────┼─────────────────────────
   1   │ stable
───────┴─────────────────────────

❯ bat lakefile.lean
───────┬─────────────────────────
       │ File: lakefile.lean
───────┼─────────────────────────
   1   │ import Lake
   2   │ open Lake DSL
   3   │
   4   │ package «testDefaultLakefile» where
   5   │   -- add package configuration options here
   6   │
   7   │ lean_lib «TestDefaultLakefile» where
   8   │   -- add library configuration options here
   9   │
  10   │ @[default_target]
  11   │ lean_exe «testdefaultlakefile» where
  12   │   root := `Main
  13   │   -- Enables the use of the Lean interpreter by the executable (e.g.,
  14   │   -- `runFrontend`) at the expense of increased binary size on Linux.
  15   │   -- Remove this line if you do not need such functionality.
  16   │   supportInterpreter := true
  17   │
  18   │ /-
  19   │ Specify package dependencies here.
  20   │ For more information, see [Adding Dependencies][1] in the Lake README.
  21   │
  22   │ [1]:  https://github.com/leanprover/lean4/tree/master/src/lake#adding-dependencies
  23   │ -/
  24   │ require std from git
  25   │   "https://github.com/leanprover/std4.git" @ s!"v{Lean.versionString}"
───────┴─────────────────────────

[Mario Carneiro]

There is another reason to prefer -- comments in an annotated lakefile or other config file, which is that you want the ability to selectively uncomment sections. If the whole thing is block commented this is more work

[Mario Carneiro]

(also the flipside of what was mentioned about vscode's Ctrl-/ shortcut is that it doesn't work to remove block comments, it only works with the singleline style)

[Adrien Champion]

Adrien Champion said:

Eric Wieser said:

I'd suggest /- comments so that it's a bit easier for the user to copy working code

Well the current doc uses -- even for multiline (see below), and also -- comments are how Cmd+/ (de)comments bits of code, so I'm not sure one would really copy/paste the commented code, just select both lines and Cmd+/ (and then copy/paste if they want)

lean_exe «bf» where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  supportInterpreter := true

@Mario Carneiro sounds familiar!

[Adrien Champion]

Though I do understand one may prefer multi-line visually. I come from Rust so I go for single-line by default, it’s just more convenient and makes writing markdown in docs make more sense as indentation has semantics

[Scott Morrison]

I think it's great that the default template lakefile will include Std.

We really want to push that all Lean users will not need to think about including Std, and it will only be people doing particularly esoteric or exciting things that need to remove the Std dependency.

[Mac Malone]

Adrien Champion said:

I still get an error that the manifest's missing, am I doing something wrong?

The automatic update change landed in v4.3.0-rc1, so your v4.2.0 is too old. The v4.3.0 stable should be out in a few days, so there should not be a long wait!

[Adrien Champion]

Alright I’ll wait until then then

[Mac Malone]

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.

[Mario Carneiro]

I think that's fine, secret environment variables like that are a reasonable way to handle nonstandard setups in tests and such

[Mario Carneiro]

(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)

[Adrien Champion]

And here I was thinking this would be the easiest PR ever

[Mario Carneiro]

one does not simply PR to lean4

[Adrien Champion]

Which is why I tried to PR lake instead but it ended up backfiring

[Adrien Champion]

Anyway, @Mario Carneiro @Mac Malone it seems like you like the env-var approach. It goes beyond the (very modest, on purpose) scope of my original PR embryo. Would this warrant a proper discussion through a RFC or something?

[Mario Carneiro]

Let Mac implement the env var stuff

[Adrien Champion]

I strongly second this plan, was not looking forward to it

[Mac Malone]

The sad part is that I will likely not be working much on maintaining Lake these next few weeks (as my focus is currently back on Reservoir), so leaving it up to me will mean this may get delayed a while.

[Mac Malone]

Also, in that case, making an issue would be a good way to keep track of when this is eventually implemented.

[Adrien Champion]

Renamed the thread and opened an RFC issue:

• https://github.com/leanprover/lean4/issues/2988

It's my first time doing this, do let me know if I messed up

[Adrien Champion]

@Mac Malone @Mario Carneiro I think there should probably be an issue specific to the env-var business. I could create one I guess, but I'm not familiar with the topic so writing an accurate, technical description is going to be difficult.
Any chance one of you guys could (tell someone qualifed to) do it?

[Mario Carneiro]

This is an issue internal to the lake project maintenance, so it's not really RFC material. It's up to Mac to handle this in the way he sees fit

[Adrien Champion]

You mean the issue I opened should not be a RFC? It was that or a bug, I thought RFC was more appropriate

[Mac Malone]

@Adrien Champion I think Mario meant the env-bar business should not be an (RFC) issue.

[Adrien Champion]

Oh, my bad, I thought it was clear I was asking for a regular issue, though I don’t know if “bug” is appropriate and since it’s that or RFC I understand the confusion

[Adrien Champion]

What I really meant was “somebody who knows about the env-var thingy should write something somewhere to track this aspect in particular”

[Mac Malone]

Since it is an implementation detail, I think the link to this Zulip thread from the RFC issue is sufficient tracking.