Segfaults in CI are a pass?

Stream: general

[Eric Wieser]

I just made #12568, which segfaults for me every time in gitpod. However, github reports that it built everything downstream of file#algebra/order/monoid in just 16s!

I assume what actually happened is that the build segfaulted in CI too, but CI considered that a pass?

[Eric Wieser]

Ah, seems only the build step swallowed the error, lint and tests segfault too and report it

[Eric Wieser]

Here's a #mwe for the segfault:

import algebra.group.with_one

-- segfault without this line
-- attribute [semireducible] with_zero

def segfault_please : with_zero ℕ → ℕ
| 0 := 0
| (n : ℕ) := n

[Gabriel Ebner]

:scream:

[Gabriel Ebner]

Ah, seems only the build step swallowed the error, lint and tests segfault too and report it

Is this because we don't set pipefail in ci?

[Gabriel Ebner]

lean#695