executable has no output after adding import

Stream: general

[Christian Merten]

While playing around with verso, I stumbled upon the following: After importing Mathlib, an executable (called via lake exe) stopped producing output.

I did not manage to make it mathlib-free, but here is how to reproduce:

1. lake new bar math
2. cd bar; lake update
3. Add one executable target to lakefile.toml:

[[lean_exe]]
name = "foo"
root = "Main"

4. Add Main.lean with

import Mathlib.Order.PropInstances

def main := IO.println "hi"

5. Run lake exe foo.

Output: Nothing, no error message and no "hi". If the mathlib import is removed, the expected output appears.
(One can certainly minimize further by inlining code from the imports).

[Eric Wieser]

What does echo $? give?

[Christian Merten]

139, so segmentation fault I assume?

[Eric Wieser]

This is already reported elsewhere

[Eric Wieser]

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

[Christian Merten]

Thanks!