feature request: Save `lake build` and `lake test` logs for downstream workflow steps

[Seasawher]

Hi, thank you for maintaining this action.
I'm the maintainer of the lean-update action.

Motivation

leanprover/lean-action runs lake build and lake test internally, but their output logs are currently only visible in the GitHub Actions job log.

This makes it difficult for later workflow steps or follow-up actions to inspect and reuse the exact build/test output. For example, in workflows using lean-update, we would like to collect the lake build / lake test logs and post or process them after lean-action has run.

At the moment, the only practical workaround is to run lake build and/or lake test again from lean-update just to capture the logs. That has a few downsides:

• it duplicates work and makes CI slower
• it can produce output that differs from the original failure
• it complicates workflows that want to summarize or report Lean build/test failures

Requested feature

Would it be possible for lean-action to save the output of lake build and lake test to files that later workflow steps can access?

Use case

This would help tools such as lean-update, which need to report or process Lean build/test results after lean-action has already run. If lean-action saved the original logs, lean-update would no longer need to rerun lake build or lake test just to obtain them.

Thanks for reading this.