[Merged by Bors] - chore: remove inlined lake-build-with-retry.sh from workflow, improve log messages

[bryangingechen]

To merge #27691, I had to inline a copy of lake-build-with-retry.sh into the workflow file (since the workflow always tries to run the master branch version of scripts, etc.). Now that that file exists in the master branch, we can remove this code.

I also improved the log messages for the step checking if the archive + counterexamples builds failed.

---

[github-actions]

PR summary f95517183c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success

[alreadydone]

A question maybe unrelated to this PR but people here probably know the answer: I don't know since when but currently the build logs are removed after builds are completed (even though you get rolling updates when building). In this run the "Check if building Archive or Counterexamples failed" step failed, but I can't see where it fails. Note that Mathlib build errors are replayed in the "lint mathlib" step, but Archive and Counterexamples build errors aren't replayed. Isn't it better to keep the Archive and Counterexamples build logs given the situation?