Relevance of "[n/m] Replayed […]" when doing `lake build`?

Stream: new members

[Isak Colboubrani]

When running lake build, I notice a significant number of [n/m] Replayed […] messages being printed.

I find these messages somewhat noisy, but I’m curious if they provide value for others.

In what specific scenarios are these messages worth paying attention to?

If they are rarely useful for the average end-user, would it make sense to suppress them by default and allow interested users to opt in?

Example output:

% git clone https://github.com/leanprover-community/mathematics_in_lean
% cd mathematics_in_lean/
% lake exe cache get
% lake build
% lake build | grep ' Replayed '
ℹ [2/2784] Replayed MIL.C01_Introduction.S01_Getting_Started
⚠ [2687/2784] Replayed MIL.C01_Introduction.S02_Overview
⚠ [2688/2784] Replayed MIL.C02_Basics.S01_Calculating
⚠ [2689/2784] Replayed MIL.C02_Basics.S02_Proving_Identities_in_Algebraic_Structures
⚠ [2690/2784] Replayed MIL.C02_Basics.S03_Using_Theorems_and_Lemmas
⚠ [2691/2784] Replayed MIL.C02_Basics.S04_More_on_Order_and_Divisibility
⚠ [2692/2784] Replayed MIL.C02_Basics.S05_Proving_Facts_about_Algebraic_Structures
⚠ [2693/2784] Replayed MIL.C03_Logic.S01_Implication_and_the_Universal_Quantifier
⚠ [2694/2784] Replayed MIL.C03_Logic.S02_The_Existential_Quantifier
⚠ [2695/2784] Replayed MIL.C03_Logic.S03_Negation
⚠ [2696/2784] Replayed MIL.C03_Logic.S04_Conjunction_and_Iff
⚠ [2697/2784] Replayed MIL.C03_Logic.S05_Disjunction
⚠ [2698/2784] Replayed MIL.C03_Logic.S06_Sequences_and_Convergence
⚠ [2699/2784] Replayed MIL.C04_Sets_and_Functions.S01_Sets
⚠ [2700/2784] Replayed MIL.C04_Sets_and_Functions.S02_Functions
⚠ [2701/2784] Replayed MIL.C04_Sets_and_Functions.S03_The_Schroeder_Bernstein_Theorem
⚠ [2702/2784] Replayed MIL.C05_Elementary_Number_Theory.S01_Irrational_Roots
⚠ [2703/2784] Replayed MIL.C05_Elementary_Number_Theory.S02_Induction_and_Recursion
⚠ [2704/2784] Replayed MIL.C05_Elementary_Number_Theory.S03_Infinitely_Many_Primes
⚠ [2705/2784] Replayed MIL.C06_Structures.S01_Structures
⚠ [2706/2784] Replayed MIL.C06_Structures.S02_Algebraic_Structures
⚠ [2707/2784] Replayed MIL.C06_Structures.S03_Building_the_Gaussian_Integers
⚠ [2708/2784] Replayed MIL.C07_Hierarchies.S01_Basics
⚠ [2709/2784] Replayed MIL.C07_Hierarchies.S02_Morphisms
⚠ [2710/2784] Replayed MIL.C07_Hierarchies.S03_Subobjects
⚠ [2718/2784] Replayed MIL.C08_Groups_and_Rings.S01_Groups
⚠ [2722/2784] Replayed MIL.C08_Groups_and_Rings.S02_Rings
ℹ [2727/2784] Replayed MIL.C09_Linear_Algebra.S01_Vector_Spaces
⚠ [2728/2784] Replayed MIL.C09_Linear_Algebra.S02_Subspaces
⚠ [2729/2784] Replayed MIL.C09_Linear_Algebra.S03_Endomorphisms
⚠ [2732/2784] Replayed MIL.C09_Linear_Algebra.S04_Bases
⚠ [2733/2784] Replayed MIL.C10_Topology.S01_Filters
⚠ [2736/2784] Replayed MIL.C10_Topology.S02_Metric_Spaces
⚠ [2737/2784] Replayed MIL.C10_Topology.S03_Topological_Spaces
⚠ [2744/2784] Replayed MIL.C11_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces
⚠ [2782/2784] Replayed MIL.C12_Integration_and_Measure_Theory.S03_Integration

[Ruben Van de Velde]

These are shown when there's output

[Ruben Van de Velde]

For example, if there's a sorry somewhere, this feature will make sure that a lake build will alert you to it. Otherwise, you'd have to rebuild everything from scratch to make sure you get all the relevant output

[Isak Colboubrani]

Consider the following example:

ℹ [2/2784] Replayed MIL.C01_Introduction.S01_Getting_Started
info: ././././MIL/C01_Introduction/S01_Getting_Started.lean:82:0: "Hello, World!"

It seems that [2/2784] Replayed MIL.C01_Introduction.S01_Getting_Started tells me that MIL/C01_Introduction/S01_Getting_Started.lean produced output. But doesn’t the next line already convey that information? :)

[Damiano Testa]

It also tells you that the oleans are still the old ones, since it was replayed, rather than built.

[Damiano Testa]

Also, if some files need to be rebuilt and others not, then knowing where you stand in the range already built/replayed vs all remaining files is potentially useful information.

[Damiano Testa]

I agree that there is redundancy and you may not need all the information every time, but it is certainly useful to have the information laid out clearly and then sift it as appropriate.

[Damiano Testa]

In fact, there is a very recent thread precisely about this: #lean4 > Silent sorry.

[Isak Colboubrani]

Would that use case be adequately addressed by providing a single-line summary (say info: Replayed cached output for <n> of <m> compiled files) at the end of lake build, rather than displaying a line for each compiled file that produces output?