Waiting for Lean server to start confusing message #323
Comments
|
Another instance of this with a different cause can be found on the Lean Zulip. |
|
@PatrickMassot This specific example now reports the following notification as of #334: "Opened folder is not a valid Lean 4 project. Please open a valid Lean 4 project containing a 'lean-toolchain' file for full functionality." Do you think that this sufficiently solves this issue? For the example from the Lean Zulip, I have other plans to make the detection of outdated and broken setups better. |
|
I now see an error message but not the one you quote. And the one I see does not really give instructions on how to improve things. |
|
You have no default toolchain set, correct?
Can you click the notification bell at the bottom right? When there are too many notifications, VS Code likes to hide them there. |
|
@PatrickMassot With the same setup as before you should now see two notifications with #347 and 0.0.118: One informing you that you lack a default toolchain, and one informing you that you should open a folder. |
|
Indeed, this what I see. This is an improvement, but still not maximally helpful. It states what is wrong but gives only a little bit of help about what to do next. The message about not being in a project could contain a button proposing to open the Setup guide. The message about not having a Lean toolchain contains no explanation or pointer to explanation about what the user should do. Do we want a button the sets up a default toolchain? A button proposing to open the Setup guide? |
|
The default toolchain error should be pretty rare because it only occurs if the user both fiddled with In the future, we want better diagnostics for broken setups in general (old versions, missing dependencies, broken lean installations, etc.) and a VS Code frontend for elan.
This is a good suggestion for all errors that new users are likely to face in general. I'll keep it in mind. |
|
Ok feel free to close the issue if you are happy with the current state (which is already very good indeed!). |
This PR has three main goals: 1. Implement a new and easily extensible mechanism to detect issues with the user's setup and notify them about it. 2. Implement an easily extensible mechanism to dump all kinds of context information about the user's system and Lean setup to make it easier to debug issues with their setup. 3. Clean up all of the existing code to the extent that is necessary in order to facilitate 1. and 2.. ### Setup diagnostic warnings and errors There are two separate kinds of setup diagnostics: Global- and project-level diagnostics. * Global-level diagnostics are checked when the first Lean file is opened. If there is an error-level setup issue, none of the Lean-specific extension features are activated. The following global-level aspects of the user's setup are checked: 1. Whether Curl and Git are installed (Error; reference to setup guide) 2. Whether some version of Lean can be found (Error; Elan installation offered) 3. Whether Elan is installed and reasonably up-to-date (Warning; Elan installation / Elan update offered) * Project-level diagnostics are checked whenever the first Lean file of a project is opened. If there is an error-level setup issue, the language client will not launch, but all of the other Lean-specific extension features will be active, provided that the global-level diagnostics did not yield an error. The following project-level aspects of the user's setup are checked: 1. Whether the language client is running in an Untitled file without an attached Lean 4 project (Warning; reference to setup guide) 2. Whether a lean-toolchain file can be found in the project associated with the file (Warning; reference to setup guide & option to open parent directory with lean-toolchain offered if present) 3. Whether some version of Lean can be found (Error) 4. Whether the project associated with the file is a Lean 3 project (Error) 5. Whether the project associated with the file is using a Lean version from before the first Lean 4 stable release (Warning) 6. Whether some version of Lake can be found (Error) If someone is willingly using a "weird" setup that triggers warning-level diagnostics, the corresponding notifications can be turned off using the `lean4.showSetupWarnings` configuration option. ### Setup diagnostic dump In the forall menu, a new command "Troubleshooting: Show Setup Information" has been added that can be used to gather information about the user's system and their Lean setup. It includes the following information: 1. Operating system 2. CPU architecture 3. CPU model 4. Total available RAM 5. Whether Curl is installed 7. Whether Git is installed 8. Whether Elan is installed and reasonably up-to-date, as well as the Elan version 9. Whether Lean is installed and reasonably up-to-date, as well as the Lean version 10. Whether a Lean project with a lean-toolchain has been opened, as well as the path to the project 11. Available Elan toolchains <img src="https://github.com/leanprover/vscode-lean4/assets/10852073/1eb65d9f-16b7-4516-a00a-48014c069c49" width="80%" /> <img src="https://github.com/leanprover/vscode-lean4/assets/10852073/7e93ff71-73d9-4fd5-92d3-cd74bef729b2" width="80%" /> ### Clean-up of user-facing legacy features - Several settings to modify the commands that are launched in specific situations have been removed (lean4.toolchainPath, lean4.lakePath, lean4.enableLake, lean4.serverEnv, lean4.serverEnvPaths) and replaced with a single setting lean4.envPathExtensions that can be used to augment the PATH variable of the VS Code extension process and all of its child processes. - Compatibility with Lean versions that did not support `lake serve` has been removed. - The exports of the extension have been cleaned up to reflect the two-stage activation of the extension (first, non-Lean specific features are activated when VS Code is launched, second, Lean-specific features are activated when a Lean file is opened). - When opening a project and installing Elan for the first time, the extension would install the given project toolchain as the default Elan toolchain and then use that toolchain for the project as well. This saves some bandwidth and is a bit quicker, but comes at the disadvantage that users will have a project-specific toolchain installed as their global default toolchain, potentially leading to unintuitive behavior down the road (e.g. when creating new projects). Now, we instead install two toolchains in this scenario: leanprover/lean4:stable as the default toolchain, and the project-specific toolchain for that project. In the future, when leanprover/elan#106 lands, this should lead to much more intuitive behavior outside of projects. ### Refactorings - Much of the old bootstrapping and Lean version check logic has been rewritten and entirely replaced with the new setup diagnostic system. Most importantly, the Lean installation bootstrapping deep in `LeanClientProvider` has been lifted out to the outer global-level setup diagnostics and the `LeanClientProvider` is now much simpler than it used to be. - The version cache in `LeanClientProvider` has been deleted. Calling `lean --version` (rarely) a second time when that specific Lean toolchain has already been installed by a previous call should be sufficiently cheap that no cache should be needed. - `config.ts` has been cleaned up. - The tests for setups without Elan have been removed as they only worked due to special test-specific behavior in the first place. I'd like to re-add better tests for this at some point in the future. - The pre-bootstrap test has been removed because it did not properly test whether the installation prompt is open. It would be nice to have proper tests for all setup diagnostics eventually, anyways. - The Typescript version has been updated 5.4.5. - Progress bars are now only displayed after 250ms to reduce visual clutter for quick-running commands. - All calls to `window.show(Error|Warning|Information)...` have been refactored to use a safer API that ensures the following invariants to prevent the VS Code extension from being blocked on a transient notification: - Notifications without input should never block the extension - Notifications with optional input should never block the extension - Notifications that block the extension must be modal ### Affected issues Fixes #323: We now have a general mechanism to improve these kinds of setup issues. Closes #326: This setting has been removed. Fixes #388: The refactored startup logic respects overrides. Closes #400: This setting has been removed. Closes #440: This setting has been removed. I checked with @eric-wieser to make sure that the setup exhibiting this issue can be implemented without this setting as well.
When the extension completely fails to find a project, it displays "Waiting for Lean server to start" forever.
Steps to reproduce:
/tmp/not_a_project/tmp/not_a_project/test.leancontaining Lean code, say#check Nat/tmp/not_a_projectin VSCodeThe infoview opens and says "Waiting for Lean server to start..." forever. The simplest improvement would be to add a paragraph starting with "If this messages stays for more than 20 seconds then you may want to..."
The text was updated successfully, but these errors were encountered: