shake going crazy

Stream: mathlib4

[Yaël Dillies]

Consider https://github.com/leanprover-community/mathlib4/pull/12974/commits/e7b3c20ab6cbb135599ce14f6e7a96744687bf5a. If you run lake exe shake, it prints

The following changes will be made automatically:
././././Mathlib/Algebra/BigOperators/Pi.lean:
  remove #[Mathlib.Algebra.GroupWithZero.Prod]
././././Mathlib/GroupTheory/Congruence.lean:
  remove #[Mathlib.Algebra.GroupWithZero.Prod]
  add #[Mathlib.Combinatorics.SimpleGraph.Basic]

then hangs (see https://github.com/leanprover-community/mathlib4/actions/runs/9125890114/job/25093012981?pr=12974, although the output is shown there. I got the output by running lake exe shake --fix locally).

[Yaël Dillies]

1. It's really surprising that shake hangs
2. The last line add #[Mathlib.Combinatorics.SimpleGraph.Basic] is definitely wrong since simple graphs are not even imported in GroupTheory.Congruence

[Yaël Dillies]

Consider #12964. I know shake can technically be non-idempotent on correct grounds (an import is needed only because TC search went along a non-optimal path, removing an earlier makes TC search suddenly use a more optimal path), however I suspect that's not the case here because the first shake commit did not change files upstream of the files touched by the second shake commit.

[Yaël Dillies]

cc @Mario Carneiro