indentation in traces

Stream: general

[Kevin Buzzard]

When traces are too large they are sometimes truncated with a message [] 86 more entries... ▶ which, when unfolded, introduces an extra layer of indentation. Is this expected? It always confuses me.

Example:

                [] [61958.000000] ✅️ apply @IsScalarTower.right to IsScalarTower R S S ▶
                [isDefEq] [26489.000000] ✅️ ?m.156 =?= IsScalarTower.right ▶
                [resume] [332.000000] propagating IsScalarTower R S S to subgoal IsScalarTower R S S of SMulCommClass R S S ▶
                [isDefEq] [26398.000000] ✅️ ?m.151 =?= Localization.instSMulCommClassOfIsScalarTower ▶
                [resume] [221.000000] propagating SMulCommClass R S S to subgoal SMulCommClass R S S of SMul S (S ⊗[R] S) ▶
                [] 86 more entries... ▼
                  [isDefEq] [968.000000] ✅️ ?m.136 =?= TensorProduct.leftHasSMul ▶
                  [resume] [1810.000000] propagating SMul S
                        (S ⊗[R]
                          S) to subgoal SMul S
                        (S ⊗[R] S) of Module S (↥(KaehlerDifferential.ideal R S) ⧸ KaehlerDifferential.ideal R S • ⊤) ▶
                  [] [1133.000000] ❌️ apply inst✝¹ to Module S ↥(KaehlerDifferential.ideal R S) ▶

The indentation jumps two spaces to the right. 50 lines further down I get [] 36 more entries... ▶ and then if I unfold that I jump two more. I assume the idea is "it's a triangle, so when you click on it you get two new spaces". Usually I find myself in the situation where I just want to see all the entries because it's never more than a few hundred in my experience, and I think that seeing them all would be less confusing than seeing the indentation. Can I either turn off extra indentation or set some setting so that I see more than 50 trace outputs in a row?

[Sebastian Ullrich]

Kevin Buzzard said:

set some setting so that I see more than 50 trace outputs in a row

Yes, this is the maxTraceChildren option