Adding an import breaks `simp only`

Stream: general

[Eric Wieser]

I'm getting something pretty scary in #7163. My change ends up breaking docs#finset.ndunion_le, presumably due to order.directed being imported in places it previously was not a slightly different order to before.

However, what really worries me is that the lemma is still broken even if I replace simp with simp only [...]:

-- works before the PR, breaks on the `simp only` with the PR.
theorem ndunion_le {s t u : multiset α} : ndunion s t ≤ u ↔ s ⊆ u ∧ t ≤ u :=
multiset.induction_on s (by simp)
  (by simp only [ndinsert_le, and_comm, and.left_comm, iff_self,
    forall_2_true_iff, implies_true_iff, cons_ndunion, cons_subset] {contextual := tt})

What else could be causing this action at a distance?

[Eric Wieser]

My only guess so far is that I'm running into a hash collision in olean files again, and the error isn't "real", but only because I have no other ideas

[Bhavik Mehta]

Eric Wieser said:

My only guess so far is that I'm running into a hash collision in olean files again, and the error isn't "real", but only because I have no other ideas

Does leanproject clean && leanproject build help with this?

[Eric Wieser]

Probably, but then my CPU will be monopolized by lean for an hour or so!

[Eric Wieser]

I tried making a #mwe of this: adding the new imports alone as in https://github.com/leanprover-community/mathlib/compare/eric-wieser/directed-import-debug result in the error "definition docs#setoid.gi is noncomputable, it depends on docs#Prop.linear_order"

[Eric Wieser]

It seems like when searching for preorder Prop, it's by coincidence that it currently finds docs#complete_lattice_Prop before docs#Prop.linear_order, the latter of which is non-computable