Commit 2024-11-07 21:30 97f7ee9b

fix: percentages in bench report (#18732) Fixes a bug reported on Zulip. The script would print percentages in the form x.y%, where y should have consisted of two digits. However, when y was in the range 0..9, it would not add a leading 0. The rest of the PR takes care of

• updating deprecated declarations and structure format;
• adding command-line analogues of the lean script for easier step-by-step debugging;
• add some comments.