Merge pull request #24 from ammkrn/path_check

add user paths for version check, fix path field access

src/config.ts

@@ -1,9 +1,27 @@
 import { workspace } from 'vscode'
 import { InfoViewTacticStateFilter } from './infoviewApi';
+import * as path from 'path';
 
 // TODO: does currently not contain config options for `./abbreviation`
 // so that it is easy to keep it in sync with vscode-lean.
 
+// Make a copy of the passed process environment that includes the user's
+// `lean4.serverEnvPaths` in the path key, and adds the key/value pairs from
+// `lean4.serverEnv`. Both of these settings can be found in the user's 
+// settings.json file
+export function addServerEnvPaths(input_env: NodeJS.ProcessEnv): NodeJS.ProcessEnv {
+    let env = Object.assign({}, input_env, serverEnv());
+    let paths = serverEnvPaths()
+    if (paths.length != 0) {
+        if (process.platform === 'win32') {
+            env['Path'] = paths.join(path.delimiter) + path.delimiter + process.env.Path
+        } else {
+            env['PATH'] = paths.join(path.delimiter) + path.delimiter + process.env.PATH
+        }
+    }  
+    return env
+}
+
 export function executablePath(): string {
     return workspace.getConfiguration('lean4').get('executablePath', 'lean')
 }

src/extension.ts

@@ -1,8 +1,8 @@
 import { workspace, commands, window, languages, ExtensionContext, TextDocument } from 'vscode'
 import { promisify } from 'util'
-import { exec } from 'child_process'
+import { execFile } from 'child_process'
 import { AbbreviationFeature } from './abbreviation'
-import { executablePath } from './config'
+import { executablePath, addServerEnvPaths } from './config'
 import { LeanClient } from './leanclient'
 import { InfoProvider } from './infoview'
 import { LeanTaskGutter } from './taskgutter'
@@ -13,17 +13,20 @@ async function checkLean4(): Promise<boolean> {
     if (folders) {
         folderPath = folders[0].uri.fsPath
     }
-    const cmd = `${executablePath()} --version`
+
+    const env = addServerEnvPaths(process.env);
+    const cmd = executablePath()
+    const options = ['--version']
     try {
         // If folderPath is undefined, this will use the process environment for cwd.
         // Specifically, if the extension was not opened inside of a folder, it
         // looks for a global (default) installation of Lean. This way, we can support
         // single file editing.
-        const { stdout, stderr } = await promisify(exec)(cmd, {cwd: folderPath})
+        const { stdout, stderr } = await promisify(execFile)(cmd, options, {cwd: folderPath, env: env })
         const filterVersion = /version (\d+)\.\d+\..+/
         const match = filterVersion.exec(stdout)
         if (!match) {
-            void window.showErrorMessage(`lean4: '${cmd}' returned incorrect version string '${stdout}'.`)
+            void window.showErrorMessage(`lean4: '${cmd} ${options}' returned incorrect version string '${stdout}'.`)
             return false
         }
         const major = match[1]
@@ -32,7 +35,7 @@ async function checkLean4(): Promise<boolean> {
         }
         return true
     } catch (err) {
-        void window.showErrorMessage(`lean4: Could not find Lean version by running '${cmd}'.`)
+        void window.showErrorMessage(`lean4: Could not find Lean version by running '${cmd} ${options}'.`)
         return false
     }
 }

src/leanclient.ts

@@ -9,7 +9,7 @@ import {
     ServerOptions
 } from 'vscode-languageclient/node'
 import * as ls from 'vscode-languageserver-protocol'
-import { executablePath, serverEnv, serverEnvPaths, serverLoggingEnabled, serverLoggingPath } from './config'
+import { executablePath, addServerEnvPaths, serverLoggingEnabled, serverLoggingPath } from './config'
 import { PlainGoal, ServerProgress } from './leanclientTypes'
 import { assert } from './utils/assert'
 import * as path from 'path'
@@ -62,12 +62,7 @@ export class LeanClient implements Disposable {
         if (this.isStarted()) {
             await this.stop()
         }
-        const env = Object.assign({}, process.env, serverEnv());
-        const paths = serverEnvPaths()
-        if (paths.length != 0) {
-            const pathKey = process.platform === 'win32' ? 'Path' : 'PATH'
-            env[pathKey] = paths.join(path.delimiter) + path.delimiter + process.env.Path
-        }
+        const env = addServerEnvPaths(process.env);
         if (serverLoggingEnabled()) {
             env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
         }