CI does not know tactic move_add/mul

Stream: mathlib4

[Ralf Stephan]

In #14895, I use the tactic move_mul. CI does not recognize it, build failing. But when I add import Mathlib.Tactic.MoveAdd the build fails because of superfluous import. What to do?

[Yaël Dillies]

Run lake exe shake --update after "the build has failed because of superfluous import"

[Ralf Stephan]

OK lake build again, with only 700 files untouched. And that was after a successful lake exe cache get. Mathlib is moving so fast. Never seen something like that.

[Ralf Stephan]

Or it's too dense, not modular enough...

[Michael Rothgang]

Ralf Stephan said:

Or it's too dense, not modular enough...

I think it's both (and people are actively working on untangling the import thicket --- this is the sort of thing which grows organically unless you actively make an effort to prevent it).