feat(CI): add summary of benchmarking output

[adomani]

Add a GitHub action triggered on the !bench comments.

Reports a summary of the changes by at least 10^9 instructions. This PR contains various examples of reports generated by this script.

Zulip

---

[github-actions]

PR summary e27dfa7992

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Bench
+ addBenchSummaryComment
+ benchOutput
+ formatDiff
+ formatFile
+ formatPercent
+ intDecs
+ summary
+ toCollapsibleTable
+ toTable

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.

[grunweg]

Thanks for writing this and slowly automating Michael Stoll's manual comments! This looks very useful!

I took a look up to line 100 of bench_summary. Here's my usual bunch of persnickety comments.

[adomani]

Michael, thank you for the review: I implemented all your comments!

[grunweg]

I randomly stumbled across this PR. I still find it useful, so left a few tweaks and a review. Enjoy! I pushed a commit with some changes directly. Please revert any you disagree with (or let's discuss)!
In any case: the current summary is much better than none --- I can happily postpone many comments to a follow-up!

I also wondered if the output can be clarified slightly, by printing the range of instructions for each collapsible table. WDYT?

[grunweg]

One of my first thoughts was: "surely this can be rewritten as a script, callable via lake exe, right"? Right now, the answer is no (because the script uses IO.Log, which requires a stronger monad than just IO) --- but this is just for debugging, right? (You could sneakily use dbg_trace, I presume...?)

Put differently: the current set-up is clever, but I wonder if something more standard is possible.

[grunweg]

I'll happily push a commit rewriting this as a script, if you think that is good.

[adomani]

A script would be nice, but maybe I would wait to see if there is interest in actually running this script outside of CI. Btw, using IO.print/IO.println may be better than dbg_trace, assuming that they are in the right monad.

[grunweg]

Good point. I was thinking about this mainly from a maintainance point of view: adding a script is well-understood - but this can easily be a follow-up.

Sure, IO.println would work (you just need an output file...).

[adomani]

Michael, thank you so much for reviewing this further!

You labelled the PR as awaiting-author, but... what is left for me to do? 😄

[adomani]

A script would be nice, but maybe I would wait to see if there is interest in actually running this script outside of CI. Btw, using IO.print/IO.println may be better than dbg_trace, assuming that they are in the right monad.

[grunweg]

The main thing was to agree if these changes are acceptable to you as well. I've pushed a tiny tweak, and am happy with this PR. (There are several directions for extending it, but none of these need to happen in this PR.) Thanks for writing it!
maintainer merge

[grunweg]

Good point. I was thinking about this mainly from a maintainance point of view: adding a script is well-understood - but this can easily be a follow-up.

Sure, IO.println would work (you just need an output file...).

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.