lean4.infoview.showGoalNames is false in the web editor

Stream: general

[Eric Wieser]

Jon Eugster said:

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,

What's the rational for showGoalNames : false?

[Eric Wieser]

The case tactic is much harder to use with that setting

[Kevin Buzzard]

That's an interesting comment because I have never understood the point of showGoalNames at all and usually my names are random very long things which just irritate me.

[Patrick Massot]

In elementary math proofs it is extremely rare to have meaningful case names.

[Kevin Buzzard]

I should probably also say that I'm not sure I ever use the case tactic :-)

[Ruben Van de Velde]

Not sure if you're suggesting that Kevin is only working on elementary math :innocent:

[Bhavik Mehta]

I like the case names for demonstrating proofs by induction, where I can say "Lean is showing you the two cases you need to fill in, and they're called the zero case and the successor case"

[Kevin Buzzard]

But I just use the lightbulb to do that.

[Aaron Liu]

I don't use the case tags often but when I want them and they're not there it takes a chunk of my time trying to figure out what they are (last time I wanted to use this was #mathlib4 > named subgoals with `obtain` @ 💬)

[Eric Wieser]

Patrick Massot said:

In elementary math proofs it is extremely rare to have meaningful case names.

I think this is perhaps due to the case name generation being suboptimal; it would be much easier to suggest fixes for this feature if the web editor didn't just pretend the feature didn't exist.

[Notification Bot]

10 messages were moved here from #general > recursive hovers on the web editor by Eric Wieser.

[Patrick Massot]

Eric Wieser said:

Patrick Massot said:

In elementary math proofs it is extremely rare to have meaningful case names.

I think this is perhaps due to the case name generation being suboptimal; it would be much easier to suggest fixes for this feature if the web editor didn't just pretend the feature didn't exist.

I don’t buy that argument to change the web editor default. You can simply use your local lean for this.

[Edward van de Meent]

I feel like there still is no reasoning given as to why it should be hidden though? It usually doesn't take up much space, so if you don't use it, don't look at it. It's not like we disable tactics and tell people "If you want to use it, turn this option on".

[Edward van de Meent]

If you really don't want to see it, "you can simply use your local lean for this"

[Edward van de Meent]

In effect, this new behaviour is changing the default, which (imo) shouldn't have happened in the first place

[Edward van de Meent]

At the very least without asking the community

[Julian Berman]

To me the reasoning on both sides seems clear, which seems to leave room to actually discuss it objectively -- the reason to change the default is asserting "these names are noisy and rarely used and that makes it confusing to new users to see them" -- and maybe new users are more likely to be seeing the web editor than local lean, which justifies different defaults, or similarly users who are doing less "intensive" Lean work. The same audience often does typically see a much smaller set of tactics, some even indeed "disabled" no?

I actually even briefly considered changing this default in lean.nvim way back when I started writing it and it was just for myself -- if I would have known people who actually were experts found them noisy too I would have thought even harder about doing it... I think Lean has a ton of knobs -- I don't think in general that "if you don't use it don't look at it" is a free cost, it does cost something to have things visible if they're never going to be used.

(Though with all that being said I think I agree with the default as-is for "normal" Lean in the end)

[Patrick Massot]

Edward van de Meent said:

I feel like there still is no reasoning given as to why it should be hidden though? It usually doesn't take up much space, so if you don't use it, don't look at it. It's not like we disable tactics and tell people "If you want to use it, turn this option on".

I think you’ve been using Lean for too long and don’t realize what it looks like for beginners. Anything that can remove noise is priceless.

[Patrick Massot]

But it’s also interesting to see that maybe some people use this live lean server a lot more than I expected. I simply never use it when I’m not helping absolute beginners who only want to devote at most three hours to Lean. Copy-pasting a code snippet into my local lean is a negligible overhead compared to the benefit of using Lean locally.

[Aaron Liu]

Patrick Massot said:

But it’s also interesting to see that maybe some people use this live lean server a lot more than I expected. I simply never use it when I’m not helping absolute beginners who only want to devote at most three hours to Lean. Copy-pasting a code snippet into my local lean is a negligible overhead compared to the benefit of using Lean locally.

My local lean is quite a bit slower, so I use the live lean server for everything that isn't directly in a project.

[Jon Eugster]

Edward van de Meent said:

At the very least without asking the community

It's much easier to just implement a default and if anybody objects, then one can have this discussion about what's best :)

