test: remove 'no elan' tests and DISABLE_ELAN flag

leanprover · Apr 30, 2024 · 73b1363 · 73b1363
1 parent 5fb8b0a
commit 73b1363
Show file tree

Hide file tree

Showing 7 changed files with 12 additions and 96 deletions.
diff --git a/.vscode/launch.json b/.vscode/launch.json
@@ -67,23 +67,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",

diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts
@@ -252,10 +252,6 @@ export function getDefaultLeanVersion(): string {
         : 'leanprover/lean4:stable'
 }
 
-export function isElanDisabled(): boolean {
-    return typeof process.env.DISABLE_ELAN === 'string'
-}
-
 /** The editor line height, in pixels. */
 export function getEditorLineHeight(): number {
     // The implementation

diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts
@@ -1,13 +1,6 @@
 import { commands, Disposable, ExtensionContext, extensions, TextDocument, window, workspace } from 'vscode'
 import { AbbreviationFeature } from './abbreviation'
-import {
-    addDefaultElanPath,
-    addToolchainBinPath,
-    getDefaultElanPath,
-    getDefaultLeanVersion,
-    isElanDisabled,
-    removeElanPath,
-} from './config'
+import { addDefaultElanPath, getDefaultLeanVersion } from './config'
 import { DocViewProvider } from './docview'
 import { AlwaysEnabledFeatures, Exports, Lean4EnabledFeatures } from './exports'
 import { checkLean4FeaturePreconditions } from './globalDiagnostics'
@@ -51,15 +44,7 @@ function findOpenLeanDocument(): TextDocument | undefined {
  * Activates all extension features that are *always* enabled, even when no Lean 4 document is currently open.
  */
 function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabledFeatures {
-    // For unit test that tests behavior when there is no elan installed.
-    if (isElanDisabled()) {
-        const elanRoot = removeElanPath()
-        if (elanRoot) {
-            addToolchainBinPath(elanRoot)
-        }
-    } else {
-        addDefaultElanPath()
-    }
+    addDefaultElanPath()
 
     context.subscriptions.push(
         commands.registerCommand('lean4.setup.showSetupGuide', async () =>
@@ -84,11 +69,7 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled
     context.subscriptions.push(
         commands.registerCommand('lean4.setup.installElan', async () => {
             await installer.installElan()
-            if (isElanDisabled()) {
-                addToolchainBinPath(getDefaultElanPath())
-            } else {
-                addDefaultElanPath()
-            }
+            addDefaultElanPath()
         }),
     )
 

diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts
@@ -1,14 +1,5 @@
 import { EventEmitter, OutputChannel, TerminalOptions, window } from 'vscode'
-import {
-    addDefaultElanPath,
-    addToolchainBinPath,
-    getDefaultElanPath,
-    getPowerShellPath,
-    isElanDisabled,
-    isRunningTest,
-    shouldAutofocusOutput,
-    toolchainPath,
-} from '../config'
+import { addDefaultElanPath, getPowerShellPath, isRunningTest, shouldAutofocusOutput, toolchainPath } from '../config'
 import { batchExecute } from './batch'
 import { ExtUri, FileUri } from './exturi'
 import { logger } from './logger'
@@ -195,12 +186,10 @@ export class LeanInstaller {
     }
 
     async autoInstall(): Promise<void> {
+        logger.log('[LeanInstaller] Installing Elan ...')
         await this.installElan()
-        if (isElanDisabled()) {
-            addToolchainBinPath(getDefaultElanPath())
-        } else {
-            addDefaultElanPath()
-        }
+        logger.log('[LeanInstaller] Elan installed')
+        addDefaultElanPath()
     }
 
     async installElan(): Promise<boolean> {

diff --git a/vscode-lean4/test/suite/index/index.ts b/vscode-lean4/test/suite/index/index.ts
@@ -1,7 +1,7 @@
 import * as glob from 'glob'
 import * as Mocha from 'mocha'
 import * as path from 'path'
-import { getTestFolder, isElanDisabled } from '../../../src/config'
+import { getTestFolder } from '../../../src/config'
 import { logger } from '../../../src/utils/logger'
 
 export function run(testsRoot: string, cb: (error: any, failures?: number) => void): void {
@@ -21,10 +21,6 @@ export function run(testsRoot: string, cb: (error: any, failures?: number) => vo
 
     logger.log('>>>>>>>>> testsRoot=' + testsRoot)
 
-    if (isElanDisabled()) {
-        logger.log('>>>>>>>>> running without elan')
-    }
-
     glob('**/**.test.js', { cwd: testsRoot }, (err, files) => {
         if (err) {
             return cb(err)

diff --git a/vscode-lean4/test/suite/runTest.ts b/vscode-lean4/test/suite/runTest.ts
@@ -83,34 +83,14 @@ async function main() {
         // now that elan is installed we can run the lean3 test in one vs code instance,
         // using `open folder` since lean3 doesn't like ad-hoc files.
 
-        // BUGBUG: this test has begun to fail on newer vscode builds with "Uncaught Error: write EPIPE"
-        // await runTests({
-        //     vscodeExecutablePath,
-        //     extensionDevelopmentPath,
-        //     extensionTestsPath: path.resolve(__dirname, 'index'),
-        //     extensionTestsEnv: {'LEAN4_TEST_FOLDER': 'lean3'},
-        //     launchArgs: ['--new-window', '--disable-gpu'] });
-        // // The '--new-window' doesn't see to be working, so this hack
-        // // ensures the following test does not re-open the lean3 folder
-        // clearUserWorkspaceData(vscodeTestPath);
-
-        // run 'no elan' tests
-        await runTests({
-            vscodeExecutablePath,
-            extensionDevelopmentPath,
-            extensionTestsPath: path.resolve(__dirname, 'index'),
-            extensionTestsEnv: { LEAN4_TEST_FOLDER: 'simple', DISABLE_ELAN: '1', DEFAULT_LEAN_TOOLCHAIN: test_version },
-            launchArgs: ['--new-window', '--disable-gpu'],
-        })
-
         clearUserWorkspaceData(vscodeTestPath)
 
         // run the infoView tests
         await runTests({
             vscodeExecutablePath,
             extensionDevelopmentPath,
             extensionTestsPath: path.resolve(__dirname, 'index'),
-            extensionTestsEnv: { LEAN4_TEST_FOLDER: 'info', DISABLE_ELAN: '1', DEFAULT_LEAN_TOOLCHAIN: test_version },
+            extensionTestsEnv: { LEAN4_TEST_FOLDER: 'info', DEFAULT_LEAN_TOOLCHAIN: test_version },
             launchArgs: ['--new-window', '--disable-gpu'],
         })
 

diff --git a/vscode-lean4/test/suite/simple/simple.test.ts b/vscode-lean4/test/suite/simple/simple.test.ts
@@ -2,7 +2,6 @@ import * as assert from 'assert'
 import { suite } from 'mocha'
 import * as path from 'path'
 import * as vscode from 'vscode'
-import { isElanDisabled } from '../../../src/config'
 import { UntitledUri } from '../../../src/utils/exturi'
 import { logger } from '../../../src/utils/logger'
 import {
@@ -16,17 +15,9 @@ import {
     waitForInfoviewHtml,
 } from '../utils/helpers'
 
-function getElanMode() {
-    let mode = ''
-    if (isElanDisabled()) {
-        mode = ' no elan '
-    }
-    return mode
-}
-
 suite('Lean4 Basics Test Suite', () => {
     test('Untitled Lean File', async () => {
-        logger.log(`=================== Untitled Lean File ${getElanMode()} ===================`)
+        logger.log('=================== Untitled Lean File ===================')
         void vscode.window.showInformationMessage('Running tests: ' + __dirname)
 
         const features = await initLean4Untitled('#eval Lean.versionString')
@@ -59,7 +50,7 @@ suite('Lean4 Basics Test Suite', () => {
     }).timeout(60000)
 
     test('Orphaned Lean File', async () => {
-        logger.log(`=================== Orphaned Lean File ${getElanMode()} ===================`)
+        logger.log('=================== Orphaned Lean File ===================')
         void vscode.window.showInformationMessage('Running tests: ' + __dirname)
 
         const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'orphan')
@@ -90,7 +81,7 @@ suite('Lean4 Basics Test Suite', () => {
     }).timeout(60000)
 
     test('Goto definition in a package folder', async () => {
-        logger.log(`=================== Goto definition in a package folder  ${getElanMode()} ===================`)
+        logger.log('=================== Goto definition in a package folder ===================')
         void vscode.window.showInformationMessage('Running tests: ' + __dirname)
 
         // Test we can load file in a project folder from a package folder and also