Lean4: Workspace not trusted in VS Code

Stream: new members

[Andrew Wheen]

I’ve had a lot of problems trying to install Lean 4 on my Windows 10 laptop using the instructions at https://leanprover.github.io/lean4/doc/quickstart.html . Everything went fine until I clicked the “Install Lean using Elan” button in VS Code. At this point, my Norton 360 security software announced that Elan was behaving dangerously and the installation had been stopped. It gave me the option of completing the installation (which I accepted) but when I tried to run Lean in VS Code the server kept stopping.
Long story short: I finally managed to complete the installation, and I was able to get responses in VS Code to inputs such as #eval Lean.versionString, but anything more complicated than that just produced error responses, and the Lean server kept stopping. Now I cannot find any way to wake it up: VS Code just sits there and says “Waiting for Lean server to start”.
The Troubleshooting section at the end of the installation instructions says that if this happens, I should try two things:
(1) Check that the VS Code Terminal is not showing some installation errors from elan. (The terminal is reporting that “No problems have been detected in this workspace”.)
(2) If that doesn't work, try also running the VS Code command Developer: Reload Window. (This produces a response that “the term ‘Developer’ is not recognised”.)
When I look in the VS Code Settings for the Lean4 Extension I find “This extension has been disabled because the current workspace is not trusted”.
I’m out of ideas. Can anyone help?

[Mario Carneiro]

the issue with (2) sounds like you did not input the command in the right place. If you type ctrl-shift-p you should get a popup menu with a bunch of different actions and a search bar at the top; if you type "Developer: Reload Window" or fragments thereof the command with this name should be selected, and enter triggers it

[Mario Carneiro]

The issue with "the current workspace is not trusted" suggests that you are using vscode in "restricted mode"; there is a dialog that pops up when you open a folder asking if you trust the contents of the folder and if you do not select "yes" lean cannot run. When you are in restricted mode, there is a banner across the top that says as much, and a "Manage" button that takes you to a page where you can elect to trust the folder you have opened. (This is because lean code can run arbitrary commands on your computer, so you should not open untrusted lean code, but no one has ever attempted to distribute lean malware to my knowledge.)

[Mario Carneiro]

The terminal is reporting that “No problems have been detected in this workspace”.

That does not sound like the terminal, that sounds like the problems view. There are a bunch of windows in that bottom section, one of them is marked "Terminal", it may be indicated with an icon that looks like a > in a box.

[Andrew Wheen]

Many thanks for your quick response. I have now run Developer: Reload Window using ctrl-shift-p. Yes, VS Code had gone into Restricted Mode, so I've fixed that and the Lean4 extension is now saying that it is enabled globally. You were right - the message was from Problem View. However, despite those changes, VS Code is still reporting that it is waiting for the Lean server to start.

[Andrew Wheen]

I want to try a complete re-installation of Lean 4, but in order to do this I need to uninstall all the components that I have installed up to now. Is there a script that I can run to get rid of anything that will cause a new installation to fail?

[Kevin Buzzard]

Uninstalling and reinstalling is unlikely to help. My conjecture: you are just playing around with a random Lean file on your computer rather than a Lean file which is sitting within a correctly configured Lean 4 project. Have you got a Lean 4 project installed? For example you could install std4 and then make a Lean file within that project and see if things work there.

[Andrew Wheen]

Following re-installation, Lean now appears to be stable but it still seems unable to find MathLib. PATH includes pointers to elan, Python and VS Code executables - does it need anything else? In response to your question, I believe that I am working with a Lean file that is sitting in a correctly-configured Lean 4 project but how would I prove this?

[Matt Diamond]

Do you have the project open in VS Code or just the file open?

[Andrew Wheen]

Is a "project" the same thing as a VS Code Workspace? If so, the answer is no.

[Alex J. Best]

You should open a folder in vscode rather than a file. And that folder should contain a lean-toolchain file. If the folder contains a lakefile.lean as well you should run lake build in the folder first to check it is set up properly

[Srikrishna Sampath Kumaran]

Hi I am trying to download python for lean. I tried to install python 3.11.0. While opening the exe file to install python it showed me the option "Add python.exe to the PATH" and I installed after which I typed the command "which python" on git bash which did not show the correct directory format as expected. Instead I already have python 3.10 in my system. So what should I do to proceed further

[Kevin Buzzard]

This is a thread about workspaces not working in Lean 4. If you're asking about Lean 3 and python problems you should start a new thread in this stream with an appropriate title.

[Andrew Wheen]

Yes, the folder did contain a lean-toolchain file and lakefile.lean. The folder is now configured as a VS Code Workspace, and I created a new Lean Test file within that workspace, but Lean4 still seems to be struggling to find MathLib. I ran lake build in the VS Code Terminal and it just thought for a moment before issuing another command prompt. Is this is another example of Lean's understated way of declaring success?

[Andrew Wheen]

