Lake Development: Extending the extension

Stream: lean4

[Shreyas Srinivas]

Hello everyone,

@Kevin Buzzard and I were discussing about how lake works in relation to a recent thread. There are two lines of thought in how lake should develop:

1. One line of thought would like to see lake develop into a proper build and dependency management tool that can handle a wide range of projects in line with lean's goals to be a programming language beyond just mathematics. This means adapting changes carefully, in a way that works for non-mathlib users as much as mathlib users and developers.
2. Another line of thought suggests that given that the current majority of users are largely working on math, it is fine to make quick changes that work for them even if it might not work for the handful of others. These changes are often as simple as copying a lean-toolchain file from the mathlib directory. A crucial concern motivating this is that new math users, including students, are not command-line savvy and complicating their life with more CLI usage is terrible. In fact, if everything could be done within vscode without dealing with lake issues, then they would take that approach.

One way that has been suggested is to add special sticky defaults for mathprojects, or maybe add a math option to lake that makes the relevant commands do sane default actions. There are a few drawbacks to this option:

1. It adds a bunch of stuff to lake that has to be refactored away when more systematic solutions are implemented (for example dependency management for stable lean toolchains and mathlib releases sometime in the future). This is technical debt.
2. Math users still have to do stuff on the CLI.

Many of the sane defaults that mathlib users request involve UX issues, such as automating the execution of some additional commands after operations like lake update. This can be accomplished in the extension. So after discussing with @Kevin Buzzard I have the following suggestion for many of these requests for changes:

1. To implement a side panel for lake (as in latex-workshop, vscoq,...) in the vscode extension. This side panel has nice gui options for standard lake operations, with descriptive titles.
2. These options implement the sane defaults that math-heavy users seek.
3. Changes to lake behaviour that mainly math users consider a necessary and immediate QoL improvement are first implemented here, and only if this is impossible, then changes are added to lake itself.
4. lake development continues as it is.
5. Math heavy users are encouraged to use the vscode panel.

[James Gallicchio]

My 2c, lake is doing too much right now, not too little. It also follows the toolchain release cycle, which is slower than I assume mathlib maintainers would like.

I'd suggest Mathlib maintain a wrapper around lake that encodes mathlib-specific workflows and simplifies CLI stuff for most users. Then, maybe CLI is simple enough for most users, and you don't need vscode side panel stuff?

[Shreyas Srinivas]

James Gallicchio said:

My 2c, lake is doing too much right now, not too little. It also follows the toolchain release cycle, which is slower than I assume mathlib maintainers would like.

I'd suggest Mathlib maintain a wrapper around lake that encodes mathlib-specific workflows and simplifies CLI stuff for most users. Then, maybe CLI is simple enough for most users, and you don't need vscode side panel stuff?

As Kevin told me, math people dread the CLI. So the less they need the CLI, the better.

[Shreyas Srinivas]

What we in CS consider a "simplified CLI" might already be too much for non-CS people, which is perfectly reasonable. It is not part of their day to day usage.

[James Gallicchio]

Makes sense. I think a simple vscode extension (separate from the main lean4 extension) to add a side panel should be pretty straightforward?

[Shreyas Srinivas]

A lot of requests for math specific conveniences are essentially saying "here's the sane default sequence of commands for math, why can't lake just do it". But lake doesn't have to do it. The extension can do it too.

[Shreyas Srinivas]

James Gallicchio said:

Makes sense. I think a simple vscode extension (separate from the main lean4 extension) to add a side panel should be pretty straightforward?

Probably. This should add no extra burden to users, since vscode allows extension packs.

[Marc Huisinga]

There will be a menu frontend for many common Lake commands in the next release of the VS Code extension, but it won't magically solve all the issues that people are having with lake.
I want to provide more UI support for all things related to projects in the future, but it'll take some time to get there.

Generally speaking, the same quality standards that apply to Lake should also apply to the extension. Supporting mathlib specially in the VS Code extension is good if it helps Mathlib users be productive, but we shouldn't cut corners and add features that are broken when not using Mathlib. At worst, they should explicitly declare that they are being used in the wrong context.

[Shreyas Srinivas]

As @James Gallicchio suggests, we could go for a separate extension for this. Then math users could ask their students to use the extension pack

[James Gallicchio]

(with a careful warning to math users to not touch the lake UI in the next release of the VS Code extension! :joy:)

As a non-math user I am nonetheless excited for the lake frontend :)

[Shreyas Srinivas]

Also @Marc Huisinga : I see my suggestion more as a layer of UX on top of lake with sane defaults that addresses many concerns that non-CS math users have, until lake matures, and the UI parts just implement lake commands.

[Marc Huisinga]

It would be helpful if you were more specific regarding "sane defaults". What is the exhaustive list of features that you want your extension to support for Mathlib and projects downstream of Mathlib in particular?

[Shreyas Srinivas]

