Skip to content

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

Merged
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-uspwrykowyts
Nov 11, 2026
Merged

mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-uspwrykowyts

Conversation

@mhuisi

@mhuisi mhuisi commented Nov 11, 2026

Copy link
Copy Markdown
Collaborator

No description provided.

On Windows, CI run 43085382097 failed in the `before all` hook of
"Project action commands > with a local git dependency": Lake's
`git fetch` of the local `dep` repository exited with an error and
wrote no output, so Lake reported only "failed to fetch the package
revision". The cause could not be found from the log.

`lake()` now runs Lake with `GIT_TRACE2` set to a new folder. Each git
process writes a trace2 log there: the command line, the child
processes and their exit codes, the `die()` messages and the exit
code. If Lake fails, the error contains these logs and the exit code
of Lake (with the NTSTATUS in hex on Windows) instead of a second copy
of stderr. A log without an `exit` line shows a git process that
stopped, and a missing log shows a process that did not start.

`withGitTrace(fn)` sets `GIT_TRACE2` in `process.env` for the time of
`fn`, so that the git calls that the extension starts through Lake
also write logs, and adds the logs to the error if `fn` fails. The two
`updateDependency` tests use it, because they run the same fetch.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@mhuisi
mhuisi merged commit f9b396a into leanprover:master Nov 11, 2026
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant