The output of `lake exe cache get` does not adhere to the "rule of silence"

[euprunin]

In Unix program design philosophy, the "rule of silence" holds that a program should remain quiet unless it has something unexpected to report:

"Rule of Silence: When a program has nothing surprising to say, it should say nothing."
[…]
"Well-designed programs treat the user's attention and concentration as a precious and limited resource, only to be claimed when necessary."

By contrast, lake exe cache get emits a flurry of messages even when there’s nothing new to convey:

% lake exe cache get
Current branch: master                             <-- could perhaps be helpful
Using cache from origin: github-username/mathlib4  <-- could perhaps be helpful
Attempting to download 5242 file(s) from leanprover-community/mathlib4 cache <-- could perhaps be helpful
Downloaded: 5242 file(s) [attempted 5242/5242 = 100%] (100% success) <-- could perhaps be helpful
No files to download                               <-- confusing since it seems to contradict the line above
Decompressing 6947 file(s)                         <-- nothing surprising
Unpacked in 4077 ms                                <-- nothing surprising
Completed successfully!                            <-- nothing surprising
% echo $?
0
% lake exe cache get
Current branch: master                             <-- could perhaps be helpful
Using cache from origin: github-username/mathlib4  <-- could perhaps be helpful
No files to download                               <-- nothing surprising
No files to download                               <-- nothing surprising
Decompressing 6947 file(s)                         <-- nothing surprising
Unpacked in 395 ms                                 <-- nothing surprising
Completed successfully!                            <-- nothing surprising
% echo $?
0

This verbosity could be reduced by suppressing routine progress updates and only displaying output when something noteworthy occurs.

[Rida-Hamadani]

lake exe cache get takes a lot of time and not having updates sounds frustrating to me. Also adding the success message was already a previous issue (#13276). I think it would be a better idea to have a --verbose or --silent version. (Personal preference towards the latter while keeping the current version as unflagged).

[euprunin]

@Rida-Hamadani It is the download step that takes a lot of time if I understand it correctly, and the output related to the download process are marked as "could perhaps be helpful" in the listing above. Thus, I think we’re in agreement about that assessment.

My suggestion is to hide the debug messages that follow when the user is no longer waiting for the downloading ("No files to download", "Decompressing 6947 file(s)", "Unpacked in 395 ms", and "Completed successfully!”).

[grunweg]

The unpacking step can also take a while. On a computer without an SSD, I've seen times of 10 seconds easily.

[euprunin]

@Rida-Hamadani @grunweg Good points. I've added a fix which takes into account your feedback in #27149.