Lean for Windows 7

Stream: new members

[Damir Gabitov]

Hello. Can I use Lean on Windows 7 (32,64) or it only for later version of Windows (8,10 etc.)? And if I can what version of Lean: Lean 4 or maybe earlier

[Eric Rodriguez]

lean should work fine on windows 7, both versions should as far as I know

[Damir Gabitov]

Thank you. As I understood, I need install VS Code, then download Lean 4 and then use Lean in VS Code? But on main page of VS Code there is only links for downloading VS Code for Win 8,10,11. They haven't support VS Code for Windows 7 anymore? Where can I find VS Code for Win 7?

[Patrick Massot]

That's a totally different question. VSCode isn't mandatory to use Lean. It is certainly the most convenient editor, especially for beginners. But you can also use Lean with emacs or vim. In principle you could even use any text editor, but then it won't be interactive anymore, you would need to type and then compile from the command line.

[Damir Gabitov]

Yes, I have read about it. I think for me it will be better to use VS Code. I have some experience in using Coq, that have own IDE, but Lean, as I understood, doesn't have.

[Patrick Massot]

I don't think any serious user of Coq uses the specific IDE rather than emacs. But I may have a biased view of Coq users since the ones I know are the tiny minority interested in mathematics.

[Damir Gabitov]

Why other editor, for example, ecmacs, better than IDE? I didn't notice that Coq IDE doesn't have some functions)

[Patrick Massot]

Did you ever use emacs or another powerful editor such as vim?

[Damir Gabitov]

Not yet, because working with proof assistants is new for me. I started with Coq some month ago, and I want try to use Lean also. I think my experience with editors will be VS Code. I also will try use Coq in it. But at this moment I don't understand one thing: I think that IDE is complete tool, and editors are as wrapper for programming language, but also have some functions like debugging, refactoring ,etc.

[Henrik Böving]

IDEs are usually tools that specialize in working as good as possible for one programming language out of the box. Text editors (at least the ones that are somewhat widespread today like VSCode, Emacs, Vim, Neovim, Atom) tend to specialize in extensibility and configurability and in some cases also change the way you input text drastically, most notably here the vim family and plugins for other editors that emulate vim behavior. For example my Emacs is configured to work like vim when it comes to text input, has LSP things (which basically means auto completion, go to definition etc. for the majority of languages), specialized plugins for lots of languages like Lean, Coq, Python, Octave etc. And other goodies like Magit which is IMO by far the best git frontend there is even compared to all IDEs I've used so far.

So for me Emacs is just my go to tool for everything when it comes to text editing, as soon as I have an Emacs somewhere I can do all of my work just the way I want it while if I was to use IDEs I'd have to download one for Coq, one for Python, one for C ..... and in the end I would probably only use a small subset of their features anyways so I'm not even getting more features in say Pycharm than in Emacs, simply because I don't have time to learn pycharm in and out because I write in much more than one language.

[Damir Gabitov]

Yes, I agree that editors in some cases are useful. You have only one editor, and you needn't own IDE for each language. I have question about Lean: tactics of Lean are based on tactics of Coq? Many have identical names and behaviour, like "intros", "assumption" , etc. and behave

[Patrick Massot]

Using VSCode which isn't a good text editor is sometimes very frustrating when you are used to a good text editor. This has nothing to do with proof assistants, it will also apply if you write TeX code or program in any language. But VSCode basically runs in a web-browser whereas vim and emacs basically run into a terminal. This advantage really allows a much fancier display which can be really useful.

[Patrick Massot]

About tactics, there are many similarities with Coq but comparing the simplest tactics like intro and assumption is misleading. You cannot expect a one to one dictionary. You should follow Lean tutorials or textbooks. You'll find a lot at https://leanprover-community.github.io/learn.html

[Damir Gabitov]

Thank you)

[Chris Lovett]

I see some issues in github about vscode on windows 7, but you could use gitpod instead, as outlined in https://github.com/leanprover/lean4-samples.