Show failing file at the end

[gebner]

When you have a file with lots of errors, the output of lake build ends in the following:

⊢ (x✝¹ * x✝).val = (x✝ * x✝¹).val

error: external command /home/gebner/.elan/toolchains/leanprover--lean4---nightly-2021-11-26/bin/lean exited with status 1
error: build failed

It would be great if lake could tell me which file failed to build (e.g. by showing the arguments to the failing command).

[tydeu]

@gebner I'm sorry, but I am not sure what you mean. Lake does log the executed lean command and its stout and stderr. Are you not seeing that? Or is there something else that you want to see?

[gebner]

Lake does log the executed lean command and its stout and stderr. Are you not seeing that?

Yes, it does indeed log the executed lean command. But only above the error messages, and it's hard to find when there's lots of error messages.

I would prefer something like this:

error: external command LEAN_PATH=./build/lib:./lean_packages/mathlib/./build/lib /home/gebner/.elan/toolchains/leanprover--lean4---nightly-2021-11-28/bin/lean -R ./. -o ./build/lib/Mathport/Syntax/Translate.olean -c ./build/ir/Mathport/Syntax/Translate.c ././Mathport/Syntax/Translate.lean exited with status 1

or if that's too long, just showing the target would be helpful:

error: failed to build ./build/lib/Mathport/Syntax/Translate.olean

[Kha]

For more complex/customized builds, might also be interesting to show the full trace back to suggest why this target was built at all

error: builder for '/nix/store/ahc0n8cdjff6vk22c5kl1nwc0gx7raih-Init.Prelude.drv' failed with exit code 1;
       last 1 log lines:
       > Init/Prelude.lean:2271:0: error: expected command
       For full logs, run 'nix log /nix/store/ahc0n8cdjff6vk22c5kl1nwc0gx7raih-Init.Prelude.drv'.
error: 1 dependencies of derivation '/nix/store/dbaca8ik9qx5xkjg2pq25ayrinfv2spb-Init-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/m3s645k62xqivrc3d7xmgj0qkdz68cq3-Init.Core-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/vsj5z7i996d7jspkflskvh8bsr0xq3jx-Init.Notation-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/7wrdblphw9lkhqjm021nkc92nahc2yfa-Init.Prelude-cc.drv' failed to build
error: 1 dependencies of derivation '/nix/store/xvm635m0q38pqmxh3plh8my6mlqfxg5d-Init-lib.drv' failed to build
error: 1 dependencies of derivation '/nix/store/s8bkci641k1gnadk9lvnbn5l7k4a5jl3-Lean-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/zx0qpj46b9dqn8kzhs4iqfx4mmnj5jly-Lean.Attributes-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/zg0wlddz8x5fzbbdnrskzi77rzprp67f-Lean.AuxRecursor-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/fhwbrkz1hb5lidzhv4b5wmrrwdvsfb5h-Lean.Class-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/lsddwbr4xid0zd0i61xa7dnr4nw66l5a-Lean.Compiler-depRoot.drv' failed to build
...

[tydeu]

Okay, makes sense. I will put this on my todo list. Currently, no information is kept about the failing build task, so doing either of these will require some major refactoring. l will keep in mind going forward and integrated it into Lake when I can.