feat: better setup diagnostics

.vscode/launch.json

@@ -17,24 +17,6 @@
                 "webRoot": "${workspaceRoot}/vscode-lean4/media"
             }
         },
-        {
-            "name": "Extension Tests - pre-bootstrap tests",
-            "type": "extensionHost",
-            "request": "launch",
-            "runtimeExecutable": "${execPath}",
-            "args": [
-                "--extensionDevelopmentPath=${workspaceFolder}/vscode-lean4",
-                "--extensionTestsPath=${workspaceFolder}/vscode-lean4/out/test/suite/index",
-                "${workspaceFolder}/vscode-lean4/test/test-fixtures/simple"
-            ],
-            "env": {
-                "LEAN4_TEST_FOLDER": "pre-bootstrap",
-                "LEAN4_PROMPT_USER": "true"
-            },
-            "cwd": "${workspaceFolder}/vscode-lean4/out/",
-            "outFiles": ["${workspaceFolder}/vscode-lean4/out/test/suite/**/*.js"],
-            "preLaunchTask": "watchTest"
-        },
         {
             "name": "Extension Tests - bootstrap tests",
             "type": "extensionHost",
@@ -67,23 +49,6 @@
             "outFiles": ["${workspaceFolder}/vscode-lean4/out/test/suite/**/*.js"],
             "preLaunchTask": "watchTest"
         },
