Corrupted olean

Stream: general

[Yaël Dillies]

#16281 is currently failing CI because file#order/imp has a corrupted olean. I tried merging master but that didn't fix anything. The file is absolutely fine in local. What do I do? :scream:

[Mauricio Collares]

Either bors r+ and hope for the best (which should be fine, because bors will squash and rebase your changes and the corrupted olean won't be used), or open a separate rebased PR. The corrupted olean was generated by nael, which is no longer in use, so this shouldn't happen again.

[Mauricio Collares]

Wait, I think 62047e97143e5f2a97ce33208df9f80b7f6e7266 doesn't build:

/home/collares/mathlib/src/data/finset/basic.lean:1252:67: error: type mismatch, term
  sup_sdiff_self_left
has type
  ∀ (a b : ?m_1), b \ a ⊔ a = b ⊔ a
but is expected to have type
  s \ t ∪ t = s ∪ t
/home/collares/mathlib/src/data/finset/basic.lean:1250:67: error: type mismatch, term
  sup_sdiff_self_right
has type
  ∀ (a b : ?m_1), a ⊔ b \ a = a ⊔ b
but is expected to have type
  s ∪ t \ s = s ∪ t

[Yaël Dillies]

Yeah, I'm expecting this kind of error, so the corrupted file is annoying...

[Mauricio Collares]

Next up:

/home/collares/mathlib/src/order/hom/basic.lean:811:0: error: (deterministic) timeout
/home/collares/mathlib/src/order/hom/basic.lean:806:0: error: (deterministic) timeout

This is order_iso.map_inf.

[Mauricio Collares]

@Yaël Dillies Please revert my commit after CI runs :) If it doesn't build after reverting, then I think you should just start another branch on top of current master.

Edit: Never mind, my previous approach was not as hacky as it should have been. I just added and removed a rm src/order/imp.olean build step to build.yml, so things should be working now.

[Eric Wieser]

Note that when CI fails, the second call of lean --make to try to fix bad oleans doesn't run