Math people would have a more comprehensive list, but I'll start with two:

1. For updating toolchains, afterlake update for mathlib projects, the lean-toolchain must be copied from mathlib's toolchain. This addresses the concerns of Patrick from the linked thread.
2. For math projects, run lake exe cache get before starting a build. Currently vscode starts its own build process rather than cache first.

[Marc Huisinga]

Shreyas Srinivas said:

Math people would have a more comprehensive list, but I'll start with two:

1. For updating toolchains, afterlake update for mathlib projects, the lean-toolchain must be copied from mathlib's toolchain. This addresses the concerns of Patrick from the linked thread. Rerun cache, before building.
2. For math projects, run lake exe cache get! before starting a build, or after a project has been opened and no oleans are found. Currently vscode starts its own build process.

1. is on my to-do list (updating lean-toolchain before lake update, though), 2. is already done when creating new math projects downstream of Mathlib (in my local branch) but could be extended to existing projects as well.

I think both of these should just be supported in the main extension. "Use this extra extension with this side panel instead of the one provided by the official extension" risks introducing another layer of confusion.

[Eric Wieser]

I've filed https://github.com/leanprover/lake/issues/180 for 1.

[Eric Wieser]

I don't think this (edit: 1.) needs any mathlib customization or a vscode extension

[Shreyas Srinivas]

Eric Wieser said:

I don't think this needs any mathlib customization or a vscode extension

I suspect the reason the new extension idea came up is that math users could install it and modify it for QoL improvements over lake, without being held up by the main extension development (for which we just learnt about the planned side panel).

[Marc Huisinga]

Shreyas Srinivas said:

Eric Wieser said:

I don't think this needs any mathlib customization or a vscode extension

I suspect the reason the new extension idea came up is that math users could install it and modify it for QoL improvements over lake, without being held up by the main extension development.

I think this idea is worth considering if there are any examples that we do not intend to implement in the official extension soon, or if they are genuinely incompatible with general usage. The ones listed so far seem perfectly fine to add to the official tooling.

[Shreyas Srinivas]

Isn't cache math-specific at the moment? A number of sensible default behaviours regarding this (like clean, get, get!) could therefore be math specific right?

[Marc Huisinga]

As mentioned earlier, I want the extension to support Mathlib and projects downstream of Mathlib specially. It should just keep working fine when used outside of this context and make it clear that commands related to Mathlib cannot be used.
For example, adjusting the "Lake update" command to always pull Mathlib's toolchain would not always be a good idea. Adding an "Update Mathlib" command that does this and displays a helpful error when used outside of Mathlib would be fine.

[Kevin Buzzard]

Right now lake is quick to suggest lake update as a solution, and right now this breaks things more often than not for mathematician users: the moment one thing goes wrong, lake suggests lake update, the user tries it and now lots of things have gone wrong.

[Shreyas Srinivas]

Marc Huisinga said:

For example, adjusting the "Lake update" command to always pull Mathlib's toolchain would not always be a good idea. Adding an "Update Mathlib" command that does this and displays a helpful error when used outside of Mathlib would be fine.

I like the idea of an update mathlib command on the proposed side panel. We should also probably give them a reset or clean option for the dependencies in case something goes wrong and users don't know how to get back to a sane state. I guess this is already part of your planned panel. This should go a long way to reduce CLI usage after a new project is initialised.

[Sebastian Ullrich]

Kevin Buzzard said:

Right now lake is quick to suggest lake update as a solution, and right now this breaks things more often than not for mathematician users: the moment one thing goes wrong, lake suggests lake update, the user tries it and now lots of things have gone wrong.

This is addressed in the next release (lean4#2525)

[Eric Wieser]

I thought this was already addressed by the introduction of inherited in the lake manifest, which we have had for a while?

[Marc Huisinga]

Shreyas Srinivas said:

Marc Huisinga said:

For example, adjusting the "Lake update" command to always pull Mathlib's toolchain would not always be a good idea. Adding an "Update Mathlib" command that does this and displays a helpful error when used outside of Mathlib would be fine.

I like the idea of an update mathlib command on the proposed side panel. We should also probably give them a reset or clean option for the dependencies in case something goes wrong and users don't know how to get back to a sane state. I guess this is already part of your planned panel. This should go a long way to reduce CLI usage after a new project is initialised.

image.png
;-)

[Patrick Massot]

Marc Huisinga said:

Adding an "Update Mathlib" command that does this and displays a helpful error when used outside of Mathlib would be fine.

Why not simply not displaying that "Update Mathlib" command for project that do not depend on Mathlib?

[Patrick Massot]

I like the idea of having a nice interface in the VSCode extension since I see so many students that are completely unable to use a terminal. But it would be nice to also have a usable client. Also remember some people use other editors. Of course we could say that people who insist to use vim or emacs don't need any interface, but they still need a usable cli.

[Shreyas Srinivas]

That goes back to my post at the top of this thread. Basically there are two concurrent goals. Get lake usable easily for math users who also coincidentally happen to be averse to CLIs, while allowing lake to mature into the build and dependency manager that lean, the language requires. One which properly manages builds, versions of dependencies, version conflicts etc. It also separates the UX concern which might be of immediate relevance for new users or teaching, from the dependency management concern that, I am guessing, will take time to fully develop.

[Marc Huisinga]

Patrick Massot said:

Marc Huisinga said:

Adding an "Update Mathlib" command that does this and displays a helpful error when used outside of Mathlib would be fine.

Why not simply not displaying that "Update Mathlib" command for project that do not depend on Mathlib?

That would be better. Finding a general abstraction that works outside of Mathlib as well would be even better. I was just pointing out the minimum I expect.

[Mac Malone]

@Patrick Massot I would expect vim or emacs users to be better able to interpret CLI errors and run multiple commands (since they are both terminal-based editors) whereas I would not necessarily expect the same from VSCode users (since it is more UI-focused).

[Arthur Paulino]

I might have said something along these lines before, but let me try to elaborate a bit more.

One thing that worries me about Lake development is that Mathlib seems to make some Lake development decisions hard to conciliate. I agree with what's been said above about Lake doing too much.

My read is that if Lean 4 is meant to go beyond mathematics and become a programming language that really stands out, Lake will need to detach from Mathlib needs that are too specific and run free to become the most amazing package manager / build tool it can be.

For example, I find it a bit weird that there exists lake new foo math because it feels inverted to me. I believe Mathlib can evolve to acquire its own wrapper tools around Lake. Similar to mathlibtools, but written in a language that people can just download a binary instead of having to setup Python (is Lean 4 a good choice?).

I also think that Mathlib can have its own VS Code extension, full of buttons to run terminal commands in the background so users don't need to reach for the terminal. These buttons can do a bunch of stuff, from calling Lake to performing Git operations.

If Lake and Mathlib embrace self-contained roles, I think it empowers both fronts to develop to their full potential, with much less tied decisions.

[Mac Malone]

@Arthur Paulino While I largely agree, there is some difficulties in doing this at the moment. Versioning tools heavily reliant on the Lean toolchain outside of it can be difficult . Namely, distribution is a major problem (how do users get the right version of mathlibtools for their project?). Thus, I think enabling this fully will require something like a lake install to add packages like mathlibtools to the toolchain.

[Arthur Paulino]

Distributing/versioning mathlibtools would become a self-contained responsibility of Mathlib maintainers. They would be free to go with it while barely having to request or wait for changes on Lake. That's the idea

[Shreyas Srinivas]

I think separating mathlib dep management from lake is a bad idea in that,

1. you would have to build these tools from scratch
2. They would largely repeat lake's functionality
3. Lean users who also work with mathlibtools would have to deal with two potentially incompatible CLI tools. Imagine working simultaneously with yarn and npm
4. Many problems that math users currently face fall into two categories:
   a) versioning: all lean projects need this anyway.
   b) UX problems: which can be dealt with by the extension.

[Shreyas Srinivas]

We need lake to be a full fledged depedency manager like cargo or cabal. Adding too many math specific hacks increases maintenance work, adds redundancy, and distracts from the main goal. Once lake is a proper dependency manager, mathlib should be able to work with it like any other dependency. Additional mathlib specific tooling built on top of it will then be consistent with lake.

[Shreyas Srinivas]

The most recurrent problems currently facing math users are the complications they face when using lake update or lake cache. This can be alleviated by offering mathlib specific GUI options that @Marc Huisinga is proposing. It also makes lean convenient for those who find CLIs inconvenient.

[Mac Malone]

Shreyas Srinivas said:

Additional mathlib specific tooling built on top of it will then be consistent with lake.

This was what I understood @Arthur Paulino's suggestion to be.

[Shreyas Srinivas]

Ah okay. I got the impression that it would be more akin to lean project. Independent and specific to math

[Shreyas Srinivas]

Arthur Paulino said:

Distributing/versioning mathlibtools would become a self-contained responsibility of Mathlib maintainers. They would be free to go with it while barely having to request or wait for changes on Lake. That's the idea

Based on this

[Shreyas Srinivas]

Also, where non-UX lake features are concerned, most libraries would be happy to have quite a few the features mathlib wants. So it makes sense that they be implemented in lake in a general way

[Julian Berman]

Also remember some people use other editors. Of course we could say that people who insist to use vim or emacs don't need any interface, but they still need a usable cli.

Tangentially speaking at least for nvim, if there are things VSCode adds that are helpful workflow-wise for anyone not as willing to spend time in the CLI I still will probably try to copy them as long as they're not intrusive, such that hopefully there's at least a kind of parallel for things you'll find in VSCode (e.g. the Refresh File Dependencies thing we of course added to match VSCode, probably a bunch of other things I'm forgetting).