Anyways, I've never looked at the goal names and I've always considered them noisy junk, so I didn't think twice adding Patrick's request about 6 weeks ago.

I'll check back here later to see if there have been more opinions, or more examples where the goal names would be useful :)

[Eric Wieser]

I've had multiple cases where I've tried to explain metavariables to someone using the web editor, only to be confused that the goals are no longer named with their metavariable names:

example : ∃ n, n ^ 2 = 4 := by
  refine ⟨?m, ?_⟩
  -- I want to see `case m` here

[Kim Morrison]

Yes, my preference is that we add these back, for consistency with the VSCode experience.

[Patrick Massot]

Again, there won’t be a setting that works for everyone, the use cases are simply too different. What we need is a way to set this from the url.

[Jon Eugster]

Patrick Massot said:

What we need is a way to set this from the url.

https://github.com/leanprover-community/lean4web/issues/52
I mentioned this to Patrick privately at some point: I don't think I'll have time to implement that myself, but I agree that would be a nice feature!

[Yakov Pechersky]

On it. Can I have branch create permissions please?

[Yakov Pechersky]

Do we want changing of the settings to be reflected back into the URL, or have this just be a "if you know, you know" option?

[Yakov Pechersky]

Example proposed diff

diff --git i/client/src/App.tsx w/client/src/App.tsx
index 0dc823d..349fe17 100644
--- i/client/src/App.tsx
+++ w/client/src/App.tsx
@@ -9,11 +9,13 @@ import { faCode } from '@fortawesome/free-solid-svg-icons'

 // Local imports
 import LeanLogo from './assets/logo.svg'
-import defaultSettings, { IPreferencesContext, lightThemes } from './config/settings'
+import defaultSettings, { IPreferencesContext, IPreferencesParams, lightThemes, preferenceParams } from './config/settings'
 import { Menu } from './Navigation'
 import { PreferencesContext } from './Popups/Settings'
 import { fixedEncodeURIComponent, formatArgs, lookupUrl, parseArgs } from './utils/UrlParsing'
 import { useWindowDimensions } from './utils/WindowWidth'
+import { useSearchParams } from 'react-router'
+

 // CSS
 import './css/App.css'
@@ -51,6 +53,7 @@ function App() {
   const [project, setProject] = useState<string>(undefined)
   const [url, setUrl] = useState<string | null>(null)
   const [codeFromUrl, setCodeFromUrl] = useState<string>('')
+  const [searchParams, _] = useSearchParams()

   /** Monaco editor requires the code to be set manually. */
   function setContent (code: string) {
@@ -90,7 +93,12 @@ function App() {
     let newPreferences: any = { ...preferences } // TODO: need `any` instead of `IPreferencesContext` here to satisfy ts
     for (const [key, value] of Object.entries(preferences)) {
       let storedValue = window.localStorage.getItem(key)
-      if (storedValue) {
+      // prefer URL params over stored
+      if (preferenceParams.includes(key) && searchParams.has(key)) {
+        const paramValue = !(searchParams.get(key) === "false")  // expecting true or false
+        console.debug(`[Lean4web] Found URL parameter for ${key}: ${paramValue}`)
+        newPreferences[key] = paramValue
+      } else if (storedValue) {
         saveInLocalStore = true
         console.debug(`[Lean4web] Found stored value for ${key}: ${storedValue}`)

[Jon Eugster]

You can also just fork the repo and make a PR from your fork, right?

[Yakov Pechersky]

Sure, if that's what you prefer

[Jon Eugster]

Thanks:blush:

[Yakov Pechersky]

image.png
https://github.com/leanprover-community/lean4web/pull/60

[Eric Wieser]

Could I suggest we make the default match vscode?

[Shreyas Srinivas]

Maybe this is just me, but I use case names every now and then. It is easier for me to skim the proof when I have them (for example when using by_cases or constructor).

[Eric Wieser]

This landed on github in https://github.com/leanprover-community/lean4web/commit/8b3e3c8dde9397be59db4ec203b00f514e91119d, right? I guess it's not yet deployed?

[Jon Eugster]

I've also haven't merged Yakov's PR yet, but I'll do that soon