Strange CI error: "unknown identifier #0"

Stream: mathlib4

[Michael Rothgang]

I get a CI error in #26221 that I cannot explain. This error happens both in mathlib CI (example log) and when building locally. It takes the form of 12 warnings on line 2, column 2 of the last file: unknown identifier '#0' --- so on the first meaningful line of the copyright header. Except that the copyright header looks perfectly fine.

Does any of the experts here have any idea what is going on, or how to debug this further? (Whatever the actual cause of the error is, the error message is terrible because it does not help me debug this, at all.)

[Matthew Ballard]

I don't think that is an o...

[Matthew Ballard]

Nevermind rhs_aux_addZ has an issue. What is MDiff?

[Michael Rothgang]

MDiff is a custom elaborator (defined in Mathlib.Geometry.Manifold.Elaborators).

[Michael Rothgang]

See this zulip thread for details.

[Matthew Ballard]

That is the source of the error.

[Michael Rothgang]

Ah, I found the bug. I needed some more syntax soup to make it work. Thanks a lot!

[Notification Bot]

Michael Rothgang has marked this topic as resolved.

[Damiano Testa]

I think that I've seen unknown identifier #0 appear when there is an expression with a non-bound variable in it.

[Notification Bot]

Michael Rothgang has marked this topic as unresolved.

[Michael Rothgang]

Can we get a better error message for this, though?

[Notification Bot]

Michael Rothgang has marked this topic as unresolved.

[Aaron Liu]

Usually I see unexpected bound variable #0 when that happens so I don't know where this error is coming from.

[Patrick Massot]

The experimental geometry elaborators definitely need better error reporting. They very probably need withRef stuff. Otherwise Lean doesn’t know where to report errors.