diff --git a/vscode-lean4/test/README.md b/vscode-lean4/test/README.md index ef35081f..4e78e0e5 100644 --- a/vscode-lean4/test/README.md +++ b/vscode-lean4/test/README.md @@ -138,7 +138,8 @@ The tests in `vscode-test-cli/`, `network/`, `wdio/` and `helpers/` run in VS Co | `stubs.trackStubs(stubs)` | Get a restore function for the stubs of a helper. `teardown.ts` restores the stubs that a test left. | | `fixtures.scaffoldFromFixture(name, prefix)` | Copy a fixture into the test home, for tests that change the project. | | `fixtures.assertNotInProject(dir)` | Make sure that no folder above `dir` has a `lean-toolchain` file or a lakefile, for tests of files outside of a project. | -| `lake.lake(cwd, args, timeoutMs)` | Run `lake` without a block of the extension host. The error contains stdout and stderr. | +| `lake.lake(cwd, args, timeoutMs)` | Run `lake` without a block of the extension host. The error contains the exit code, stdout, stderr and the git trace logs. | +| `gitTrace.withGitTrace(fn)` | Run `fn` with `GIT_TRACE2` set, so that the git calls of the extension (also through Lake) write logs. If `fn` fails, the error contains the logs. Lake does not tell how a git call failed. | | `testHome.requireIsolatedTestHome({ requireElanHome })` | Make sure that the test home is isolated before a test changes elan state. | | `testHome.makeTestWorkDir(prefix)` | Make a scratch folder in the test home. | | `mockToolchain.withMockToolchain(name, { leanVersion }, fn)` | Link a mock toolchain whose `lean` prints the given version. If the extension starts a server from it, wait in `fn` until the server ended (see `preconditions.test.ts`). On Windows, the removal stops the programs that still run from the toolchain, and logs them. | diff --git a/vscode-lean4/test/helpers/gitTrace.ts b/vscode-lean4/test/helpers/gitTrace.ts new file mode 100644 index 00000000..3528fde3 --- /dev/null +++ b/vscode-lean4/test/helpers/gitTrace.ts @@ -0,0 +1,79 @@ +import * as fs from 'node:fs' +import * as path from 'node:path' +import { makeTestWorkDir } from './testHome' + +// If `GIT_TRACE2` is the absolute path of a folder, each git process writes a +// log (Git trace2, normal format) to a new file in the folder. The log shows +// the command line, the child processes and their exit codes, the messages of +// `die()`, and the exit code of the process. +// +// Lake does not tell how a git call failed. For example, it reports a failed +// `git fetch` only as "failed to fetch the package revision". On Windows, git +// can also stop without a message: then Lake shows no output of git at all. +// With the logs, a log without an `exit` line shows the process that stopped, +// and a missing log shows a process that did not start. +// +// The value must be a folder. With `1` or `2`, git writes the log to stdout or +// stderr, and Lake reads the stdout of some git calls. + +// Makes a new folder for the logs. The next test run deletes it. +export function makeGitTraceDir(): string { + return makeTestWorkDir('git-trace-') +} + +// Returns the logs in `dir`, in the order in which the processes started. +export function readGitTrace(dir: string): string { + let files: string[] + try { + // The file names start with the start time of the process (the trace2 + // session ID), so the alphabetical order is the start order. + files = fs.readdirSync(dir).sort() + } catch (e) { + return `git trace: cannot read ${dir}: ${(e as Error).message}` + } + if (files.length === 0) { + return `git trace: no git process wrote a log to ${dir}` + } + const logs = files.map(file => `--- ${file}\n${fs.readFileSync(path.join(dir, file), 'utf8').trimEnd()}`) + return `git trace (${dir}):\n${logs.join('\n')}` +} + +// Runs `fn` with `GIT_TRACE2` in `process.env`. The extension starts its +// processes with `process.env`, so its git calls (also through Lake) write +// logs. If `fn` fails, the error message gets the logs. +export async function withGitTrace(fn: () => Promise): Promise { + const dir = makeGitTraceDir() + const previous = process.env.GIT_TRACE2 + process.env.GIT_TRACE2 = dir + try { + return await fn() + } catch (e) { + throw appendToError(e, readGitTrace(dir)) + } finally { + if (previous === undefined) { + delete process.env.GIT_TRACE2 + } else { + process.env.GIT_TRACE2 = previous + } + } +} + +// Adds `text` to the message of `e`. The stack starts with the message, and +// mocha and the state dump (`teardown.ts`) print the stack, so we change the +// message in the stack too. We keep the error object: mocha shows the diff of +// an `AssertionError`. +function appendToError(e: unknown, text: string): unknown { + if (!(e instanceof Error)) { + return new Error(`${String(e)}\n${text}`) + } + const message = e.message + e.message = `${message}\n${text}` + if (e.stack !== undefined) { + // A function as the replacement, so that `$` in the logs is not a pattern. + e.stack = + message !== '' && e.stack.includes(message) + ? e.stack.replace(message, () => e.message) + : `${e.stack}\n${text}` + } + return e +} diff --git a/vscode-lean4/test/helpers/lake.ts b/vscode-lean4/test/helpers/lake.ts index d20006cb..f54e9716 100644 --- a/vscode-lean4/test/helpers/lake.ts +++ b/vscode-lean4/test/helpers/lake.ts @@ -1,5 +1,6 @@ import { execFile } from 'node:child_process' import { promisify } from 'node:util' +import { makeGitTraceDir, readGitTrace } from './gitTrace' const execFileAsync = promisify(execFile) @@ -7,21 +8,50 @@ const execFileAsync = promisify(execFile) // `execFileSync`: a build or a download takes minutes, and a synchronous call // blocks the extension host for that time. Stops lake after `timeoutMs`. Fails // with stdout and stderr in the message: Lake writes most errors to stdout. +// The message also has the logs of the git calls of Lake (`gitTrace.ts`): +// Lake does not tell how a git call failed. export async function lake(cwd: string, args: string[], timeoutMs: number): Promise { + const traceDir = makeGitTraceDir() try { const { stdout } = await execFileAsync('lake', args, { cwd, - env: process.env, + env: { ...process.env, GIT_TRACE2: traceDir }, encoding: 'utf8', maxBuffer: 64 * 1024 * 1024, timeout: timeoutMs, }) return stdout } catch (e) { - const err = e as Error & { stdout?: string; stderr?: string } + const err = e as ExecError throw new Error( - `\`lake ${args.join(' ')}\` failed in ${cwd}: ${err.message}\n` + - `stdout:\n${err.stdout ?? ''}\nstderr:\n${err.stderr ?? ''}`, + `\`lake ${args.join(' ')}\` failed in ${cwd}: ${describeFailure(err, timeoutMs)}\n` + + `stdout:\n${err.stdout ?? ''}\nstderr:\n${err.stderr ?? ''}\n${readGitTrace(traceDir)}`, ) } } + +// The error of `execFile`. `code` is the exit code, or a string if lake did not start. +type ExecError = Error & { + code?: number | string | null + signal?: string | null + killed?: boolean + stdout?: string + stderr?: string +} + +function describeFailure(err: ExecError, timeoutMs: number): string { + if (typeof err.code === 'string') { + return err.message + } + if (err.killed) { + return `stopped after the timeout of ${timeoutMs} ms (${err.signal})` + } + if (err.signal) { + return `stopped by ${err.signal}` + } + // On Windows, a crash gives an NTSTATUS code, for example 0xC0000005. + const code = err.code ?? 'unknown' + return typeof code === 'number' && code > 255 + ? `exit code ${code} (0x${code.toString(16).toUpperCase()})` + : `exit code ${code}` +} diff --git a/vscode-lean4/test/vscode-test-cli/project-actions.test.ts b/vscode-lean4/test/vscode-test-cli/project-actions.test.ts index 7a9faf0d..99f13ada 100644 --- a/vscode-lean4/test/vscode-test-cli/project-actions.test.ts +++ b/vscode-lean4/test/vscode-test-cli/project-actions.test.ts @@ -7,6 +7,7 @@ import { openInEditor } from '../helpers/editors' import { elanCachedResolution } from '../helpers/elan' import { scaffoldFromFixture } from '../helpers/fixtures' import { git, gitText, initGitRepo } from '../helpers/git' +import { withGitTrace } from '../helpers/gitTrace' import { lake } from '../helpers/lake' import { choose, dismiss, withPrompts } from '../helpers/prompts' import { withQuickPicks } from '../helpers/quickPicks' @@ -231,6 +232,9 @@ describe('Project action commands', function () { // `consumer/lakefile.toml` requires `dep` with `git = "../dep"`. Both halves // are copied into the same folder, so the relative URL resolves. + // `lake update` fetches `dep` with git. On Windows, this fetch failed one + // time without a message from git. Thus a failure shows the logs of the git + // calls (`lake` and `withGitTrace`). describe('with a local git dependency', function () { let depDir: string let consumerDir: string @@ -263,15 +267,17 @@ describe('Project action commands', function () { assert.notStrictEqual(expectedRev, beforeRev) await openAndAwaitClient(Uri.file(path.join(consumerDir, 'Consumer.lean')), CLIENT_READY_MS) - await withQuickPicks(['dep'], async () => { - await withPrompts( - [choose(/^This command will update dep to its most recent version\./, 'Proceed')], - async () => { - await commands.executeCommand('lean4.project.updateDependency') - }, - ) + await withGitTrace(async () => { + await withQuickPicks(['dep'], async () => { + await withPrompts( + [choose(/^This command will update dep to its most recent version\./, 'Proceed')], + async () => { + await commands.executeCommand('lean4.project.updateDependency') + }, + ) + }) + assert.strictEqual(readDepRev(), expectedRev) }) - assert.strictEqual(readDepRev(), expectedRev) }) // Lake reads a channel such as `leanprover/lean4:stable` as a name that it @@ -289,25 +295,27 @@ describe('Project action commands', function () { git(depDir, 'commit', '-am', 'Change the Lean version of dep') await openAndAwaitClient(Uri.file(path.join(consumerDir, 'Consumer.lean')), CLIENT_READY_MS) - await withQuickPicks(['dep'], async () => { - await withPrompts( - [ - choose(/^This command will update dep to its most recent version\./, 'Proceed'), - choose( - /^The Lean version '.*' of the open project differs from the Lean version '.*' of dep\./, - 'Update Lean Version', - ), - // The file watcher of the client sees the new `lean-toolchain`. - dismiss(/^Project Lean version \(`lean-toolchain`\) of 'consumer' has changed\./, { - optional: true, - }), - ], - async () => { - await commands.executeCommand('lean4.project.updateDependency') - }, - ) + await withGitTrace(async () => { + await withQuickPicks(['dep'], async () => { + await withPrompts( + [ + choose(/^This command will update dep to its most recent version\./, 'Proceed'), + choose( + /^The Lean version '.*' of the open project differs from the Lean version '.*' of dep\./, + 'Update Lean Version', + ), + // The file watcher of the client sees the new `lean-toolchain`. + dismiss(/^Project Lean version \(`lean-toolchain`\) of 'consumer' has changed\./, { + optional: true, + }), + ], + async () => { + await commands.executeCommand('lean4.project.updateDependency') + }, + ) + }) + assert.strictEqual(fs.readFileSync(consumerToolchainPath, 'utf8'), depToolchain) }) - assert.strictEqual(fs.readFileSync(consumerToolchainPath, 'utf8'), depToolchain) }) }) })