Very confusing error message

Stream: new members

[Dan Abramov]

Can you find the actual error in this sea of noise?

Screenshot 2025-08-24 at 23.40.52.png

(Hint: there is only one line of this log that's the actual cause of the problem)

I know where to look for it now but it mystified me for a while.

Is it worth filing an issue? If yes, in which repo? At which seam is the fault?

[Matt Diamond]

huh, I was going to say there are 2 unsolved goals but you're saying there's only one relevant line?

[Dan Abramov]

Yup, the actual error is caused by something else.

[Dan Abramov]

Well, actually you are correct, however these goals aren't from the current file.

[Dan Abramov]

Basically, my problem with this is that it is easy to assume that the fault is in the file I'm working on (which is Section_3_6.lean, however it's actually in one of the dependencies (Section_3_5.lean) . I didn't even realize what these goals refer to unless you pointed them out. This is in a sense "user error" (I didn't correlate the logs to my files) but it is very disorienting because usually InfoView tells me information about what I'm looking at now. I never expect it to contain log spew from other files.

[Dan Abramov]

The other problem is that the not-actually-fatal errors obscure the problem that did cause the build to fail.