Weird issue creating a new project

Stream: new members

[Ruth Plümer]

Hello, I have been working with Lean for quite some time now, but I have never set up a project myself.
Today, I tried setting up a new project by myself on my Linux laptop for the first time. Basically, I followed the instructions under https://leanprover-community.github.io/install/project.html#creating-a-lean-project and created a new project called

my_project

under the path

path/PROJECT/my_project

Everything seemed to have worked fine, after following the instructions, the folder under

path/PROJECT/my_project

contained a lakefile.lean, a lean-toolchain, a .git-subfolder, a .gitignore-file, a project.lean and a subfolder

path/PROJECT/my_project/My_Project

containing a Basic.lean file. The problem was when I tried to open the my_project folder in VS-Code, I couldn't work at the Basic.lean-file. I got syntax-highlighting, but I couldn't toggle an infoview, the key shortcut didn't work and the \forall-sign in the upper left corner only showed options like "Open Project..." and "Search with Loogle", but not "Toggle infoview" like it usually does. Also, the file didn't get executed.

When opening VS-code, it showed me the following infobox:

 Lean-version 'leanprover/lean4:v4.23.0-rc2' of Lean project 'path/PROJECT/my_project/My_Project' is not installed. Do you wish to install it?

But when I clicked 'yes' the download never finished / got aborted. What I find weird is that under

path/mathematics_in_lean

I have stored the Mathematics in Lean project, which I can open, execute and work on in VScode as usual.

Does anyone have an idea what I've been doing wrong? Any help is appreciated!

[Weiyi Wang]

I am not sure what exactly went wrong, but does the problem persist if you uses vscode lean extension's wizard (Lean icon -> New project...) to create a project?

[Kevin Buzzard]

@Ruth Plümer those are legacy (ie out of date) instructions. Please delete everything and then follow the official instructions at the top of the web page which you posted above.

[Ruben Van de Velde]

Do you mean the "The recommended way to create..." sentence? Then we should bold that or something, because it currently doesn't stand out at all

[Kevin Buzzard]

Sorry, deleted "linked to". I think we should delete those old instructions, but IIRC others argued that they should stay.

[Marc Huisinga]

It sounds like the Lean extension is refusing to activate in this project because the right Lean version failed to install - there is likely an error in a popup in the bottom right in VS Code that has a "Retry" button that you can use to re-run the installation. You've probably already installed the Lean version of mathematics_in_lean, which is why the issue doesn't occur there.

If re-trying to install leanprover/lean4:v4.23.0-rc2 from the VS Code extension doesn't work, could you try running lean +leanprover/lean4:v4.23.0-rc2 --version from a terminal and paste the output?

[Paul Schwahn]

Kevin Buzzard said:

I think we should delete those old instructions, but IIRC others argued that they should stay.

At least the instructions on how to update mathlib in a project are still very useful to me. Is there an updated version for them as well?