Segfault building Mathlib4

Stream: general

[Julian Berman]

Attempting to build Mathlib4 (commit 6668fecbb) seems to segfault for me here on macOS. Can anyone reproduce? Specifically, it segfaults reliably when building [336/856] Building Mathlib.Tactic.Tauto -- trying to grab a backtrace and/or remember how to skip that and see if it segfaults anywhere else.

[Julian Berman]

(OT: what is that new "speaker"-y icon in Zulip that appears just next to the thread name in the sidebar? Do just I see that, or is it there for others?) EDIT: Oh I see, hovering over the three dots says it means "Follow" and is probably because I created the thread. Presumably some Zulip update has tweaked the UI there, never mind this bit.

[David Renshaw]

seems to work fine for me at that commit. Maybe you have some local state that needs to be clobbered?

[Kyle Miller]

I just did a clean build on an M2 mac, and lake build Mathlib.Tactic.Tauto worked fine

[Julian Berman]

Hrm, ok, will blow away the build directory and see, thanks both.

[Julian Berman]

OK yes after removing build/ and lake-packages it seems to be progressing...

[Sebastian Ullrich]

Please, when you find these kinds of issues, make a copy of the project directory first so we actually have a chance to fix them :)

[Julian Berman]

@Sebastian Ullrich that was mostly why I asked in the first place! Good to know, I'll be sure to do so next time.