fix: adhoc files should not pick up default lean version from open folder

vscode-lean4/src/leanclient.ts

@@ -50,6 +50,7 @@ export class LeanClient implements Disposable {
     private subscriptions: Disposable[] = []
     private noPrompt : boolean = false;
     private showingRestartMessage : boolean = false;
+    private elanDefaultToolchain: string;
 
     private didChangeEmitter = new EventEmitter<DidChangeTextDocumentParams>()
     didChange = this.didChangeEmitter.event
@@ -91,11 +92,12 @@ export class LeanClient implements Disposable {
     /** Files which are open. */
     private isOpen: Map<string, TextDocument> = new Map()
 
-    constructor(workspaceFolder: WorkspaceFolder | undefined, folderUri: Uri, storageManager : LocalStorageService, outputChannel : OutputChannel) {
+    constructor(workspaceFolder: WorkspaceFolder | undefined, folderUri: Uri, storageManager : LocalStorageService, outputChannel : OutputChannel, elanDefaultToolchain: string) {
         this.storageManager = storageManager;
         this.outputChannel = outputChannel;
         this.workspaceFolder = workspaceFolder; // can be null when opening adhoc files.
         this.folderUri = folderUri;
+        this.elanDefaultToolchain = elanDefaultToolchain;
         this.subscriptions.push(workspace.onDidChangeConfiguration((e) => this.configChanged(e)));
     }
 
@@ -139,7 +141,7 @@ export class LeanClient implements Disposable {
         this.restartingEmitter.fire(undefined)
         this.toolchainPath = this.storageManager.getLeanPath();
         if (!this.toolchainPath) this.toolchainPath = toolchainPath();
-        const version = this.storageManager.getLeanVersion();
+        let version = this.storageManager.getLeanVersion();
         const env = addServerEnvPaths(process.env);
         if (serverLoggingEnabled()) {
             env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
@@ -174,6 +176,13 @@ export class LeanClient implements Disposable {
             executable = (this.toolchainPath) ? join(this.toolchainPath, 'bin', 'lean') : 'lean';
         }
 
+        const cwd = this.folderUri?.fsPath
+        if (!cwd && !version){
+            // Fixes issue #227, for adhoc files it would pick up the cwd from the open folder
+            // which is not what we want.  For adhoc files we want the (default) toolchain instead.
+            version = this.elanDefaultToolchain;
+        }
+
         let options = version ? ['+' + version] :[]
         if (useLake) {
             options = options.concat(['serve', '--'])
@@ -182,8 +191,8 @@ export class LeanClient implements Disposable {
         }
 
         // Add folder name to command-line so that it shows up in `ps aux`.
-        if (this.folderUri) {
-            options.push('' + this.folderUri.fsPath)
+        if (cwd) {
+            options.push('' + cwd)
         } else {
             options.push('untitled')
         }
@@ -192,7 +201,7 @@ export class LeanClient implements Disposable {
             command: executable,
             args: options.concat(serverArgs()),
             options: {
-                cwd: this.folderUri?.fsPath,
+                cwd,
                 env
             }
         }

vscode-lean4/src/utils/clientProvider.ts

@@ -274,13 +274,15 @@ export class LeanClientProvider implements Disposable {
             this.pending.set(key, true);
             logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString());
 
+            const elanDefaultToolchain = await this.installer.getElanDefaultToolchain(folderUri);
+
             // We must create a Client before doing the long running testLeanVersion
             // so that ensureClient callers have an "optimistic" client to work with.
             // This is needed in our constructor where it is calling ensureClient for
             // every open file.  A workspace could have multiple files open and we want
             // to remember all those open files are associated with this client before
             // testLeanVersion has completed.
-            client = new LeanClient(workspaceFolder, folderUri, this.localStorage, this.outputChannel);
+            client = new LeanClient(workspaceFolder, folderUri, this.localStorage, this.outputChannel, elanDefaultToolchain);
             this.subscriptions.push(client);
             this.clients.set(key, client);
 

vscode-lean4/src/utils/leanInstaller.ts

@@ -20,7 +20,8 @@ export class LeanInstaller implements Disposable {
     private localStorage: LocalStorageService;
     private subscriptions: Disposable[] = [];
     private prompting : boolean = false;
-    private defaultToolchain : string;
+    private defaultToolchain : string; // the default to use if there is no elan installed
+    private elanDefaultToolchain : string = ''; // the default toolchain according to elan (toolchain marked with '(default)')
     private workspaceSuffix : string = '(workspace override)';
     private defaultSuffix : string = '(default)'
     private versionCache: Map<string,LeanVersion> = new Map();
@@ -67,7 +68,7 @@ export class LeanInstaller implements Disposable {
                     return { version: '4', error: 'no elan installed' }
                 }
             } else if (! await isCoreLean4Directory(packageUri)) {
-                const defaultVersion = await this.getDefaultToolchain(packageUri);
+                const defaultVersion = await this.getElanDefaultToolchain(packageUri);
                 if (!defaultVersion) {
                     void this.showToolchainOptions(packageUri);
                 } else {
@@ -409,14 +410,20 @@ export class LeanInstaller implements Disposable {
         return stdout;
     }
 
-    async getDefaultToolchain(packageUri: Uri): Promise<string> {
+    async getElanDefaultToolchain(packageUri: Uri): Promise<string> {
+        if (this.elanDefaultToolchain){
+            return this.elanDefaultToolchain;
+        }
+
         const toolChains = await this.elanListToolChains(packageUri);
         let result :string = ''
         toolChains.forEach((s) => {
             if (s.endsWith(this.defaultSuffix)){
                 result = this.removeSuffix(s);
             }
         });
+
+        this.elanDefaultToolchain = result;
         return result;
     }
 
@@ -510,6 +517,7 @@ export class LeanInstaller implements Disposable {
 
             // clear any previous lean version errors.
             this.versionCache.clear();
+            this.elanDefaultToolchain = this.defaultToolchain;
 
             return result;
         }