From 9fbca4ddbdecab64923d750a686f18b534a37e5c Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Thu, 30 Jan 2025 16:16:31 +0100
Subject: [PATCH] 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    |  2 +-
 vscode-lean4/media/guide-installElan-windows.md |  2 +-
 vscode-lean4/src/utils/leanInstaller.ts         | 14 ++++++--------
 3 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/vscode-lean4/media/guide-installElan-unix.md b/vscode-lean4/media/guide-installElan-unix.md
index 09082b32f..cae8c53d5 100644
--- a/vscode-lean4/media/guide-installElan-unix.md
+++ b/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.
diff --git a/vscode-lean4/media/guide-installElan-windows.md b/vscode-lean4/media/guide-installElan-windows.md
index 054c0fcd1..40f98fe6f 100644
--- a/vscode-lean4/media/guide-installElan-windows.md
+++ b/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.
diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts
index 0cad1167d..819ebaba5 100644
--- a/vscode-lean4/src/utils/leanInstaller.ts
+++ b/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 () => {