Skip to content

Commit

Permalink
chore: adjust tests for adjusted activation logic
Browse files Browse the repository at this point in the history
  • Loading branch information
@mhuisi
mhuisi committed Apr 29, 2024
1 parent 86502c0 commit e73a0e7
Show file tree
Hide file tree
Showing 12 changed files with 125 additions and 83 deletions.
17 changes: 15 additions & 2 deletions vscode-lean4/src/exports.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,19 @@ export interface Lean4EnabledFeatures {
projectOperationProvider: ProjectOperationProvider
}

export interface Exports extends AlwaysEnabledFeatures {
activatedLean4Features: Thenable<Lean4EnabledFeatures>
export interface EnabledFeatures extends AlwaysEnabledFeatures, Lean4EnabledFeatures {}

export class Exports {
alwaysEnabledFeatures: AlwaysEnabledFeatures
lean4EnabledFeatures: Promise<Lean4EnabledFeatures>

constructor(alwaysEnabledFeatures: AlwaysEnabledFeatures, lean4EnabledFeatures: Promise<Lean4EnabledFeatures>) {
this.alwaysEnabledFeatures = alwaysEnabledFeatures
this.lean4EnabledFeatures = lean4EnabledFeatures
}

async allFeatures(): Promise<EnabledFeatures> {
const lean4EnabledFeatures = await this.lean4EnabledFeatures
return { ...this.alwaysEnabledFeatures, ...lean4EnabledFeatures }
}
}
49 changes: 24 additions & 25 deletions vscode-lean4/src/extension.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,29 +155,28 @@ export async function activate(context: ExtensionContext): Promise<Exports> {
const alwaysEnabledFeatures: AlwaysEnabledFeatures = activateAlwaysEnabledFeatures(context)
activateAbbreviationFeature(context, alwaysEnabledFeatures.docView)

return {
...alwaysEnabledFeatures,
activatedLean4Features: new Promise(async (resolve, _) => {
const doc: TextDocument | undefined = findOpenLeanDocument()
if (doc) {
const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features(
context,
alwaysEnabledFeatures.installer,
)
resolve(lean4EnabledFeatures)
} else {
// No Lean 4 document yet => Load remaining features when one is open
const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => {
if (isLean4Document(doc)) {
const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features(
context,
alwaysEnabledFeatures.installer,
)
resolve(lean4EnabledFeatures)
disposeActivationListener.dispose()
}
}, context.subscriptions)
}
}),
}
const lean4EnabledFeatures: Promise<Lean4EnabledFeatures> = new Promise(async (resolve, _) => {
const doc: TextDocument | undefined = findOpenLeanDocument()
if (doc) {
const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features(
context,
alwaysEnabledFeatures.installer,
)
resolve(lean4EnabledFeatures)
} else {
// No Lean 4 document yet => Load remaining features when one is open
const disposeActivationListener: Disposable = workspace.onDidOpenTextDocument(async doc => {
if (isLean4Document(doc)) {
const lean4EnabledFeatures: Lean4EnabledFeatures = await activateLean4Features(
context,
alwaysEnabledFeatures.installer,
)
resolve(lean4EnabledFeatures)
disposeActivationListener.dispose()
}
}, context.subscriptions)
}
})

return new Exports(alwaysEnabledFeatures, lean4EnabledFeatures)
}
12 changes: 6 additions & 6 deletions vscode-lean4/test/suite/bootstrap/bootstrap.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,15 +22,15 @@ suite('Lean4 Bootstrap Test Suite', () => {

// this will wait up to 60 seconds to do full elan lean install, so test machines better
// be able to do that.
const lean = await initLean4Untitled('#eval Lean.versionString')
const info = lean.exports.infoProvider
const features = await initLean4Untitled('#eval Lean.versionString')
const info = features.infoProvider
const expected = '4.0.0-nightly-'
assert(info, 'No InfoProvider export')

// give it a extra long timeout in case test machine is really slow.
logger.log('Wait for elan install of Lean nightly build...')
await waitForActiveClient(lean.exports.clientProvider, 120)
await waitForActiveClientRunning(lean.exports.clientProvider, 300)
await waitForActiveClient(features.clientProvider, 120)
await waitForActiveClientRunning(features.clientProvider, 300)

const hackNeeded = false
if (hackNeeded) {
Expand Down Expand Up @@ -69,8 +69,8 @@ suite('Lean4 Bootstrap Test Suite', () => {
void vscode.window.showInformationMessage('Running tests: ' + __dirname)

// Lean is already installed so this should be quick.
const lean = await initLean4Untitled('#eval Lean.versionString')
const info = lean.exports.infoProvider
const features = await initLean4Untitled('#eval Lean.versionString')
const info = features.infoProvider
assert(info, 'No InfoProvider export')

logger.log('Wait for Lean nightly build server to start...')
Expand Down
6 changes: 3 additions & 3 deletions vscode-lean4/test/suite/docview/docview.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,8 @@ suite('Documentation View Test Suite', () => {
void vscode.window.showInformationMessage('Running tests: ' + __dirname)
const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple')
const mainFile = path.join(testsRoot, 'Main.lean')
const lean = await initLean4(mainFile)
const info = lean.exports.infoProvider
const features = await initLean4(mainFile)
const info = features.infoProvider
assert(info, 'No InfoProvider export')
const expectedVersion = 'Hello:'
let html = await waitForInfoviewHtml(info, expectedVersion)
Expand All @@ -36,7 +36,7 @@ suite('Documentation View Test Suite', () => {

await vscode.commands.executeCommand('lean4.docView.open')

const docView = lean.exports.docView
const docView = features.docView
assert(docView, 'No docView export')
const expectedMenuItem = 'Abbreviations Cheatsheet'
html = await waitForDocViewHtml(docView, expectedMenuItem)
Expand Down
16 changes: 8 additions & 8 deletions vscode-lean4/test/suite/info/info.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@ suite('InfoView Test Suite', () => {
const b = 22
const expectedEval1 = (a * b).toString()

const lean = await initLean4Untitled(`#eval ${a}*${b}`)
const info = lean.exports.infoProvider
const features = await initLean4Untitled(`#eval ${a}*${b}`)
const info = features.infoProvider
assert(info, 'No InfoProvider export')

await assertStringInInfoview(info, expectedEval1)
Expand All @@ -49,8 +49,8 @@ suite('InfoView Test Suite', () => {
const c = 77
const d = 7

const lean = await initLean4Untitled(`#eval ${a}*${b}`)
const info = lean.exports.infoProvider
const features = await initLean4Untitled(`#eval ${a}*${b}`)
const info = features.infoProvider
assert(info, 'No InfoProvider export')

const expectedEval1 = (a * b).toString()
Expand Down Expand Up @@ -84,12 +84,12 @@ suite('InfoView Test Suite', () => {

const expectedEval = '[1, 2, 3]'

const lean = await initLean4Untitled('#eval [1, 1+1, 1+1+1] \n')
const features = await initLean4Untitled('#eval [1, 1+1, 1+1+1] \n')
const editor = await waitForActiveEditor()
const firstLine = editor.document.lineAt(0).range
editor.selection = new vscode.Selection(firstLine.end, firstLine.end)

const info = lean.exports.infoProvider
const info = features.infoProvider
assert(info, 'No InfoProvider export')
await waitForInfoviewHtml(info, expectedEval, 30, 1000, false)

Expand Down Expand Up @@ -127,8 +127,8 @@ suite('InfoView Test Suite', () => {
const b = 95
const prefix = 'Lean version is:'

const lean = await initLean4Untitled(`#eval ${a}*${b}`)
const info = lean.exports.infoProvider
const features = await initLean4Untitled(`#eval ${a}*${b}`)
const info = features.infoProvider
assert(info, 'No InfoProvider export')

const expectedEval = (a * b).toString()
Expand Down
9 changes: 7 additions & 2 deletions vscode-lean4/test/suite/lean3/lean3.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,12 @@ import { suite } from 'mocha'
import * as path from 'path'
import * as vscode from 'vscode'
import { logger } from '../../../src/utils/logger'
import { closeAllEditors, waitForActiveEditor, waitForActiveExtension } from '../utils/helpers'
import {
assertLean4FeaturesNotLoaded,
closeAllEditors,
waitForActiveEditor,
waitForActiveExtension,
} from '../utils/helpers'

suite('Lean3 Compatibility Test Suite', () => {
test('Lean3 project', async () => {
Expand All @@ -21,7 +26,7 @@ suite('Lean3 Compatibility Test Suite', () => {

const lean = await waitForActiveExtension('leanprover.lean4')
assert(lean, 'Lean extension not loaded')
assert(!lean.exports.isLean4Project, 'Lean4 extension should not be running!')
await assertLean4FeaturesNotLoaded(lean.exports)

logger.log('Checking vscode commands...')
const cmds = await vscode.commands.getCommands(true)
Expand Down
6 changes: 3 additions & 3 deletions vscode-lean4/test/suite/multi/multi.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,10 @@ suite('Multi-Folder Test Suite', () => {
void vscode.window.showInformationMessage('Running tests: ' + __dirname)

const multiRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'multi')
const lean = await initLean4(path.join(multiRoot, 'test', 'Main.lean'))
const features = await initLean4(path.join(multiRoot, 'test', 'Main.lean'))

// verify we have a nightly build running in this folder.
const info = lean.exports.infoProvider
const info = features.infoProvider
assert(info, 'No InfoProvider export')
await assertStringInInfoview(info, '4.0.0-nightly-')

Expand All @@ -30,7 +30,7 @@ suite('Multi-Folder Test Suite', () => {
await assertStringInInfoview(info, version)

// Now verify we have 2 LeanClients running.
const clients = lean.exports.clientProvider
const clients = features.clientProvider
assert(clients, 'No LeanClientProvider export')
const actual = clients.getClients().length
assert(actual === 2, 'Expected 2 LeanClients to be running, but found ' + actual)
Expand Down
7 changes: 3 additions & 4 deletions vscode-lean4/test/suite/pre-bootstrap/user.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,9 @@ suite('Lean4 Pre-bootstrap Test Suite', () => {

// this will wait up to 60 seconds to do full elan lean install, so test machines better
// be able to do that.
const promptUser = true
const projectRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple')
const lean = await initLean4(path.join(projectRoot, 'Main.lean'))
const info = lean.exports.infoProvider
const features = await initLean4(path.join(projectRoot, 'Main.lean'))
const info = features.infoProvider
const expected1 = 'Waiting for Lean server to start...'
const expected2 = 'nightly' // lean was already installed before this test started!
assert(info, 'No InfoProvider export')
Expand All @@ -33,7 +32,7 @@ suite('Lean4 Pre-bootstrap Test Suite', () => {

let retries = 10
while (html.indexOf(expected1) > 0) {
const installer = lean.exports.installer
const installer = features.installer
if (!installer?.isPromptVisible()) {
html = await waitForInfoviewLambda(info, lambda, 10)
retries--
Expand Down
18 changes: 9 additions & 9 deletions vscode-lean4/test/suite/restarts/restarts.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,14 +28,14 @@ suite('Lean Server Restart Test Suite', () => {

// add normal values to initialize lean4 file
const hello = 'Hello World'
const lean = await initLean4Untitled(`#eval "${hello}"`)
const info = lean.exports.infoProvider
const features = await initLean4Untitled(`#eval "${hello}"`)
const info = features.infoProvider
assert(info, 'No InfoProvider export')

logger.log('make sure language server is up and running.')
await assertStringInInfoview(info, hello)

const clients = lean.exports.clientProvider
const clients = features.clientProvider
assert(clients, 'No LeanClientProvider export')

logger.log('Insert eval that causes crash.')
Expand Down Expand Up @@ -73,14 +73,14 @@ suite('Lean Server Restart Test Suite', () => {

// add normal values to initialize lean4 file
const hello = 'Hello World'
const lean = await initLean4Untitled(`#eval "${hello}"`)
const info = lean.exports.infoProvider
const features = await initLean4Untitled(`#eval "${hello}"`)
const info = features.infoProvider
assert(info, 'No InfoProvider export')

logger.log('make sure language server is up and running.')
await assertStringInInfoview(info, hello)

const clients = lean.exports.clientProvider
const clients = features.clientProvider
assert(clients, 'No LeanClientProvider export')

logger.log('Insert eval that causes crash.')
Expand Down Expand Up @@ -119,9 +119,9 @@ suite('Lean Server Restart Test Suite', () => {

// run this code twice to ensure that it still works after a Restart Server
for (let i = 0; i < 2; i++) {
const lean = await initLean4(path.join(simpleRoot, 'Main.lean'))
const features = await initLean4(path.join(simpleRoot, 'Main.lean'))

const info = lean.exports.infoProvider
const info = features.infoProvider
assert(info, 'No InfoProvider export')

const activeEditor = vscode.window.activeTextEditor
Expand All @@ -139,7 +139,7 @@ suite('Lean Server Restart Test Suite', () => {
logger.log(`>>> Found "${versionString}" in infoview`)

logger.log('Now invoke the restart server command')
const clients = lean.exports.clientProvider
const clients = features.clientProvider
assert(clients, 'No LeanClientProvider export')
const client = clients.getClientForFolder(new FileUri(simpleRoot))
if (client) {
Expand Down
14 changes: 7 additions & 7 deletions vscode-lean4/test/suite/simple/simple.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ suite('Lean4 Basics Test Suite', () => {
logger.log(`=================== Untitled Lean File ${getElanMode()} ===================`)
void vscode.window.showInformationMessage('Running tests: ' + __dirname)

const lean = await initLean4Untitled('#eval Lean.versionString')
const info = lean.exports.infoProvider
const features = await initLean4Untitled('#eval Lean.versionString')
const info = features.infoProvider
assert(info, 'No InfoProvider export')

await assertStringInInfoview(info, '4.0.0-nightly-')
Expand Down Expand Up @@ -63,14 +63,14 @@ suite('Lean4 Basics Test Suite', () => {
void vscode.window.showInformationMessage('Running tests: ' + __dirname)

const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'orphan')
const lean = await initLean4(path.join(testsRoot, 'factorial.lean'))
const features = await initLean4(path.join(testsRoot, 'factorial.lean'))

const info = lean.exports.infoProvider
const info = features.infoProvider
assert(info, 'No InfoProvider export')
const expectedVersion = '5040' // the factorial function works.
const html = await waitForInfoviewHtml(info, expectedVersion)

const installer = lean.exports.installer
const installer = features.installer
assert(installer, 'No LeanInstaller export')
const toolChains = await installer.elanListToolChains(new UntitledUri())
let defaultToolChain = toolChains.find(tc => tc.indexOf('default') > 0)
Expand Down Expand Up @@ -101,9 +101,9 @@ suite('Lean4 Basics Test Suite', () => {
// and again using "open folder" mode.

const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple')
const lean = await initLean4(path.join(testsRoot, 'Main.lean'))
const features = await initLean4(path.join(testsRoot, 'Main.lean'))

const info = lean.exports.infoProvider
const info = features.infoProvider
assert(info, 'No InfoProvider export')
let expectedVersion = 'Hello:'
let html = await waitForInfoviewHtml(info, expectedVersion)
Expand Down
6 changes: 3 additions & 3 deletions vscode-lean4/test/suite/toolchains/toolchain.test.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,12 +21,12 @@ suite('Toolchain Test Suite', () => {

const testsRoot = path.join(__dirname, '..', '..', '..', '..', 'test', 'test-fixtures', 'simple')

const lean = await initLean4(path.join(testsRoot, 'Main.lean'))
const features = await initLean4(path.join(testsRoot, 'Main.lean'))

// turn off the user prompts so restart of lean server happens automatically.
const info = lean.exports.infoProvider
const info = features.infoProvider
assert(info, 'No InfoProvider export')
const installer = lean.exports.installer
const installer = features.installer
assert(installer, 'No LeanInstaller export')

// wait for info view to show up.
Expand Down
Loading

0 comments on commit e73a0e7

Please sign in to comment.