De-emphasizing inaccessible hypothesis names

Stream: lean4

[Sebastian Ullrich]

Quite some time ago I implemented a simple client-side filter in Emacs for inaccessible hypotheses
image.png
AFAIR, @Marc Huisinga implemented it in vscode-lean4 at the same time, but because of some bug it was never actually triggered? In any case, now that the implementation has changed completely anyway through widgets, I wanted to gauge interest for finally bringing this feature to VS Code/the infoview widget

[Sebastian Ullrich]

If eliding the cross symbol is too controversial, I think highlighting without elision would still be valuable. At least in HTML we would be able to add the symbol when copying text without displaying it, I assume.

[Sebastian Ullrich]

Apparently I'd already complained previously: https://github.com/leanprover/vscode-lean4/issues/18. But the problem wasn't really the cross elision (which I think is fixable as mentioned) but the lackluster/unclear highlighting compared to Emacs (where nobody has complained about the elision so far, afair). And then the code was lost completely in https://github.com/leanprover/vscode-lean4/pull/37.

[Julian Berman]

When you say filter you mean the dimming right? Not that the hypotheses are totally removed from the shown state?

[Julian Berman]

Just trying to make sure I understand the screenshot.

[Sebastian Ullrich]

Yes, more of an Instagram filter than a list filter

[Sebastian Ullrich]

For completeness, Leo has also since implemented a server-side filter that completely hides the names (but not types) of inaccessible variables of proposition type

[Julian Berman]

Perhaps, regardless of how they're indicated / differentiated, it'd be helpful to have a hover message that explains what they are? E.g. hovering shows something like "n✝ is an inaccessible hypothesis because its name was automatically generated by ..."? Otherwise it'd seem hard to guess why the highlighting is different, and hard even to ask about if the color was different between users.

[Sebastian Ullrich]

Heh, that would require some novel metadata. But at least a static message would be very reasonable, yes. Which really is true for crossed names even without highlighting.

[Julian Berman]

Yeah I suppose didn't mean to mix 2 ideas in one, even just a static message I think makes it easier to muck with how they display.

[Gabriel Ebner]

I strongly disagree with hiding the crosses, so it is intentional that I never implemented it.

[Gabriel Ebner]

The crosses are an essential part of how name resolution works in Lean 4. Users will see them in error messages and on Zulip, so they'll need to know what they signify anyhow. Having two different ways to communicate the same information is just unnecessarily confusing.

[Sebastian Ullrich]

@Gabriel Ebner What about the highlighting (or rather low-lighting) then? The specific displayed name doesn't matter all that much anymore anyway if it is deemphasized to such a degree as in Emacs

[Gabriel Ebner]

Personally I don't see the point of graying them out, but it is a compromise I could live with.

[Sebastian Ullrich]

I guess the good thing with HTML is that we also have plenty of other options :silence: image.png

[Mario Carneiro]

One thing to consider re: "the names aren't important" is that these names will appear in the types of hypotheses, so it's important to know which is which

[Sebastian Ullrich]

Right, I should mention that the Emacs filter also applies to references of these names (as did the original VS Code implementation, I think). But I'm completely on board with not touching the names and willing to change that in Emacs as well.

[Mario Carneiro]

so I agree with gabriel that we shouldn't be doing anything other than putting the dagger on and maybe styling them differently (in a way that indicates that they are different but does not make them harder to see)

[Sebastian Ullrich]

PR'ed https://github.com/leanprover/vscode-lean4/pull/249