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
Patrick Massot (Nov 24 2019 at 16:39):
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:
- download https://github.com/leanprover/lean/releases/tag/v3.4.2 wherever you want, and make sure the
binfolder gets added to PATH.
- download a
.leanfolder from mathlib-nightly
- download VScode+extension
- starts creating random Lean files.
Last updated: May 15 2021 at 02:11 UTC