How to install Lean 3.4.2 with VSCode on the Windows ?

Stream: new members

[YurySerdyuk]

I have a need to work with Lean version 3.4.2 on the Windows.
I have directories bin, include, lib on my machine.
How to connect VSCode with these files ?

[YurySerdyuk]

I have a need to work with Lean version 3.4.2 on the Windows.
I have directories bin, include, lib on my machine.
How to connect VSCode with these files ?

[Anne Baanen]

If you installed Lean the official way, then whenever you open a Lean project VS Code will automatically start the right Lean version.

[Anne Baanen]

Do you already have a project that you need this version for, or do you want to make a new project?

[YurySerdyuk]

I would like to create new project.
As I see, I need to install some extension for that.
The extension manager propose to me as extensions
-- Lean 3 language support v.0.16.58
-- Lean4 language support v.0.0.103
Should I install an extension for Lean 3 and
what to do next ?

[Ruben Van de Velde]

For a new project, you definitely should not use 3.4.2, that's very old. Depending on what mathematics you want to do, you might use a recent version of lean 3 or 4

[Jireh Loreaux]

If you are starting a new project of any sort, I strongly encourage you to use Lean 4.

[YurySerdyuk]

I would like to reproduce the proofs from the work https://matryoshka-project.github.io/pubs/dermitzakis_bsc_thesis.pdf,
https://github.com/MarkosDe/bb_alg/blob/master/src/bb_alg.lean
This work was performed under Lean 3.4.2. The main advantage, as I understood, is that, for example,
finsupp structure is computable, whereas in the current version finsupp is an uncomputable structure
(https://leanprover-community.github.io/mathlib_docs/data/finsupp/basic.html).

[Alex J. Best]

If you have elan and leanproject installed properly then this should be as simple as running leanproject get https://github.com/MarkosDe/bb_alg.git in your home directory actually I am not sure of this, maybe elan also no longer supports 3.4.2 out of the box, at least this didnt work for me, perhaps as the version used by this project is not even 3.4.2 but some random nightly from a few years ago

[Alex J. Best]

Then when opening the project in vscode you should install the lean 3 extension, but it may be the case that some things have moved on from 3.4.2, but the only way to know is to try it out

[Alex J. Best]

I did in the end get this project to work, by changing the leanpkg.toml file to say lean_version = "3.4.1"

[YurySerdyuk]

Can you write down the steps which I must carry out after running VSCode ?
How to
1) point out the location of Lean 3.4.2 bin, include, lib files,
2) to load file with the source code,
3) find the location of leanpkg.toml file
and so on.

[Alex J. Best]

Usually it is best to install elan, which manages those files for you. See https://github.com/leanprover/elan

[Alex J. Best]

Then you can git clone https://github.com/MarkosDe/bb_alg.git, modify the leanpkg.toml file as above, and than navigate to the directory you cloned and run leanpkg build

[Alex J. Best]

To be honest though I'm not sure it will be worth the effort

[Alex J. Best]

Most of what you will learn from the code you can surely learn by reading the report you linked

[Kevin Buzzard]

Note also this thread which talks about Buchberger in Lean 4. The finsupp structure in 2019 mathlib was computable in a theoretical sense but not in any practical sense so I'm not sure you could ever hope to actually do any Groebner basis calculation in Lean 3 which would not be trivial to do by hand. Lean 3 is a programming language which in three weeks' time will be abandoned by pretty much everyone.