simplest way to create a vscode folder of lean files?

Stream: new members

[rzeta0]

I'd like to create a folder of lean example files, which will eventually become a set of tutorial examples.

The example code I previously downloaded, The Mechanics of Proof, has several other things (html folder, lake-manifest.json, lakefle.lean, lean-toolchain, scripts folder, Library folder, etc etc) which to me seem unnecessary for a minimal setup.

The official guide inside VSCode talks about two options for setting up a Lean project folder - one for general programming, and one for doing maths with maths lib. Even this latter option creates a folder with several files (.git folder, lake-manifest.json, makefile.lean, lean-toolchain...).

My question is this: what is the absolute minimum structure for a folder of related simple example lean files?

I was hoping that using the .lean file extension and an import Mathlib.Tactic would be sufficient for VSCode to run the file.

I have searched the web, but can't find an answer to my question.

I am pretty sure i don't want "Lake" which seems to be something the automatically compiles executables.

---

Update: Minimal setup here also means that if someone takes a copy of the folder (eg from GitHub) they can run the files as intended.

Comment: I notice that entering code examples into http://live.lean-lang.org doesn't require me to set up manifests or json or other files. It just works.

[Chris Bailey]

If you just have a <name>.lean file you can still work with it in vscode as long as the machine has vscode and a compatible versin of Lean installed, so I guess that's the bare minimum.

That being said, I don't think you actually want a "minimal setup". If you want other people to be able to use your work, you want to include a lean-toolchain file to ensure that your users are using the right version of Lean to run your code. If you want mathlib, then you need a lakefile because you're now importing an external dependency; Lean needs to know what version of mathlib you want, and where to get it.

[rzeta0]

Thanks Chris - can I ask, of lean-toolchain tells vscode which version of lean to get, why can't it also tell which version of mathlib to get?

To a beginner like me it seems overkill to have two files. A single dependencies.txt file (or other name) would seem simple enough. Is the reason historical?

[rzeta0]

also I'm guess the live.lean-lang.org just uses a standard set of dependencies eg latest lean and the most common libraries like mathlib ?

[rzeta0]

am i correct in assuming that:

• lean-toolchain is a file for vscode, telling it how to set up a lean runtime
• lake file is for lean, telling lean how to import dependencies

[llllvvuu]

lean-toolchain is for elan, which is Lean's version of nvm/pyenv/rustup/etc. the VSCode extension might use elan, i'm not sure.

[Chris Bailey]

The lakefile is for lake which is Lean's package/build manager. It contains dependency information and also information about your own lean project.

I think you're right that the live editor just does a bunch of magic behind the scenes, that's pretty common since the developers of those live environments only want to expose a safe-ish sandbox for people to use.

I don't know the developers' actual reasons for using two files, aside from lake/elan being different tools. For vcs, ci, anything automated, it makes swapping out or updating the toolchain easier.

[Jon Eugster]

@rzeta0 in the webeditor you can enter something like

import Webeditor
#package_versions

to see which packages and which versions are used. The instructions for that workaround are in the dropdown menu under "Tools". Also, in the preferences, you can select different projects to run, such as "stable lean", "nightly lean", or "lean with mathlib".

Behind the scenes all these "projects" are basically folders of the same steucture as you would get from lake new myProject lib. And this should probably also be your "minimal setup" to distribute Lean tutorials in a compatible way.

And to elaborate on the 2-3 files, I believe the main reason to have a separate toolchain file and a lakefile.lean is that the latter config file is actually parsed using Lean, and therefore the toolchain must be known prior. (New projects will have optionally a lakefile.toml instead, but still having the option to use such a powerful config file can be very useful)