CI failure in import-graph

Stream: mathlib4

[Kim Morrison]

@Jon Eugster @Paul Lezeau, just a heads up that "feat: add #import_diff command #73" https://github.com/leanprover-community/import-graph/pull/73 seems to have introduced a failure in CI (perhaps intermittent)?

See https://github.com/leanprover-community/import-graph/actions/runs/17717638873/job/50344747854?pr=81.

This hit me when trying to upgrade the toolchain today.

[Kim Morrison]

This is non-deterministic, and whether we see an error depends on lake's choice of build order, which we can't rely on.

[Kim Morrison]

As I'm in the middle of a release process, I don't have time to stop to fix this, so I am deleting the two files that cause the non-determinism, and asking if you two can arrange fixing this after the fact? Thank you. :-)

[Paul Lezeau]

Sure! I’ll take a look at this tomorrow:)

[Jon Eugster]

Thanks for spotting Kim! Do I see this correctly that there is no CI running on PRs to that repo? I'll have a look and fix CI if required to avoid this in the future

[Jon Eugster]

import-graph#83 should fix this by removing any non-determinism and (hopefully?) fixing CI to run on all PRs. @Paul Lezeau I've also sorted the outputs of the command alphabetically

[Paul Lezeau]

Oh nice! Thanks!