Zulip Chat Archive

Stream: new members

Topic: Goal accomplished for term mode


Patrick Lutz (Jun 02 2020 at 21:14):

This isn't really a question, but I find it slightly sad that Lean doesn't tell me goals accomplished!when I complete a proof in term mode. I miss the little dopamine rush that it gives me

Mario Carneiro (Jun 02 2020 at 21:15):

Lean prefers negative reinforcement. "Congratulations, you aren't wrong anymore."

Reid Barton (Jun 02 2020 at 21:17):

it should put an :octopus: under each error-free declaration

Mario Carneiro (Jun 02 2020 at 21:20):

Setting aside the silly options, it isn't really clear how to have a UI that recognizes your achievements without going overboard. Perhaps something like flashing the entire definition body briefly (change the text color or something) if this is the first time the server has seen a theorem with this name being proven?

Mario Carneiro (Jun 02 2020 at 21:23):

It is also useful just to have confirmation that you are done, since term mode is often a matter of hunting down errors on underscores and there are a few seconds after I am done that I need to look over the definition to make sure I haven't missed anything

Reid Barton (Jun 02 2020 at 21:30):

Maybe the yellow bars should become orange/red bars when the declaration is done processing, but contains a warning/error?

Reid Barton (Jun 02 2020 at 21:30):

I use console emacs so I don't even get the bars...

Reid Barton (Jun 02 2020 at 21:32):

Or green bars next to everything that's okay? Is that too much?

Mario Carneiro (Jun 02 2020 at 21:32):

I already have some difficulty distinguishing the "compiling" orange bars from "git modified" orange bars. Please no more yellow/orange

Reid Barton (Jun 02 2020 at 21:33):

Wow all these fancy features

Reid Barton (Jun 02 2020 at 21:34):

I wonder whether I can set up emacs to change the text background color in place of the bars

Mario Carneiro (Jun 02 2020 at 21:34):

I think using low contrast "greyed out" text would work well as a substitute for "compiling" orange bars

Mario Carneiro (Jun 02 2020 at 21:35):

although since the compiling status of the current proof changes often it may be too distracting

Bryan Gin-ge Chen (Jun 02 2020 at 21:36):

Hmm, my git modified bars are blue for added lines and green for modified lines.

Mario Carneiro (Jun 02 2020 at 21:39):

Hm, me too. Maybe I was thinking of the search highlighting

Mario Carneiro (Jun 02 2020 at 21:41):

Ah, "git modified" is orange in my night theme

Mario Carneiro (Jun 02 2020 at 21:45):

I think I recall seeing a green checkmark on every checked definition in Arend, and I do think that it is too much. It doesn't look like something that scales well to large developments, especially if your IDE wants to be helpful and tell you where all the annotations are

Bryan Gin-ge Chen (Jun 02 2020 at 21:56):

I'm guessing it's not possible with the current Lean 3 server, since we only get line / column annotations on errors, but it'd be nice if we could get the "Lean goal" window to show not only the tactic state but also all errors arising from the current proof or theorem. Currently I think it only shows errors if they happen to be on the same line as the cursor.

Kevin Buzzard (Jun 03 2020 at 07:30):

@Patrick Lutz how about the Zelda "get item" music plays every time you finish a term mode proof?

Jesse Michael Han (Jun 08 2020 at 02:45):

Reid Barton said:

I wonder whether I can set up emacs to change the text background color in place of the bars

@Reid Barton yes, use M-x customize-face lean-server-task-face

i doubled the thickness of lean-server-task-fringe-face and it was a huge quality-of-life buff

Kevin Buzzard (Jun 08 2020 at 08:07):

https://xkcd.com/378/


Last updated: Dec 20 2023 at 11:08 UTC