Zulip Chat Archive

Hello. I've successfully installed Lean. I used instruction from Lean Community's web-page. So I installed Git, Git Bash, Python, Extension for VS Code and so on. But I have two questions:
Question 1: It's about deleting Git, Git Bash and Python after installing. I don't use Git , I don't use Python as programming language. I don't understand one step after installing extension in VS Code: On Command Palette you need type Select Default Profile and choose Git Bash. I won't do this yet, but Lean works, I've tried some code. What does it mean and if it's not necessary to choose Git Bash can I delete it? Can I delete Python or works of Lean depends on Python?
Question 2: For example, I want to install Lean on computer without an access to Internet. I can copy VS Code, extension for Lean, Python (if it need) from USB-disk on that computer. But how to install Lean Prover itself? What files I need?

Johan Commelin (Oct 01 2022 at 14:09):

@Damir Gabitov It is very hard to use Lean effectively without Python. Using it without git might be possible, but I strongly advice against it.

Johan Commelin (Oct 01 2022 at 14:10):

If you want to do things the non-standard way, be sure to read https://leanprover-community.github.io/toolchain.html

Kevin Buzzard (Oct 01 2022 at 14:12):

It all depends on what you want to do. If you ever want to make a new project, it is immediate with python and extremely inconvenient without. If you ever want to put a project online it is easy with git and inconvenient without. If you want to download a project from the internet then it is easy with git and python and extremely inconvenient without.

Damir Gabitov (Oct 01 2022 at 14:21):

So, than it's better for me not delete Python and Git, although I've installed Lean for learning proving on it, and I won't be use it for creating online projects, and I think I won't be use Git . Installation of Lean takes a lot of commands. Is it possible to create .exe file for installing Lean itself? For example, if I'm going to install in on computer without Internet?

Damir Gabitov (Oct 01 2022 at 14:23):

Oh, sorry, I find it on GitHub , I use your link https://leanprover-community.github.io/toolchain.html. Thank you. So, I need compile that file?

Patrick Massot (Oct 01 2022 at 14:24):

Damir, did you see the "Maybe a couple of nights" section at https://leanprover-community.github.io/get_started.html#maybe-a-couple-of-nights? It's exactly meant for people who want to run Lean on their computer but don't (yet?) intend to do anything serious using it.

Patrick Massot (Oct 01 2022 at 14:24):

There you'll find a zip file containing everything in a single folder with no installation requirement, and a tutorial to play with.

Damir Gabitov (Oct 01 2022 at 14:25):

Yes, I tried it. But it didn't work on my computer. Is it for Windows 7 too?

Patrick Massot (Oct 01 2022 at 14:26):

I have no idea about what's happening under Windows. It's very difficult to offer support for user-hostile operating systems.

Patrick Massot (Oct 01 2022 at 14:28):

Oh wow, Windows 7 is from 2009. I guess the answer is it's unsupported, sorry.

Damir Gabitov (Oct 01 2022 at 14:29):

Ok, I will try files from GitHub . At this moment Lean works on VS Code on my computer. Can you explain what this files on GitHub: lean-...-darwin.zip, lean-...-windows.zip.? I saw darwin on Coq system too. (As I understand SourceCode.zip is need compilation on C compiler)

Patrick Massot (Oct 01 2022 at 14:41):

Darwin means Apple, you don't want this on your computer.

Damir Gabitov (Oct 01 2022 at 14:56):

Ok. Thank you

sho (Oct 24 2022 at 11:28):

Hey all, I am a undergrad student trying to learn Lean. I am not sure how to install Lean on Debian tho. Should I go for elan package, the lean4 binaries on the website or should I get the lean4 extension on vscode ?

sho (Oct 24 2022 at 11:29):

I tried installing through elan and also installed the lean4 plugin on vscode

Kevin Buzzard (Oct 24 2022 at 11:29):

Are you more mathematically or computer-science inclined? For maths you should install Lean 3 following the instructions on the leanprover-community website. For CS you should install Lean 4 following instructions on Microsoft's website.

sho (Oct 24 2022 at 11:31):

I am more cs inclined. Thanks

Kevin Buzzard (Oct 24 2022 at 11:32):

Then go with elan, VS Code and the Lean 4 extension. And also create or download a project to hack on Lean (using the nightly versions which are much more up to date), don't just edit a random lean file and expect things to work out of the box. Lean works much better in a project.

Kevin Buzzard (Oct 24 2022 at 11:33):

elan will do all of the lean downloading for you.

Mauricio Collares (Oct 24 2022 at 11:58):

For using Lean 4, install elan using the instructions from https://github.com/leanprover/elan (it's just curl ... | sh and it performs a user installation), as the elan Debian package is currently incompatible with Lean 4 (apt remove it first if you've already installed it).