-        {
-            "name": "Extension Tests - adhoc with no elan",
-            "type": "extensionHost",
-            "request": "launch",
-            "runtimeExecutable": "${execPath}",
-            "args": [
-                "--extensionDevelopmentPath=${workspaceFolder}/vscode-lean4",
-                "--extensionTestsPath=${workspaceFolder}/vscode-lean4/out/test/suite/index"
-            ],
-            "env": {
-                "LEAN4_TEST_FOLDER": "simple",
-                "DISABLE_ELAN": "1"
-            },
-            "cwd": "${workspaceFolder}/vscode-lean4/out/",
-            "outFiles": ["${workspaceFolder}/vscode-lean4/out/test/suite/**/*.js"],
-            "preLaunchTask": "watchTest"
-        },
         {
             "name": "Extension Tests - infoview",
             "type": "extensionHost",

README.md

@@ -157,14 +157,6 @@ This extension contributes the following settings (for a complete list, open the
 
 ### Server settings
 
-* `lean4.toolchainPath`: specifies the location of the Lean toolchain to be used when starting the Lean language server. Most users (i.e. those using `elan`) should not ever need to change this. If you are bundling Lean and `vscode-lean` with [Portable mode VS Code](https://code.visualstudio.com/docs/editor/portable), you might find it useful to specify a relative path to Lean. This can be done by starting this setting string with `%extensionPath%`; the extension will replace this with the absolute path of the extension folder. For example, with the default directory setup in Portable mode, `%extensionPath%/../../../lean` will point to `lean` in the same folder as the VS Code executable / application.
-
-* `lean4.lakePath`: specifies the location of the Lake executable to be used when starting the Lean language server (when possible). If left unspecified, the extension defaults to the Lake executable bundled with the Lean toolchain. Most users thus do not need to use this setting. It is only really helpful if you are building a Lake executable from the source and wish to use it with this extension.
-
-* `lean4.serverEnv`: specifies any Environment variables to add to the Lean 4 language server environment.  Note that when opening a [remote folder](https://code.visualstudio.com/docs/remote/ssh) using VS Code the Lean 4 language server will be running on that remote machine.
-
-* `lean4.serverEnvPaths`: specifies any additional paths to add to the Lean 4 language server environment PATH variable.
-
 * `lean4.serverArgs`: specifies any additional arguments to pass on the `lean --server` command line.
 
 * `lean4.serverLogging.enabled`: specifies whether to do additional logging of

lean4-infoview-api/package.json

@@ -14,7 +14,7 @@
     ],
     "license": "Apache-2.0",
     "devDependencies": {
-        "typescript": "^4.9.5",
+        "typescript": "^5.4.5",
         "vscode-languageserver-protocol": "^3.17.3"
     }
 }

lean4-infoview/package.json

@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.6.1",
+    "version": "0.7.0",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -39,12 +39,12 @@
         "@types/marked": "^4.3.1",
         "@types/react": "^18.2.15",
         "@types/react-dom": "^18.2.7",
-        "current-release": "npm:@leanprover/infoview@^0.4.0",
+        "current-release": "npm:@leanprover/infoview@^0.7.0",
         "react": "^18.2.0",
         "react-dom": "^18.2.0",
         "rollup": "^3.26.2",
         "rollup-plugin-css-only": "^4.3.0",
-        "typescript": "^4.9.5"
+        "typescript": "^5.4.5"
     },
     "dependencies": {
         "@leanprover/infoview-api": "~0.4.0",

package.json

@@ -25,7 +25,7 @@
         "lint-staged": "^15.2.2",
         "prettier": "3.2.5",
         "prettier-plugin-organize-imports": "^3.2.4",
-        "typescript": "^4.9.5"
+        "typescript": "^5.4.5"
     },
     "lint-staged": {
         "*.{ts,tsx,js}": [

vscode-lean4/media/guide-help.md

@@ -1,9 +1,11 @@
 ## Collecting VS Code Output
-If you are encountering an issue with this VS Code extension, copying the output from the 'Lean: Editor' output panel can be helpful for others who are trying to help you. 
+If you are encountering an issue with Lean or this VS Code extension, copying the output from the 'Lean: Editor' output panel can be helpful for others who are trying to help you. 
 You can open the 'Lean: Editor' output panel by clicking on the ∀-symbol in the top right and selecting 'Troubleshooting: Show Output'.
 
   ![Show Output](show-output.png)
 
+Additionally, copying the information that is displayed when clicking on the ∀-symbol in the top right and selecting 'Troubleshooting: Show Setup Information' is also very helpful.
+
 ## Asking Questions on the Lean Zulip Chat
 
 To post a question on the [Lean Zulip chat](https://leanprover.zulipchat.com/), you can follow these steps:

vscode-lean4/package.json

@@ -22,12 +22,6 @@
             "type": "object",
             "title": "Lean 4",
             "properties": {
-                "lean4.toolchainPath": {
-                    "type": "string",
-                    "default": "",
-                    "markdownDescription": "**DO NOT CHANGE** unless you know what you are doing. Path to your Lean toolchain. Leave this blank to get the default location from your PATH environment or from the default elan install location.",
-                    "scope": "machine-overridable"
-                },
                 "lean4.input.enabled": {
                     "type": "boolean",
                     "default": true,
@@ -73,36 +67,14 @@
                     "default": false,
                     "markdownDescription": "Enable automatically building dependencies when opening a file. In Lean versions pre-4.2.0, dependencies are always built automatically regardless of this setting."
                 },
-                "lean4.serverEnv": {
-                    "type": "object",
-                    "default": {},
-                    "description": "Environment variables to add to the Lean 4 server environment",
-                    "additionalProperties": {
-                        "type": "string",
-                        "description": "environment variable to add"
-                    },
-                    "scope": "machine-overridable"
-                },
-                "lean4.serverEnvPaths": {
+                "lean4.envPathExtensions": {
                     "type": "array",
                     "default": [],
-                    "description": "Paths to add to the Lean 4 server environment PATH variable.",
+                    "markdownDescription": "Additional entries to add to the PATH variable of the Lean 4 VS Code extension process and any of its child processes.",
                     "items": {
                         "type": "string",
-                        "description": "a path to add to the environment"
-                    },
-                    "scope": "machine-overridable"
-                },
-                "lean4.enableLake": {
-                    "type": "boolean",
-                    "default": true,
-                    "markdownDescription": "Enable Lake server when possible."
-                },
-                "lean4.lakePath": {
-                    "type": "string",
-                    "default": "",
-                    "markdownDescription": "Path to Lake. Leave this blank to use the Lake from the toolchain.",
-                    "scope": "machine-overridable"
+                        "description": "Entry to add to the PATH variable"
+                    }
                 },
                 "lean4.serverArgs": {
                     "type": "array",
@@ -184,10 +156,10 @@
                     "default": 200,
                     "description": "Time (in milliseconds) which must pass since latest edit until elaboration begins. Lower values may make editing feel faster at the cost of higher CPU usage."
                 },
-                "lean4.showInvalidProjectWarnings": {
+                "lean4.showSetupWarnings": {
                     "type": "boolean",
                     "default": true,
-                    "markdownDescription": "Show warnings whenever a .lean-file is opened in a folder that does not contain a 'lean-toolchain' file."
+                    "markdownDescription": "Show warning notifications when the Lean setup has warning-level issues."
                 },
                 "lean4.alwaysShowTitleBarMenu": {
                     "type": "boolean",
@@ -313,6 +285,12 @@
                 "title": "Troubleshooting: Show Output",
                 "description": "Show output channel containing all progress updates and errors of commands"
             },
+            {
+                "command": "lean4.troubleshooting.showSetupInformation",
+                "category": "Lean 4",
+                "title": "Troubleshooting: Show Setup Information",
+                "description": "Show setup information for the environment that the VS Code extension is running in"
+            },
             {
                 "command": "lean4.setup.showSetupGuide",
                 "category": "Lean 4",
@@ -561,6 +539,9 @@
                 {
                     "command": "lean4.troubleshooting.showOutput"
                 },
+                {
+                    "command": "lean4.troubleshooting.showSetupInformation"
+                },
                 {
                     "command": "lean4.setup.showSetupGuide"
                 },
@@ -634,6 +615,11 @@
                     "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
                     "group": "4_troubleshooting"
                 },
+                {
+                    "command": "lean4.troubleshooting.showSetupInformation",
+                    "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
+                    "group": "4_troubleshooting"
+                },
                 {
                     "submenu": "lean4.titlebar.versions",
                     "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
@@ -902,7 +888,7 @@
         "test": "node ./out/test/suite/runTest.js"
     },
     "dependencies": {
-        "@leanprover/infoview": "~0.6.1",
+        "@leanprover/infoview": "~0.7.0",
         "@leanprover/infoview-api": "~0.4.0",
         "axios": "^1.6.7",
         "cheerio": "^1.0.0-rc.12",
@@ -928,7 +914,7 @@
         "ovsx": "^0.8.3",
         "source-map-loader": "^3.0.2",
         "ts-loader": "^9.5.1",
-        "typescript": "^4.9.5",
+        "typescript": "^5.4.5",
         "webpack": "^5.90.3",
         "webpack-cli": "^4.10.0"
     },