recursive hovers on the web editor

Stream: general

[Jovan Gerbscheid]

When I use the web editor (live.lean-lang.org), I can't (recursively) hover over terms in the infoview which is quite annoying. Is it possible to fix this?

I also can't crtl+click on terms in the infoview, in the way that is possible for terms in the editor itself, but that is less of an issue.

[Floris van Doorn]

You can do it by clicking on subterms:
image.png
Does this solve your problem, or do you want to do it specifically by hovering?

[Jovan Gerbscheid]

Oh wow, I didn't realize that, thank you!

[Floris van Doorn]

You can also click in the infoview in VSCode. That has the advantage that the hover doesn't disappear just from mouse movement.

[Jovan Gerbscheid]

Yes, I see that now, that is very useful.

[Jon Eugster]

I've changed that setting (so that you need to click) a while ago following the wish of Patrick Massot because his student's got way too many confusing pop-ups flashing everywhere. It could also be configurable setting...

[Jovan Gerbscheid]

If people think that clicking is better, then why not change this in vscode as well? :)

[Kevin Buzzard]

I certainly know the "way too many confusing pop-ups" feeling, when you have to actively look for a space in your code to put your cursor because every = sign you hit gives you a massive pop up!

[Jovan Gerbscheid]

I haven't encountered this problem myself. Is there a reason to have the mouse over the tactic state when you're not looking for hover info?

[Kevin Buzzard]

You get pop ups wherever your mouse is in VS Code and I'm pretty much always using it full screen

[Jovan Gerbscheid]

I see, there are also the non-recursive hovers in the editor, which work the same way in the web editor.

[Patrick Massot]

This setting is specifically crucial for talks and lectures. In that case putting the mouse cursor on the infoview to point at things is very common.

[Patrick Massot]

Note that in VSCode there is already a setting for this. The hard-coded thing in only in the web editor.

[Marc Huisinga]

Jovan Gerbscheid said:

If people think that clicking is better, then why not change this in vscode as well? :)

Because, as you experienced yourself, it isn't easily discoverable, especially since hovers work differently by default in the rest of VS Code. We have a setting to disable the hovers specifically for talks and lectures, though.

[Jon Eugster]

Indeed, in lean4web we just set some default options (here) which might differ from the defaults set in VS-Code:

"lean4.input.eagerReplacementEnabled": true,
"lean4.infoview.showGoalNames": false,
"lean4.infoview.emphasizeFirstGoal": true,
"lean4.infoview.showExpectedType": false,
"lean4.infoview.showTooltipOnHover": false,

Generally I try to choose the settings based on (~ in this order):

• clean and simple appearance
• keeping the configurable settings minimal, only containing settings where no clear favourite can be found (e.g. editor.wordWrap or editor.acceptSuggestionOnEnter)
• best setting for inspecting a code snippet from a Zulip message
• best setting for presenting Lean in talks or for complete beginners doodling around before installing Lean themselves
• best setting for viewing the code on mobile (or generally non-desktop)

I'm happy to change these settings in lean4web or make some available in the user interface if there there is any argument for doing so.

On the other hand, the defaults for VSCode are managed by Marc & the FRO and they might have different reasoning on what's the best default choice as lean4web and the VSCode extension differ a bit in their main purpose.

[Jovan Gerbscheid]

I also got confused recently about the second goal being shaded compared to the first goal. Good to know it's a setting :)

[Patrick Massot]

There is an unavoidable tension because the live server is used in wildly different situations. It is used by experts following links from code blocks on zulip and it is used by total beginners who want to see some Lean without installing anything and without registering on any website (so no CodeSpaces, no GitPod).

[Patrick Massot]

I think it’s good that the default settings favor the total beginner case.

[Patrick Massot]

But it would be even nicer to allow more configuration (not only more setting exposed, maybe hidden in an “advanced settings” panel, but also via url arguments).

[Notification Bot]

10 messages were moved from this topic to #general > lean4.infoview.showGoalNames is false in the web editor by Eric Wieser.