Install using elan missing

Stream: lean4

[Horatiu Cheval]

Someone who is trying to install Lean 4 on a Windows machine machine I don't have access to right now, following to quickstart guide, claims that the "Install Lean using Elan" popup doesn't appear. Is this something known, or do you think it is the case that they are probably doing something wrong?

[Horatiu Cheval]

Sorry, nevermind, it seems they did't create a new .lean file, and the popup didn't simply appear on select language

[sfkjnsfjkls]

Screenshot-2023-02-19-at-19.21.41.png
getting this error on M1 for installing lean4

[Kevin Buzzard]

The relevant part of the screenshot is missing. Did you open the root directory of a correctly formatted lean project using VS Code's "open folder" functionality?