How are projects supposed to be set up in Lean 4? The documentation for the leanproject python program that is used for setting up projects in Lean 3 states that leanproject is not applicable for Lean 4. This suggests that the Lean Project documentation on the Lean Community website is not applicable either. The only project documentation that I can find that is clearly for Lean 4 is this: https://limperg.de/posts/2021-05-31-lean4-project.html and it looks both unofficial and out of date.

[Kevin Buzzard]

Yes unfortunately now we are in a transitional period. As a general rule the stuff on the leanprover-community website is 99.9% likely to be Lean 3 specific, and the stuff on Microsoft's website is 99.9% likely to be Lean 4 specific. Obviously there are many similarities, but when it comes to plumbing like this the two worlds are very different. I would search the MS Lean pages for answers to questions like this (I would tell you but I don't have a clue, I have only ever cloned Lean 4 projects rather than made my own, but I would imagine that the process you're looking for will be on the MS pages leanprover.github.io)

[Kevin Buzzard]

yeah https://leanprover.github.io/lean4/doc/quickstart.html#create-a-lean-project it's there (assuming you've done all the stuff above it)

[Andrew Wheen]

Yes, those were the instructions that I followed. The initial installation was screwed up by over-enthusiastic Norton 360 security software, but I re-installed everything from the beginning and it should be clean now. Quickstart just tells you to run "lake init foo" and "lake build" - both of which appear to execute correctly. However, it is clear from the infoview screen on the right that there is still something missing.

[Andrew Wheen]

6Nov22: I have definitely created a Lean4 Project / Package: “lake init foo” and “lake build” ran properly, the correct set of files appeared (as listed at https://leanprover.github.io/lean4/doc/setup.html ) and lake init confirmed that the package was installed. The Lean server is clearly running because the VS Code InfoView window shows correct responses to #eval commands. However, when I try to enter a simple theorem that has run correctly on the Lean Web Editor, I get responses such as “unknown identifier“ and “No info found”. I appreciate that there are differences between Lean3 and Lean4, but the server is clearly struggling for some reason. It even fails to print “Hello” when running the main.lean file that came with the package. Any suggestions would be most welcome!

[Alex J. Best]

What is the theorem that gives you errors

[Ruben Van de Velde]

And which lean web editor?

[Andrew Wheen]

The Lean Web Editor that I'm using is the one at https://leanprover-community.github.io/lean-web-editor/ . Is there a better one somewhere?
One theorem that gave me errors on Lean 4 running on VS Code was pow_pow from the Natural Number Game, Power World, Level 7 (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=4&level=7). I was able to get this to run on the web editor, although some changes were required from the solution that worked in the Natural Number Game. I then tried a simpler theorem (succ_eq_add_one from Level 5 of Addition World) and again there is a problem on VS Code's InfoView. In both cases, it provides almost no feedback except comments such as "No info found" or " 'begin' is an unknown operator". Although it doesn't object when I type in the goal, it doesn't recognise what it is. Does that help?

[Ruben Van de Velde]

Yeah, that's the lean 3 web editor, you really shouldn't expect lean 3 code to just work. If you paste what you tried, someone (who isn't me) will probably be able to help

[Andrew Wheen]

I really dont think that it's a Lean3 / Lean4 compatibility problem. I've just taken some Lean4 code that was published alongside the The Lean 4 Theorem Prover and Programming Language (System Description) document - so it should be correct! When I put it into VS Code, the colours suggest that the code is being correctly parsed but InfoView just says "No info found". It doesn't change when I move the cursor around, or even when I introduce errors into the code.

[Kevin Buzzard]

Lean 4 code will not work in the lean 3 web editor. The syntax is sufficiently different. Think of them as different languages.

[Andrew Wheen]

Yes, I would not expect Lean4 code to run in the web editor, but I would expect it to run in VS Code that has been configured to run Lean4. That is the problem!

[Eric Wieser]

Can you paste the exact code you're trying to run in Lean4 here?

[Andrew Wheen]

It's here: https://github.com/leanprover/lean4/blob/cade2021/doc/BoolExpr.lean

[Kevin Buzzard]

That code is from 2021 and Lean 4 is a dynamic moving target right now. It's unlikely that code written in 2021 will still compile with the latest nightly.

[Andrew Wheen]

I don't mind it throwing up some errors. (In fact, I confidently expect some errors.) But VS Code just sits there saying "No info found". It's not a coding problem, but every part of the installation seems to be set up correctly.

[Alex J. Best]

Well you said before that you got errors like "begin' is an unknown operator", which is precisely what lean 4 would say when given lean 3 code. So it sounds like it is definitely doing something nontrivial

[Alex J. Best]

And to be clear what happens if you add the line #eval main in the Main.lean file

[Andrew Wheen]

Apologies. I've just found some Lean4 code that seems to run properly in VS Code, so it looks like the implementation is ok after all. I recently read the document called "Significant changes from Lean 3" and got the impression that the changes would have relatively little impact on theorem proving, but it now appears that I was wrong. I've got some learning to do!

[Andrew Wheen]

PS - Many, many thanks to everyone who contributed to this thread. Your comments have been really helpful.