VScode warning

Stream: general

[Patrick Massot]

Do you think the VScode extension could issue a warning if asked to work outside of a folder containing a leanpkg.path?

Gabriel has implemented this feature in the latest release! :tada:

Amazing, thanks @Gabriel Ebner! Maybe the message is a bit too strong. In principle people could still want to work on a lonely Lean file using only core (or using mathlib installed inside HOME/.lean). The new message could tell it's unlikely to be good.

[Patrick Massot]

I'm writing that because, in the last couple of months, I noticed several users who would like a softer introduction to Lean, without creating a Lean project. I used to believe that assuming a sane python environment (or a sane way to create one) was a not a big requirement. But experience proves I'm wrong. There are too many users of user-hostile operating systems like Windows or MacOS. Maybe we should also be documenting a lighter way to get started, that only involves getting a precompiled Lean + one precompiled mathlib inside ~/.lean.

[Patrick Massot]

Arg, leanpkg install https://github.com/leanprover-community/mathlib immediately tries to compile instead of letting people download oleans.

[Patrick Massot]

Maybe we should have mathlib-nightly offering a .lean folder to download. This way we could tell people: if do not want to use Lean seriously you can:

• download https://github.com/leanprover/lean/releases/tag/v3.4.2 wherever you want, and make sure the bin folder gets added to PATH.
• download a .lean folder from mathlib-nightly
• download VScode+extension
• starts creating random Lean files.