feat: lake: `.nobuild` trace file for debugging (#12076) This PR adds additional debugging information to a run of `lake build --no-build` via a `.nobuild` trace file. When a build fails due to needing a rebuild, Lake emits the new expected trace next as `.nobuild` file next to the build's old `.trace`. The inputs recorded in these files can then be compared to debug what caused the mismatch. To help keep the build directory clean, the `.nobuild` trace file is removed on the next successful build.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.