section name mismatch

Stream: lean4

[Yury G. Kudryashov]

Hi, when I'm trying to close a section/namespace with wrong name, the error message says "invalid end, name mismatch" but doesn't tell me what are the conflicting names.

[Kevin Buzzard]

On the other hand you have the breadcrumbs at the top telling you this

[Yury G. Kudryashov]

Not in case of an unnamed section (at least in Emacs).

[Yury G. Kudryashov]

In my case, it was noncomputable section inserted by mathport.

[Mario Carneiro]

it should say <section> for an unnamed section

[Yury G. Kudryashov]

IMHO, error messages should be informative without an editor session.

[Yury G. Kudryashov]

At least, if it's easy to make them informative.

[Mario Carneiro]

Apparently there is a CompletionInfo.endSection which would in theory give you a ctrl-space completion support, but it does not seem to be implemented

[Mario Carneiro]

lean4#2255

[David Thrane Christiansen]

While interactive editors are great, I agree with @Yury G. Kudryashov - error messages occur in many other contexts, such as CI systems, where the reader needs to reconstruct context in their heads. Of course there's a balance between distracting verbosity and useful information, but "I expected a thing, but I won't tell you what it is" seems to err on the side of too little information to me.