fix: do not suggest that installing elan also installs lean (#577)

With Elan 4.0.0, installing Elan doesn't actually install a toolchain
anymore. Only when creating or opening a project it will install a
toolchain. This PR adjusts the setup guide and the Elan installation
prompt to reflect that.

vscode-lean4/media/guide-installElan-unix.md

@@ -3,4 +3,4 @@
 
 Clicking [this link](command:lean4.setup.installElan) will download the [Elan setup script](https://github.com/leanprover/elan/blob/master/elan-init.sh) and execute it.
 
-If the script executes without displaying an error, both Elan and a current stable version of Lean 4 have been installed. If it displays an error that you do not understand, click on the 'Questions and Troubleshooting' step on the left.
+If the script executes without displaying an error, Elan has successfully been installed. If it displays an error that you do not understand, click on the 'Questions and Troubleshooting' step on the left.

vscode-lean4/media/guide-installElan-windows.md

@@ -3,4 +3,4 @@
 
 Clicking [this link](command:lean4.setup.installElan) will download the [Elan setup script](https://github.com/leanprover/elan/blob/master/elan-init.ps1) and execute it.
 
-If the script executes without displaying an error, both Elan and a current stable version of Lean 4 have been installed. If it displays an error that you do not understand, click on the 'Questions and Troubleshooting' step on the left.
+If the script executes without displaying an error, Elan has successfully been installed. If it displays an error that you do not understand, click on the 'Questions and Troubleshooting' step on the left.

vscode-lean4/src/utils/leanInstaller.ts

@@ -97,16 +97,14 @@ export class LeanInstaller {
         void this.showRestartPromptAndRestart('Lake file configuration changed', packageUri)
     }
 
-    private installElanPrompt(reason: string | undefined): { message: string; item: 'Install Elan and Lean 4' } {
+    private installElanPrompt(reason: string | undefined): { message: string; item: 'Install Elan' } {
         let message: string
         if (reason !== undefined) {
-            message = `${reason} Do you wish to install Lean's version manager Elan and a recent stable version of Lean 4?`
+            message = `${reason} Do you wish to install Lean's version manager Elan?`
         } else {
-            message =
-                "This command will install Lean's version manager Elan and a recent stable version of Lean 4.\n\n" +
-                'Do you wish to proceed?'
+            message = "This command will install Lean's version manager Elan.\n\n" + 'Do you wish to proceed?'
         }
-        const item = 'Install Elan and Lean 4'
+        const item = 'Install Elan'
         return { message, item }
     }
 
@@ -145,11 +143,11 @@ export class LeanInstaller {
         severity: NotificationSeverity,
         reason: string | undefined,
         // eslint-disable-next-line @typescript-eslint/no-redundant-type-constituents
-        options: StickyNotificationOptions<'Install Elan and Lean 4' | string>,
+        options: StickyNotificationOptions<'Install Elan' | string>,
         otherItems: StickyInput<string>[] = [],
     ): Disposable {
         const p = this.installElanPrompt(reason)
-        const installElanItem: StickyInput<'Install Elan and Lean 4'> = {
+        const installElanItem: StickyInput<'Install Elan'> = {
             input: p.item,
             continueDisplaying: false,
             action: async () => {