Goal accomplished for term mode

Stream: new members

[Patrick Lutz]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

Wow all these fancy features

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Jesse Michael Han]

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]

https://xkcd.com/378/