Zulip Chat Archive

Stream: lean4

Topic: De-emphasizing inaccessible hypothesis names


Sebastian Ullrich (Aug 28 2022 at 12:05):

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 (Aug 28 2022 at 12:06):

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 (Aug 28 2022 at 12:26):

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 (Aug 28 2022 at 12:31):

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

Julian Berman (Aug 28 2022 at 12:31):

Just trying to make sure I understand the screenshot.

Sebastian Ullrich (Aug 28 2022 at 12:33):

Yes, more of an Instagram filter than a list filter

Sebastian Ullrich (Aug 28 2022 at 12:34):

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 (Aug 28 2022 at 12:45):

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 (Aug 28 2022 at 12:47):

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 (Aug 28 2022 at 12:48):

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 (Aug 28 2022 at 12:55):

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

Gabriel Ebner (Aug 28 2022 at 13:01):

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 (Aug 28 2022 at 13:03):

@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 (Aug 28 2022 at 13:04):

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

Sebastian Ullrich (Aug 28 2022 at 13:19):

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

Mario Carneiro (Aug 28 2022 at 13:23):

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 (Aug 28 2022 at 13:25):

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 (Aug 28 2022 at 13:25):

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 (Aug 30 2022 at 11:40):

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


Last updated: Dec 20 2023 at 11:08 UTC