lake: dump link-args response file on link failure

When a Lake-driven link step fails, the user sees ld's diagnostic but not the response-file contents that produced it. The link is invoked as cc -o foo.so @foo.so.rsp (or .exe.rsp); the rsp body — every -L, -l, --whole-archive, absolute archive path, and the order they appear in — is the actual command the linker consumed, and it is the smallest thing that explains the failure.

Today reconstructing the rsp requires the user to know rsp files exist, know where Lake writes them (e.g. <pkg>/.lake/build/lib/libfoo.so.rsp, <pkg>/.lake/build/bin/foo.exe.rsp), remember to cat the file in CI before the post-failure cleanup wipes it, and then take another CI roundtrip to get the output. None of that is information Lake doesn't already have at the moment of failure.

We hit this four times this past week debugging Linux/Windows link breakage on https://github.com/leanprover/lp and https://github.com/leanprover/soplex-ffi (issue tracking https://github.com/leanprover/lp/issues/170 + the in-elaborator GMP interposition crash + a Lake -K config-propagation gap). Every iteration burned a CI roundtrip to learn what was in the rsp.

Proposal

A new opt-in surface, behind a flag and an env var:

• lake build --print-link-args ...
• LAKE_PRINT_LINK_ARGS=1

When enabled, on link failure Lake emits one structured log entry per failed link with the target name, the rsp file path, and the rsp body. On success the dump is suppressed unless -v is also passed. The unconditional default stays as today (rsp path is not printed at all) because precompiled-module exes can produce thousands of args and dumping them by default would bury the linker diagnostic.

Reasonable variants if the full body is judged too noisy even behind a flag: a capped dump (head/tail N lines with a ...truncated... marker), or print only the rsp path on failure plus a one-line "rerun with `--print-link-args` to dump" hint.

Where it plugs in

Lake's proc infrastructure already captures the failing link command's stderr and emits it as a log entry; the same emission point can read the rsp file and append it to the entry. The link sites in Lake/Build/Common.lean (buildLeanSharedLib, buildLeanExe) compose the rsp path and pass it to compileSharedLib / compileExe, so the path is already in scope at the failure site.

Out of scope

A larger lake build --explain <target> mode that reports the computed link inputs, transitive extern_lib artifacts, moreLinkArgs stack, and toolchain-prefix discovery would be very useful but is meaningfully bigger design work. This issue is the minimum useful slice: dump the file Lake already wrote.

🤖 Prepared with Claude Code

Start in Lake/Build/Common.lean at buildLeanSharedLib and buildLeanExe, then follow compileSharedLib/compileExe into Lake's proc failure-log emission. Trace how the rsp path and link stderr are available at failure time. Done means the opt-in flag and LAKE_PRINT_LINK_ARGS behavior produce one structured failed-link entry with the target, rsp path, and body while preserving the described success and default behavior.