RFC Proposal for vscode extension:

Stream: lean4

[Shreyas Srinivas]

RFC Proposal for vscode extension:
Current Behaviour
Currently the bootstrapping procedure kicks in when a lean file is opened, and if no toolchain is found, the installation of lean can be triggered. Thus the install process asks users to open a lean file to trigger installation by calling showInstallOptions. This is also what lean docs suggest
The Problem
For at least some windows users the step asking them to creating a new file creates a .txt file
by default which is not read as a lean file. Further, and more importantly, mathematical users and teachers would prefer that their students don't open individual files in the first place. They would prefer students and new users directly open a project. However, the standard way to start a new project is thoughlake new, which requires the toolchain to be installed i.e. a :chicken: and :egg: problem. Other ways could be to download/clone and open an existing project i.e. more CLI use, which is again anathema for math classes.

Possible Solution
Provide a vscode command called Check Lean Toolchain that also triggers showInstallOptions as required

[Shreyas Srinivas]

Bonus: If this command is easily accessible, it would be nice. For an example from latex workshop, see the screenshot
example_lean_suggestion.png

[Shreyas Srinivas]

If accepted, I am happy to make the github issue and implement the command at the very minimum

[Shreyas Srinivas]

I will wait for comments from the extension developers

[Julian Berman]

Maybe this isn't directly related, in which case feel free to ignore, but just on:

mathematical users and teachers would prefer that their students don't open individual files in the first place

Has someone given another recent look as to what's required to remove that limitation in VSCode? I remember I looked myself at one point and got stuck trying to figure out VSCode's APIs, but maybe it's worth another look, particularly from someone who's more familiar with them?

[Marc Huisinga]

In the next version of the extension, there will be a step-by-step walkthrough that opens as soon as you install the extension and has step with a button you can click to install Elan using a command. It also provides links to books and buttons to initialize and open projects in a way that doesn't even let you open wrong folders.
Here's a screenshot:
image.png
Is that sufficient to cover this use-case?

[Marc Huisinga]

Perhaps also worth mentioning is that the walkthrough is platform specific, so MacOS and Windows users get the right instructions.

[Kevin Buzzard]

Does "set up lean 4 project" give you a sub-question "do you want to use Lean's maths library with your project? [hint: if you want to do maths then answer "yes"]"?

[Marc Huisinga]

Julian Berman said:

Maybe this isn't directly related, in which case feel free to ignore, but just on:

mathematical users and teachers would prefer that their students don't open individual files in the first place

Has someone given another recent look as to what's required to remove that limitation in VSCode? I remember I looked myself at one point and got stuck trying to figure out VSCode's APIs, but maybe it's worth another look, particularly from someone who's more familiar with them?

I believe the main reason is that folks wanted to prevent the extension from activating and doing stuff when the file is not a Lean 4 file, as people do use VS Code for other things. You can do away with this though and the next version of the extension will provide a number of commands (e.g. installing elan, opening projects, etc.) even when no Lean 4 file is active. There's also a setting to disable this in case you find the Lean 4 menu always being shown in the top right annoying.

[Marc Huisinga]

Kevin Buzzard said:

Does "set up lean 4 project" give you a sub-question "do you want to use Lean's maths library with your project? [hint: if you want to do maths then answer "yes"]"?

image.png

[Shreyas Srinivas]

Julian Berman said:

Maybe this isn't directly related, in which case feel free to ignore, but just on:

mathematical users and teachers would prefer that their students don't open individual files in the first place

Has someone given another recent look as to what's required to remove that limitation in VSCode? I remember I looked myself at one point and got stuck trying to figure out VSCode's APIs, but maybe it's worth another look, particularly from someone who's more familiar with them?

I didn't know this was a vscode limitation. Vscode works reasonably well with individual files outside a lake project until you want to add dependencies and import other files. Then it is not clear how (and in what order) one must compile lean files to make the imports work and how to automate this in a way that is not simply reinventing lake.

[Shreyas Srinivas]

Marc Huisinga said:

In the next version of the extension, there will be a step-by-step walkthrough that opens as soon as you install the extension and has step with a button you can click to install Elan using a command. It also provides links to books and buttons to initialize and open projects in a way that doesn't even let you open wrong folders.

Will it rollback changes if I take a step back in the walkthrough to do something different?

[Marc Huisinga]

Shreyas Srinivas said:

Marc Huisinga said:

Julian Berman said:

Maybe this isn't directly related, in which case feel free to ignore, but just on:

mathematical users and teachers would prefer that their students don't open individual files in the first place

Has someone given another recent look as to what's required to remove that limitation in VSCode? I remember I looked myself at one point and got stuck trying to figure out VSCode's APIs, but maybe it's worth another look, particularly from someone who's more familiar with them?

I believe the main reason is that folks wanted to prevent the extension from activating and doing stuff when the file is not a Lean 4 file, as people do use VS Code for other things. You can do away with this though and the next version of the extension will provide a number of commands (e.g. installing elan, opening projects, etc.) even when no Lean 4 file is active. There's also a setting to disable this in case you find the Lean 4 menu always being shown in the top right annoying.

I didn't know this was a vscode limitation. Single files work reasonably well until you want to add dependencies and imports. Then it is not clear how (and in what order) one must compile lean files to make the imports work.

It's not a limitation, but common practice for language specific extensions is that they only activate for the specific language ID that they are handling (so as to not be annoying when working with other languages). Hence, since the extension used to respect this, in order to start bootstrapping you had to open an empty file and tell VS Code that the open file is a Lean 4 file so that the extension then activates.

Shreyas Srinivas said:

Marc Huisinga said:

In the next version of the extension, there will be a step-by-step walkthrough that opens as soon as you install the extension and has step with a button you can click to install Elan using a command. It also provides links to books and buttons to initialize and open projects in a way that doesn't even let you open wrong folders.

