## Stream: general

### Topic: VScode warning

#### Patrick Massot (Nov 24 2019 at 16:28):

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 (Nov 24 2019 at 16:31):

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 (Nov 24 2019 at 16:39):

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

#### Patrick Massot (Nov 24 2019 at 16:42):

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:

Last updated: May 15 2021 at 02:11 UTC