test: log git calls when Lake fails in the local-dep tests

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. |

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<T>(fn: () => Promise<T>): Promise<T> {
+    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
+}

vscode-lean4/test/helpers/lake.ts

@@ -1,27 +1,57 @@
 import { execFile } from 'node:child_process'
 import { promisify } from 'node:util'
+import { makeGitTraceDir, readGitTrace } from './gitTrace'
 
 const execFileAsync = promisify(execFile)
 
 // Runs `lake ...args` in `cwd` and returns its stdout. `execFile`, not
 // `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<string> {
+    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}`
+}

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)
         })
     })
 })