Segfault after updating to v4.22.0-rc3

Stream: general

[Vlad]

After updating Lean from v4.21.0-rc3 to v4.22.0-rc3, our project's executable immediately segfaults when run. We reduced the issue to a minimal example:

import Mathlib.Order.Disjoint

-- Copied from Mathlib.Order.PropInstances
instance Prop.instBoundedOrder : BoundedOrder Prop where
  top := True
  le_top _ _ := True.intro
  bot := False
  bot_le := @False.elim

def main : IO Unit := do
  IO.println "ok"

This example works in v4.21.0-rc3 but segfaults in v4.22.0-rc3 without output. However, commenting out the Prop.instBoundedOrder instance prevents the crash.

We are actively investigating this and would welcome suggestions on where to look. Could this be related to our configuration, or might it indicate a regression in v4.22?

OS: Windows 10
Lake: 5.0.0-src+7c3ca70
Mathlib: ab35957594546b036883f7a882015d6fa2d650bf

[Yaël Dillies]

See #mathlib4 > `import Mathlib.Order.PropInstances` causing segment fault

[Mauricio Collares]

There are other threads about it, but the summary is that this is fixed by lean4#9310, which will be backported to the 4.22 branch

[Kim Morrison]

This is fixed on v4.22.0-rc4 now.