shake spurious failure

Stream: mathlib4

[Artie Khovanov]

In #20818, shake tells me to remove an import, but removing that import breaks the file. What can I do to fix the CI?

[Bolton Bailey]

You can use the --update flag

[Bolton Bailey]

From lake exe shake --help:

  --update
    Assume that all issues we find are false positives and update the config
    file to include them.

[Bolton Bailey]

I find shake pretty frequently breaks my build, which ideally it would not do :shrug:. If shake was doing multiple things, you can also try reinserting the import and rerunning shake, sometimes I think when shake makes multiple changes they step on each other's toes.

[Ruben Van de Velde]

Breaks it how?

[Bolton Bailey]

Ruben Van de Velde said:

Breaks it how?

Not sure what you're asking - I will often run lake exe shake --fix and I will find that when I build again, files are not importing things they need to import, leading to errors about how things were not found.

For example here is an error I experienced today when trying to split, happy to get insights:

> lake build ; lake exe shake --fix ; lake build
Build completed successfully.
The following changes will be made automatically:
././././Mathlib/Data/List/TakeDrop.lean:
  remove #[Mathlib.Data.List.Basic]
  add #[Mathlib.Order.Basic, Mathlib.Data.Nat.Defs, Mathlib.Data.List.Defs]
  instead
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Forall2
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Lattice
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Perm.Subperm
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Infix
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Flatten
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Lex
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.MinMax
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.InsertIdx
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Palindrome
    import [Mathlib.Data.List.Basic] in Mathlib.Data.Stream.Init
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.DropRight
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Enum
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.Indexes
    import [Mathlib.Data.List.Basic] in Mathlib.Data.List.ReduceOption
././././Mathlib/Data/List/Forall2.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
  instead
    import [Mathlib.Data.List.TakeDrop] in Mathlib.Data.List.Nodup
././././Mathlib/Data/List/Lattice.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/Perm/Subperm.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/Flatten.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/Lex.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/ProdSigma.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Defs]
././././Mathlib/Data/List/MinMax.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/InsertIdx.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/Palindrome.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/Stream/Init.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/Enum.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/Indexes.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
././././Mathlib/Data/List/ReduceOption.lean:
  remove #[Mathlib.Data.List.TakeDrop]
  add #[Mathlib.Data.List.Basic]
Successfully applied 17 suggestions.
✖ [1627/5991] Building Mathlib.Data.List.ProdSigma
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH= /Users/boltonbailey/.elan/toolchains/leanprover--lean4---v4.16.0-rc2/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -Dweak.linter.docPrime=false -Dweak.linter.hashCommand=true -Dweak.linter.oldObtain=true -Dweak.linter.refine=true -Dweak.linter.style.cdot=true -Dweak.linter.style.dollarSyntax=true -Dweak.linter.style.header=true -Dweak.linter.style.lambdaSyntax=true -Dweak.linter.style.longLine=true -Dweak.linter.style.longFile=1500 -Dweak.linter.style.missingEnd=true -Dweak.linter.style.multiGoal=true -Dweak.linter.style.setOption=true ././././Mathlib/Data/List/ProdSigma.lean -R ./././. -o ././.lake/build/lib/Mathlib/Data/List/ProdSigma.olean -i ././.lake/build/lib/Mathlib/Data/List/ProdSigma.ilean -c ././.lake/build/ir/Mathlib/Data/List/ProdSigma.c --json
error: ././././Mathlib/Data/List/ProdSigma.lean:48:3: unknown tactic
error: ././././Mathlib/Data/List/ProdSigma.lean:47:49: unsolved goals
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length
error: ././././Mathlib/Data/List/ProdSigma.lean:83:3: unknown tactic
error: ././././Mathlib/Data/List/ProdSigma.lean:82:69: unsolved goals
α : Type u_1
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (l₁.sigma l₂).length = Nat.sum (map (fun a ↦ (l₂ a).length) l₁)
error: ././././Mathlib/Data/List/ProdSigma.lean:92:3: unknown tactic
error: ././././Mathlib/Data/List/ProdSigma.lean:91:47: unsolved goals
α : Type u_1
β : Type u_2
x : α
y : β
xs : List (α × β)
⊢ (y, x) ∈ map Prod.swap xs ↔ (x, y) ∈ xs
error: Lean exited with code 1

[Ruben Van de Velde]

Oh, this is because shake doesn't know what tactics are used, so ProdSigma just needs a Mathlib.Tactic.Cases import for induction'

[Bolton Bailey]

Ok great, making this work automatically sounds like a good candidate for an issue/PR to the Shake tool.

[Bolton Bailey]

Not to be too ungrateful to the people who brought us this software, but I have another complaint about shake evinced by this terminal output:

~/Desktop/mathlibcontribution/mathlib4 master !13 ?1 ...................................... INT 30s 08:49:16
> lake build Mathlib.Algebra.Algebra.Subalgebra.Rank
Build completed successfully.                                                                           /0.4s

~/Desktop/mathlibcontribution/mathlib4 master !13 ?1 .............................................. 08:49:21
> lake exe shake Mathlib.Algebra.Algebra.Subalgebra.Rank
There are out of date oleans. Run `lake build` or `lake exe cache get` first                            /1.2s

Seems to me that it shouldn't be too hard for shake to succeed on a particular module if that module has been built, but for whatever reason, that was not happening for me.

[Ruben Van de Velde]

I think in that case it's impossible to do the interesting half of what shake does - fix the imports in files that import Mathlib.Algebra.Algebra.Subalgebra.Rank; just fixing the imports in that file can be done (manually) with #min_imports

[Bolton Bailey]

Then why is there an option for it?

[Ruben Van de Velde]

I don't know

[Bolton Bailey]

Ah, perhaps I am misunderstanding. Maybe the point is that it shakes not on everything below, but on everything above or everything above and below the provided module, but not unrelated files?

[Bolton Bailey]

Arguments:
  <MODULE>
    A module path like `Mathlib`. All files transitively reachable from the
    provided module(s) will be checked.

[Bolton Bailey]

What would perhaps be most ideal is to be able to shake on just those things <4 or so hops away from the file in question, so that I don't have to spend 20 minutes rebuilding the library multiple times per PR.

[Artie Khovanov]

I'm not sure how to do what is being suggested given that I can't build all of Mathlib locally on my laptop. It's the central CI that's failing.

[Kim Morrison]

@Artie Khovanov, after CI fails because of shake, you can then run lake exe cache get locally, followed by lake exe shake --fix or lake exe shake --update.