What's in a sanitized `Name`?

Stream: lean4 dev

[Wojciech Nawrocki]

I discovered something that could use clarification while debugging an issue that blew up the new calc widget. I went into it expecting Names to always faithfully represent internal data, in particular that a name with macro scopes would have a form such as `foo._@.Module._hyg.1, and that tombstones would only appear in types that represent pretty-printed output such as as String or Format. However, that is not what happens. We have sanitizeNames which rewrites the userName field of local hypotheses to be Name.str .anonymous "blah✝".

Then in the server code, we put these into names : Array Name here. This works fine for displaying in the infoview, but if we try to deserialize an InteractiveHypothesisBundle inside an RPC method for widget purposes, the FromJson Name instance blows up in String.toName.

I think my preferred solution is to, rather than 'fix' String.toName to accept these names with tombstones, stop pretending that they are actual Names and re-type InteractiveHypothesisBundle : Array String. This should be a backwards-compatible change as the JSON representation is a string in either case. But I am posting here in case the dev team has other feedback. Is a PR welcome?

[Sebastian Ullrich]

Sounds good to me!