Will it rollback changes if I take a step back in the walkthrough to do something different?

You can always go back in the guide or open it again later (the checkmarks are just a visual feature at this point since VS Code disabled conditions for them a while ago). It's also not really branching. You install the dependencies, you install Elan and then you either create/open/clone a project.

[Schrodinger ZHU Yifan]

BTW, the command I used most in vscode for now is “Restart the lean language server” :grinning:

[Shreyas Srinivas]

@Marc Huisinga : Apologies, I was responding to Julian. I am aware of the way language specific extensions are activated. In fact that's what started this thread.

[Patrick Massot]

Marc Huisinga said:

Kevin Buzzard said:

Does "set up lean 4 project" give you a sub-question "do you want to use Lean's maths library with your project? [hint: if you want to do maths then answer "yes"]"?

image.png

The first item is ambiguous. What if you want to build a math library?

[Patrick Massot]

Up to now this never happened, but it could.

[Marc Huisinga]

Patrick Massot said:

Marc Huisinga said:

Kevin Buzzard said:

Does "set up lean 4 project" give you a sub-question "do you want to use Lean's maths library with your project? [hint: if you want to do maths then answer "yes"]"?

image.png

The first item is ambiguous. What if you want to build a math library?

I'm aware and I still want to simplify this a bit before pushing it out.

[Patrick Massot]

Great. Thank you very much for your work on this!

[Shreyas Srinivas]

@Patrick Massot : Are you considering a world where mathlib is not the only lean project :wink: :exploding_head: Now I have seen everything.

@Marc Huisinga : To clarify on both my points. I am responding to the aversion to use single lean files in practice. The paradox I described in the opening message is a result of exactly this.

As for rollback, here's what I mean: Suppose I create a mathlib project, and then step back to start the project creation stage to create an executable without math, will the process remove mathlib and rewrite lakefile accordingly or will mathlib remain in lake-packages.

[Marc Huisinga]

Suppose I create a mathlib project, and then step back to start the project creation stage to create an executable without math, will the process remove mathlib and rewrite lakefile accordingly or will mathlib remain in lake-packages.

No. You can create a new project without math, though.
In the distant future I'd also like to provide a GUI editor for simple lakefiles using VS Code's custom editor API, but that will still have to wait for a bit.

[Shreyas Srinivas]

I am happy to help if you need an extra hand. I do need the update on save feature asap to save my laptop, so I started fiddling with a local copy of the extension already.

[Wojciech Nawrocki]

In the distant future I'd also like to provide a GUI editor for simple lakefiles using VS Code's custom editor API, but that will still have to wait for a bit.

@Marc Huisinga what would be the intended use case of such an editor?

[Marc Huisinga]

Wojciech Nawrocki said:

In the distant future I'd also like to provide a GUI editor for simple lakefiles using VS Code's custom editor API, but that will still have to wait for a bit.

Marc Huisinga what would be the intended use case of such an editor?

It would retain the declarative nature of Lake configuration while making it easier for beginners to adjust the file without first having to learn how Lake files are structured. Most other IDEs provide GUI editors for common configuration formats, too, much like VS Code provides one for its settings.json.

[Eric Wieser]

I think the difficulty is that the lakefile is not a configuration format like json, its a script

[Scott Morrison]

I hope the vast majority of projects will have entirely declarative lakefiles. I am still suffering from the trauma of scala build files. It's no fun trying to come to grips with a new project and you can't even read the build file because it's monadic ascii soup.

[Marc Huisinga]

Eric Wieser said:

I think the difficulty is that the lakefile is not a configuration format like json, its a script

Right, but I expect most simple lakefiles (especially those that beginners are likely to encounter) to be structured regardless.

[Mario Carneiro]

it is difficult to "optimistically parse" a format like lean hoping that it is not doing anything fancy though

[Mario Carneiro]

meaning that even if they could be expressed declaratively, it is nevertheless the case that they are not

[Eric Wieser]

I think it's likely to be fairly common that beginner lakefiles copy the mathlib4 lakefile (for pp.unicode.fun, pp.proofs.withType=false, and maybe the contentious autoImplicit=false), and such lakefiles are not declarative in the usual sense.

[Eric Wieser]

I'd argue that the lake new math or whatever command should generate a lakefile pre-populated in this way.

[Wojciech Nawrocki]

@Marc Huisinga I agree that a visual editor for settings files à la VSCode's own Settings panel for settings.json could be helpful for beginners.

I also believe that keeping lakefiles procedural and then attempting to hide that complexity using a custom UI is a terrible, terrible idea. A more viable path might be to introduce a new lakefile.json (or whatever, as long as it's declarative) format and slowly migrate away from lakefile.lean files, while continuing to support that option for projects that really do need arbitrary build scriptability.

[Wojciech Nawrocki]

Eric Wieser said:

I think it's likely to be fairly common that beginner lakefiles copy the mathlib4 lakefile (for pp.unicode.fun, pp.proofs.withType=false, and maybe the contentious autoImplicit=false), and such lakefiles are not declarative in the usual sense.

The current mathlib4 lakefile can totally be phrased declaratively. It mostly just sets compiler/server options and declares some targets. Of course the price you pay for a restricted language is that constructs such as conditionals

meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

are necessarily somewhat more awkward to express (see optional dependencies in Rust's Cargo.toml) but the gain in not having to deal with crazy build scripts (see Scott's point) is significant.

[Marc Huisinga]

Just to be clear, this was a random idea from my list of unrefined ideas and I do not plan on working on it any time soon. I'm not committed to any particular way of working with simple lake configurations, either.

[Wojciech Nawrocki]

Definitely! I wanted to voice this concern in case it does came up as a more concrete plan.