Zulip Chat Archive

Stream: general

Topic: vscode infoview overhaul

Edward Ayers (May 08 2020 at 11:59):

To whom it may concern,

To make my widget-view thing work in vscode, I modified the code for the vscode extension's infoview quite a lot. In particular infoview.ts is now just a dumb pipe that forwards all the server messages to the webview which is running some react code to update the infoview. So all of the code to do with formatting messages and handling the state of the infoview is now done in the webview javascript. The HTML of the webview page is set once and then the rest is done with server messages and code running in the webview.

But I broke stuff like freezing the state and the red highlighting thing. I don't want to cause a regression in functionality so I thought I'd make a thread where we can chat about what should be in the featureset for this overhauled version, or perhaps it is best left alone.

My questions are:

does anyone use the red code highlighting feature? (sometimes when you hover over an error message or goal the relevant sourcetext will be highlighted in red.)
the goal view came with output freezing, which I intend to keep, are there any other features of the infoview that are needed by anyone? Filtering different members of the local variables list should be possible using the widget system.

Patrick Massot (May 08 2020 at 12:01):

I never use the red thing. For a very long time I thought this was a bug, before someone told me it is a feature.

Patrick Massot (May 08 2020 at 12:02):

About 2, see https://github.com/leanprover/vscode-lean/issues/151

Chris Hughes (May 08 2020 at 12:20):

I only just found out about the red highlighting feature. I only ever use Display Goal, never Display Messages.

Mario Carneiro (May 08 2020 at 12:20):

does anyone use the red code highlighting feature? (sometimes when you hover over an error message or goal the relevant sourcetext will be highlighted in red.)

Oh, I almost forgot about that. That's perfect for the feature I just PR'd, vscode-lean#158, which adds a "sticky position" flag to give live goal feedback somewhere other than the current cursor position. Right now there is no visible indicator of where it is or even if it is on, so a little red line on the mark would help.

Edward Ayers (May 08 2020 at 13:21):

Maybe it would be cool to have that the infoview produces a goal state etc under your cursor, and then you have the option to 'pin' the state, then the infoview will report what is going on at that cursor position and the cursor infoview will render below that

Bryan Gin-ge Chen (May 08 2020 at 14:48):

This sounds great! The infoview has definitely needed a refactoring along the lines you described for a while.

Edward Ayers (Jun 17 2020 at 16:49):

Would anyone mind if the 'Display Messages' command and button in vscode was dropped (So there is only 'Display Goal'? What is the use case for it? In the overhauled version there is a collapsible section called All Messages that is always present instead.

Bhavik Mehta (Jun 17 2020 at 16:50):

I sometimes find it useful to use when there's a red underline on one character which I can't spot, and the display messages button helps find it

Bhavik Mehta (Jun 17 2020 at 16:50):

All messages would be fine instead though

Edward Ayers (Jun 17 2020 at 16:51):

Yeah the idea of the new version is that it would display both the goals and all of the messages always. And if there are too many all messages you can just collapse it.

Gabriel Ebner (Jun 17 2020 at 16:52):

all of the messages always

There are two collapsible sections: one for the errors on the current line (shown by default), and another one for all errors in the current file (hidden by default). You can toggle them individually.

Bhavik Mehta (Jun 17 2020 at 16:53):

What's the difference between the new version and the existing version?

Bryan Gin-ge Chen (Jun 17 2020 at 16:54):

The new version is a complete overhaul so there are a ton of differences.

Bhavik Mehta (Jun 17 2020 at 16:54):

Sure, but I mean in relation to the info which Ed is talking about

Bryan Gin-ge Chen (Jun 17 2020 at 16:58):

Maybe these screenshots help? Screenshot-2020-06-17-12.57.56.png Screenshot-2020-06-17-12.58.19.png

Bryan Gin-ge Chen (Jun 17 2020 at 16:59):

I just noticed that the blue bar to the left of the "Tactic State" widget changes to yellow when I resize the window. Is that intentional?

Bhavik Mehta (Jun 17 2020 at 17:00):

Ah yeah that clears it up perfectly, thanks!

Patrick Massot (Jun 17 2020 at 17:01):

I find this blue line distracting, and it feels like it's eating some of our precious horizontal space.

Gabriel Ebner (Jun 17 2020 at 17:01):

changes to yellow

I also find this irritating. It also lights up yellow when I move around with the cursor.

Edward Ayers (Jun 17 2020 at 17:02):

Bryan Gin-ge Chen said:

I just noticed that the blue bar to the left of the "Tactic State" widget changes to yellow when I resize the window. Is that intentional?

It changes to yellow when the state changed and it's updating, so I am guessing what is happening is that resizing the window is changing the 'region of interest' and this causes it to update

Gabriel Ebner (Jun 17 2020 at 17:02):

And when there's no info it switches between "no info found" and "updating...", which I can't stand either.

Edward Ayers (Jun 17 2020 at 17:02):

Glad that people are speaking out

Patrick Massot (Jun 17 2020 at 17:06):

We are still very grateful for your work!

Bryan Gin-ge Chen (Jun 17 2020 at 17:16):

On Lean 3.4.2 with an empty file I'm still seeing the "Error updating: . Try again." message.

Edward Ayers (Jun 17 2020 at 17:25):

Ok to get rid of the flashy color change issue i've put an easing animation on the colour change so that it changes colour slowly. Would people rather that the vertical bar is removed and that the title state changes colour or keep the vertical bar? My reasoning behind the bar is that it looks similar to the orange in the text editor gutter when a lean file is loading

Gabriel Ebner (Jun 25 2020 at 14:45):

A new vscode extension pre-release for today's Lean release, now with widget trace message support. The widget branch has been merged, so this will be the next vscode extension release. I think all issues that were publicly mentioned in the last thread are fixed now. Please let me know about additional bugs, otherwise this will land in your vscode.
lean-0.15.15.vsix

Kevin Buzzard (Jun 25 2020 at 14:54):

Did we lose "pause" functionality?

Kevin Buzzard (Jun 25 2020 at 14:55):

(he says, staring at the output of the linter at the end of a very long file)

Gabriel Ebner (Jun 25 2020 at 15:02):

Hmm, that's supposed to be the "pin", which pins the current position. But that seems to disable error messages..

Bryan Gin-ge Chen (Jun 25 2020 at 15:12):

There is a pause icon but it doesn't seem to behave as the play / pause icons do in the current version. If I click the (new) pause icon and then move the cursor, the icon changes back and the info view changes too, whereas with the current version of the extension, the entire infoview window is frozen until I click play again.

Gabriel Ebner (Jun 25 2020 at 15:29):

Oh yeah, the pause button is pretty broken. :sad:

Gabriel Ebner (Jun 25 2020 at 15:38):

Pinning is fixed now. As a workaround for pausing, you can first pin and then pause the pinned view. :-/
lean-0.15.15.vsix

Alex J. Best (Jun 25 2020 at 15:53):

Not a bug, but a feature request!:
First let me say widgets are amazing, I love using the new info view.
One thing that would make it even better would be a jump to definition / or expand to include the definition in the tooltips.
For example you're doing a long proof and some unfolding and rewriting and you end up with a term in your goal you don't know the definition of, with widgets you can see the type which is great, but sometimes seeing the definition is helpful for next steps, or jumping to the definition to check out nearby lemmas.
I had a go at implementing this myself, but got a bit stymied, as the vscode jump to def is position is based on the position of the cursor in the file, so I couldn't see how to repurpose it quickly, I imagine from within lean in the widget code it might be easier to find the code location, but I also don't yet know how put the right html in the widget to get to get vscode to jump to that location anyway.
So if someone knows how to do this I think it would be very cool!

Gabriel Ebner (Jun 25 2020 at 15:56):

jump to definition

I'd suggest the following implementation:

The goal widget (in interactive_expr.lean) annotates the output with links to filename & line number (these are accessible from meta code)
Define a html syntax to relay these links to the vscode extension.
Make the vscode extension recognize these links and hook them up correctly.

Bryan Gin-ge Chen (Jun 25 2020 at 16:13):

If pausing will only work for pinned views, maybe the pause button should be hidden for non-pinned views?

Pausing still seems to be canceled after I edit the file.

Also, if I start with my cursor in a #print statement or in a tactic block, the info view doesn't display the info there until I click or move the cursor.

Bryan Gin-ge Chen (Jun 25 2020 at 16:16):

This might be for a future release, but could we get a command / keyboard shortcut to expand /collapse the "all messages" widget? Maybe the old ctrl+alt+shift+enter?

Bryan Gin-ge Chen (Jun 25 2020 at 16:25):

I've been using the extension development host to test and the launched extension seems to reliably crash on close if I leave it open for longer than a few minutes.

Bryan Gin-ge Chen (Jun 25 2020 at 16:26):

I don't see any messages in the debug console though.

Patrick Massot (Jun 25 2020 at 18:03):

We cannot click the Try this links.

Patrick Massot (Jun 25 2020 at 19:19):

The widget view swallows the body of let statements.

Patrick Massot (Jun 25 2020 at 19:20):

Compare the tactic state in widget and plain text at the end of the first line in:

example : true :=
begin
  let n := 0,
  trivial
end

Gabriel Ebner (Jun 25 2020 at 22:08):

Last update for today: the pausing now also works for non-pinned views. Try this also works. lean-0.15.15.vsix

The let display unfortunately needs to be fixed in lean (lean#360), or patched in mathlib
The ctrl+alt+shift+enter shortcut is filed (vscode-lean#188)
I hope I didn't miss anything here.

Patrick Massot (Jun 25 2020 at 22:09):

Thanks!

Patrick Massot (Jun 25 2020 at 22:09):

Zulip says the VSCode extension repo should move to leanprover-community

Bryan Gin-ge Chen (Jun 25 2020 at 22:19):

leanprover/vscode-lean#188

Bryan Gin-ge Chen (Jun 26 2020 at 07:46):

The type of the term under the cursor no longer shows up in the status bar. Do we still want this feature? I've found it useful sometimes, but it's not very discoverable and probably most people don't know it exists. If people still want it, the quickest way I can see to fix it is to add back some of this code, but I haven't studied the new info view code yet, so that might be too hacky.

Gabriel Ebner (Jun 26 2020 at 08:40):

I didn't notice it was gone because I've never used it. You could use the same approach as now and send a message to the extension (using post) from the Info component when it updates.

Patrick Massot (Jun 26 2020 at 08:41):

Gabriel won't like this comment, but we lost the goals accomplished color.

Gabriel Ebner (Jun 26 2020 at 08:44):

The goals accomplished color was the default text color. It's actually gained color: it's now blue.

Gabriel Ebner (Jun 26 2020 at 08:44):

Unfortunately, this now needs to be fixed in core lean (we can also patch it from mathlib)

Patrick Massot (Jun 26 2020 at 08:45):

It's not blue here.

Patrick Massot (Jun 26 2020 at 08:45):

Maybe I have an outdated extension.

Gabriel Ebner (Jun 26 2020 at 08:47):

You could also have an outdated mathlib/lean. The tactic state rendering (including the color and text for "goals accomplished") is now implemented in lean.

Patrick Massot (Jun 26 2020 at 08:48):

My mathlib is from yesterday afternoon.

Patrick Massot (Jun 26 2020 at 08:48):

It may be too old.

Patrick Massot (Jun 26 2020 at 08:48):

It's from the bump to 3.16.5 commit.

Patrick Massot (Jun 26 2020 at 08:49):

But I don't see any commit that seem relevant.

Gabriel Ebner (Jun 26 2020 at 08:50):

Ok, I also have a mathlib with 3.16.4. And my "goals accomplished" is blue.

Patrick Massot (Jun 26 2020 at 08:50):

Then you have an outdated mathlib

Rob Lewis (Jun 26 2020 at 08:50):

I'm on the latest extension and 3.16.5, it's blue for me too.

Patrick Massot (Jun 26 2020 at 08:50):

It's 3.16.5 now.

Patrick Massot (Jun 26 2020 at 08:56):

Weird, it's blue again now. But the font size is now tiny.

Edward Ayers (Jun 26 2020 at 11:07):

Alex J. Best said:

One thing that would make it even better would be a jump to definition / or expand to include the definition in the tooltips. ...

Hi Alex! Thanks for this, another idea for implementing this would be to change the type of tactic.save_widget so that it also supports actions like 'reveal definition' instead of just 'insert text' implemented at the moment.

Edward Ayers (Jun 26 2020 at 11:08):

Thanks so much to @Gabriel Ebner for patiently reviewing my code.

Edward Ayers (Jun 26 2020 at 11:10):

Kevin Buzzard said:

Did we lose "pause" functionality?

Wrt pausing. Is the problem that it is buggy or that it works differently to previously? I reimplemented the pausing from scratch so if there is a difference in behaviour it's just because I didn't look at how the old pausing works carefully enough.

Gabriel Ebner (Jun 26 2020 at 11:11):

Yesterday the pause did not work on the main (non-pinned) info. If you pressed pause and then moved the cursor, then it would immediately unpause.

Gabriel Ebner (Jun 26 2020 at 11:12):

But that's fixed now.

Bryan Gin-ge Chen (Jun 26 2020 at 16:03):

Some more requests, I might be able to work on some of these this weekend:

The README still needs to be updated (I promised to help with this, so I'll work on this first.)
Could we get a way to pause "all messages"?
The keyboard shortcut that expands "all messages" only seems to work when the info view window is focused, which makes it less convenient. Could we get it to work from the editor window as well? (Also, it seems to now be ctrl+opt+shift+enter on mac, whereas the old all messages was cmd+opt+shift+enter)
Could we add tooltips to the various icons in the info view?
It can be a little tough to tell where one widget ends and the next one begins. Can we update the styling somehow to make that clearer? Maybe the top-level widget headers should have a different color background? Or maybe there should be more indentation, or some outlining?

Gabriel Ebner (Jun 26 2020 at 16:55):

Thank you for taking care of the README!
Pausing all messages is implemented now.
I don't think we have a shortcut to expand all messages.
Tooltips work for me.
I agree that the styling could use a bit of love. To me it feels much more crowded than the current info view. I'd prefer to avoid indentation though, horizontal screen real estate is already a scarce commodity with mathlib theorem statements.

Gabriel Ebner (Jun 26 2020 at 17:01):

The expand all messages shortcut is implemented. Complain if you want this to be a toggle instead.

Bryan Gin-ge Chen (Jun 28 2020 at 15:13):

Gabriel Ebner said:

The expand all messages shortcut is implemented. Complain if you want this to be a toggle instead.

Yes, it'd be nice if it were a toggle. :smile: (I'm not sure why I thought it was implemented before. Maybe I had all messages in focus and pressing enter expanded / collapsed it?)

Tooltips also work for me, but it takes a bit longer than I expected.

In this screenshot, (from Kevin's thread), you can see that p, q, r, ... are all squished together in the tactic state to form one giant variable pqrstuvw: Screenshot-2020-06-28-11.07.56.png

(going through the info view code today, hopefully README PR tonight...)

Edward Ayers (Jun 28 2020 at 18:17):

should be fixed by lean#365

Rob Lewis (Jun 29 2020 at 18:33):

When I have two variables with the same type consecutive in the context, the tactic state view seems to concatenate their names without a space. This doesn't happen with an underscore. image.png

Rob Lewis (Jun 29 2020 at 18:33):

Any ideas?

Rob Lewis (Jun 29 2020 at 18:34):

Also, I still have the extension installed from a .vsix file, do you know if there's a way to go back to the marketplace version?

Alex J. Best (Jun 29 2020 at 18:35):

@Rob Lewis is this the same issue as the previous message in the thread?

Rob Lewis (Jun 29 2020 at 18:35):

Oh, haha, it is. Sorry.

Gabriel Ebner (Jun 29 2020 at 19:03):

There is no going back. You will get the new version anyhow as soon as Bryan is finished with the readme.

Patrick Massot (Jun 29 2020 at 19:05):

Is the let bug fixed?

Gabriel Ebner (Jun 29 2020 at 19:06):

The let bug is unfortunately in Lean, but we can also fix it from mathlib. I wanted to fix this in mathlib after #3181.

Gabriel Ebner (Jun 29 2020 at 19:37):

Since let-values seem to be strangely important to you: #3228

Patrick Massot (Jun 29 2020 at 19:47):

Thanks!

Patrick Massot (Jun 29 2020 at 19:48):

Is it strange to want to see the let values?

Gabriel Ebner (Jun 29 2020 at 19:48):

No, not at all.

Kevin Buzzard (Jun 29 2020 at 20:14):

The main use I have for seeing the let values is that their absence indicates to me that I used have by accident.

Bryan Gin-ge Chen (Jul 06 2020 at 06:34):

The first draft of the vscode-lean README refresh is finally done: leanprover/vscode#202

Since I made a ton of changes, it'd be great to get some feedback. See the PR'd README here. Any comments, criticisms and corrections appreciated!

Jasmin Blanchette (Jul 06 2020 at 07:17):

The first link of your post gives me a 404.

Johan Commelin (Jul 06 2020 at 07:20):

It should be vscode-lean instead of merely vscode.

Gabriel Ebner (Jul 06 2020 at 13:44):

Muhaha.

Kevin Buzzard (Jul 06 2020 at 14:52):

I'm streaming tomorrow and I'm going to have lets. Is there any way I can their definitions showing up?

Patrick Massot (Jul 06 2020 at 14:55):

Hopefully this will be fixed by then.

Bryan Gin-ge Chen (Jul 06 2020 at 15:00):

Johan Commelin said:

It should be vscode-lean instead of merely vscode.

whoops, fixed, though vscode-lean 0.16.0 has been released in the meantime!

Edward Ayers (Jul 06 2020 at 15:05):

Bryan this readme is gorgeous!

Bryan Gin-ge Chen (Jul 06 2020 at 15:07):

Thanks Ed, I hope it accurately captures how to use all the new features! I was up a bit late working on it, so I wouldn't be surprised if I got some / many things wrong...

Kevin Buzzard (Jul 06 2020 at 15:08):

Oh wooah -- to anyone only half-paying attention here and who thinks that they know everything about the tactic state -- Bryan's README indicates that there are now a gazillion new tricks that you can do with this new "widget" version.

Edward Ayers (Jul 06 2020 at 15:15):

My only worry is that if we update the looks of the infoview in the future then some of the screenshots might need to be redone. But maybe it's ok to have slightly out of date screenshots because they still convey the functionality well.

Patrick Massot (Jul 06 2020 at 15:22):

Isn't the screenshot using some parentheses plugins?

Bryan Gin-ge Chen (Jul 06 2020 at 15:24):

Oh yeah, I did have bracket pair colorizer turned on. Hope that's not too distracting.

Edward Ayers (Jul 06 2020 at 15:25):

I think it's fine

Patrick Massot (Jul 06 2020 at 15:25):

The new README looks awesome

Patrick Massot (Jul 06 2020 at 15:25):

Should we render it somewhere on the community website too? We should also move the leanproject documentation there, it's currently too difficult to find

Patrick Massot (Jul 06 2020 at 15:27):

It seems there is a missing icon at https://github.com/leanprover/vscode-lean/blob/master/media/reveal-file-location.png

Bryan Gin-ge Chen (Jul 06 2020 at 15:31):

Whoops, thanks for catching that! https://github.com/leanprover/vscode-lean/pull/203

Gabriel Ebner (Jul 06 2020 at 15:44):

Kevin Buzzard said:

I'm streaming tomorrow and I'm going to have lets. Is there any way I can their definitions showing up?

The formatting of the tactic state is now tied to the mathlib version essentially, so you need to update mathlib to see lets. The fix was merged on June 30.

Kevin Buzzard (Jul 06 2020 at 16:12):

Indeed I'm way behind, I'm back on June 28th. Thanks!

Sebastien Gouezel (Jul 06 2020 at 17:58):

Looks like my vscode has just updated and given me the new widgets. This is amazing.

Of course, I have a (very little) complaint :-) In the attached image, you can see that I don't have access to the button to close the type display, because the type is too large. If the button could be (also?) in the upper left corner, to the left of Prop, it would help!

Edward Ayers (Jul 06 2020 at 18:00):

oh dear that's a bug. As a quick fix, you can scroll to the far right of the infoview with the scrollbar at the bottom to get to the close button

Mario Carneiro (Jul 06 2020 at 18:01):

alternatively, you should be able to dismiss it by clicking elsewhere in the view?

Sebastien Gouezel (Jul 06 2020 at 18:01):

That's not a bug, I can scroll right (a lot) to get access to the button, or enlarge a lot the corresponding window. So, my message is more a feature request than a bug report.

Edward Ayers (Jul 06 2020 at 18:02):

Mario Carneiro said:

alternatively, you should be able to dismiss it by clicking elsewhere in the view?

elsewhere in the expression

Edward Ayers (Jul 06 2020 at 18:03):

I can't get my version of infoview to scroll, it always word wraps instead...

Sebastien Gouezel (Jul 06 2020 at 18:05):

It wraps words if it's a complicated type, but if there are many types when you select a large expression, it doesn't.

Johan Commelin (Jul 06 2020 at 18:07):

Oooh, I've finally updated my branch to latest master. This is sweeeet. :sweet_potato: :candy: :pancakes: :honey:

Yakov Pechersky (Jul 06 2020 at 18:28):

It seems that the 0.16.0 extension no longer works with SSH-Remote VSCode

Yakov Pechersky (Jul 06 2020 at 18:28):

I see no contents in Lean infoview

Bryan Gin-ge Chen (Jul 06 2020 at 18:29):

What version of Lean is your project using?

Yakov Pechersky (Jul 06 2020 at 18:29):

Still able to see output in Problems in the tab next to Termianl

Yakov Pechersky (Jul 06 2020 at 18:29):

What's the most straightforward way to check that?

Bryan Gin-ge Chen (Jul 06 2020 at 18:29):

What does version say in leanpkg.toml?

Bryan Gin-ge Chen (Jul 06 2020 at 18:30):

I think the issue is that the infoview now uses its own separate server connection (whereas before it used the same one as the editor), and this is probably too complicated for the remote vscode functionality to keep track of.

Bryan Gin-ge Chen (Jul 06 2020 at 18:31):

We'll need to think about related stuff to get "live share" to work too.

Yakov Pechersky (Jul 06 2020 at 18:31):

lean_version = "leanprover-community/lean:3.16.5"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "f06e4e00a32ce6a349a0d2b0e3a65cd453599dbd"}```

Yakov Pechersky (Jul 06 2020 at 18:32):

=C I'm going to have to downgrade =C

Bryan Gin-ge Chen (Jul 06 2020 at 18:34):

Here's the page we'll have to study to fix this: https://code.visualstudio.com/api/advanced-topics/remote-extensions

Gabriel Ebner (Jul 06 2020 at 18:37):

Bryan Gin-ge Chen said:

I think the issue is that the infoview now uses its own separate server connection (whereas before it used the same one as the editor), and this is probably too complicated for the remote vscode functionality to keep track of.

It's not just the server connection of the infoview (which is tunneled over regular webview messages; if clicking buttons in the infoview used to work then this shouldn't be the issue). There is also an HTTP server that we run on localhost, which is very likely to be a problem: https://github.com/leanprover/vscode-lean/blob/bcece76b9cff5a06653510b0dea7c58692c84f30/src/staticserver.ts

Edward Ayers (Jul 06 2020 at 18:37):

https://code.visualstudio.com/api/advanced-topics/remote-extensions

Bryan Gin-ge Chen (Jul 06 2020 at 18:38):

Gabriel Ebner said:

It's not just the server connection of the infoview (which is tunneled over regular webview messages; if clicking buttons in the infoview used to work then this shouldn't be the issue). There is also an HTTP server that we run on localhost, which is very likely to be a problem: https://github.com/leanprover/vscode-lean/blob/bcece76b9cff5a06653510b0dea7c58692c84f30/src/staticserver.ts

Ah, true. But I thought that was added a while back. @Yakov Pechersky was the most recent previous version of the extension working for you?

Yakov Pechersky (Jul 06 2020 at 18:39):

Just downgraded to 0.15.1, and the Lean Goal window shows info as before today.

Edward Ayers (Jul 06 2020 at 18:41):

I get Failed to load resource: net::ERR_CONNECTION_REFUSED in the webview developer tools if I use it remotely

Edward Ayers (Jul 06 2020 at 18:43):

I think the problem is that this line is not resolving index.js correctly: https://github.com/leanprover/vscode-lean/blob/bcece76b9cff5a06653510b0dea7c58692c84f30/src/infoview.ts#L363

Gabriel Ebner (Jul 06 2020 at 18:48):

Yep, that looks just like to workaround HTTP server that we use to serve the index.js.

Gabriel Ebner (Jul 06 2020 at 18:48):

This looks useful: https://code.visualstudio.com/api/advanced-topics/remote-extensions#forwarding-localhost

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:10):

Hello! Is there a way to inlcude a :party_ball: whenever a goals accomplished is reached at the end of a lemma/theorem/proof?

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:11):

I'm on 3.16.5 lean version and 0.16.1 vscode extension and heard the legend that emojis had been added...

Johan Commelin (Jul 09 2020 at 04:12):

We had such an emoji for 2 or 3 weeks... but it was decided that it would be better to have something sober and professional. (Even though the atmosphere here on Zulip is extremely relaxed and we make fun with emojis all the time.)

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:15):

... Can I toggle a "fun" string option somewhere?

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:16):

Also, :broken_heart: on the :thumbs_down: vs Emojis :(

Mario Carneiro (Jul 09 2020 at 04:18):

Maybe we can have a vscode setting to change the string so users can do this for themselves?

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:19):

Yup, just modifying the goals accomplished string in VSCode seems reasonable.

Johan Commelin (Jul 09 2020 at 04:24):

Miguel Raz Guzmán Macedo said:

Also, :broken_heart: on the :thumbs_down: vs Emojis :(

Sure, I get it. :oops: :shrug: But not everyone is well-versed in emoji... so it might be better to default to the universal world-dominating lang. :see_no_evil:

(Aside: why is there no :emoji:?)

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:25):

In the JuliaLang Slack/Zulip we uploaded custom emojis for the Unicode Consortium :D

Johan Commelin (Jul 09 2020 at 04:28):

@Miguel Raz Guzmán Macedo Note that, really, replacing the "goals accomplished" string with an emoji isn't enough. It should actually play the imperial march to be complete.

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:29):

We might as well just rick roll people on every completed proof amirite :sweat_smile:

Johan Commelin (Jul 09 2020 at 04:31):

But if you do it every time, it isn't rickrolling anymore, right?

Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:34):

Only on April fools, and once.

Just to keep people on their toes.

Patrick Massot (Jul 09 2020 at 08:04):

I think the goals accomplished message could have a special CSS class and the extension setting should allow CSS code.

Patrick Massot (Jul 09 2020 at 08:05):

See https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive_expr.lean#L305

Patrick Massot (Jul 09 2020 at 08:06):

I tried to modify it to make that line bigger but failed. @Edward Ayers is there any documentation we could read here?

Edward Ayers (Jul 09 2020 at 09:39):

how did it fail?

Edward Ayers (Jul 09 2020 at 09:41):

The stylesheet that is loaded in by default is called 'tachyons' and the docs are here. I wanted a set of default styles that were configurable without having to use lots of inline styles or needing to change a stylesheet so it seemed like a good enough fit.

Edward Ayers (Jul 09 2020 at 09:41):

You can also add your own inline styles if you prefer

Edward Ayers (Jul 09 2020 at 09:43):

So eg you could do h "div" [style [("font-size", "1.5rem")]] ["goals accomplished"].

Edward Ayers (Jul 09 2020 at 09:46):

Having custom classes for things and then making a stylesheet somewhere is a bad idea because now the widgets will behave differently across different editor setups.

Edward Ayers (Jul 09 2020 at 09:48):

Mario Carneiro said:

Maybe we can have a vscode setting to change the string so users can do this for themselves?

With widgets you can do this in mathlib, make a custom environment option for 'fun mode' and then edit this line to check for the fun mode option.

Patrick Massot (Jul 09 2020 at 09:53):

The help is wanted is not about tachyons, it's about h in h "div" [style [("font-size", "1.5rem")]] ["goals accomplished"]

Edward Ayers (Jul 09 2020 at 10:03):

The other source of widget docs is here

Edward Ayers (Jul 09 2020 at 10:04):

meta def rainbow {α} : string → html α
| x :=
  let r := ["red", "gold", "yellow", "green", "blue", "purple"] in
  h "div" [cn "f2"] $ list.map_with_index (λ i (x: char), h "span" [cn $ "" <| list.nth r (i % r.length)] [x.to_string]) $ string.to_list x

#html (rainbow "goals accomplished")

Patrick Massot (Jul 09 2020 at 10:08):

He means https://leanprover-community.github.io/mathlib_docs/core/init/meta/widget/basic.html

Patrick Massot (Jul 09 2020 at 10:08):

Thanks!

Kenny Lau (Jul 09 2020 at 10:16):

It looks like the "filter" (that filters out statements in the context) is not very permanent; if you set it somewhere it only applies to that specific place.

Patrick Massot (Jul 09 2020 at 10:18):

Yes, Ed knows. It will be fixed eventually.

Kenny Lau (Jul 09 2020 at 10:20):

ok thanks

Amanda Hauer (Jul 13 2020 at 20:39):

Yakov Pechersky said:

It seems that the 0.16.0 extension no longer works with SSH-Remote VSCode

Downgrading to an earlier version such as 0.15.15 will make the problem go away for now. Hopefully, an update is released that makes Lean Infoview work in remote containers as well.

Bryan Gin-ge Chen (Jul 13 2020 at 21:07):

It's definitely on our radar. The big feature we'd like to go after first is getting "Live Share" to work. It's likely that in the course of investigating that we'll learn things that will help us with SSH-Remote compatibility as well.

Johan Commelin (Jul 30 2020 at 04:50):

I'm currently working on a Dutch mini-localisation. Can I overwrite the "goals accomplished" message?

Johan Commelin (Jul 30 2020 at 04:51):

(Other than that, I'm mostly just doing meta def tactic.interactive.dutch_name := tactic.interactive.english_name)

Bryan Gin-ge Chen (Jul 30 2020 at 04:57):

I think you can copy the override that's done in mathlib. Here's where "goals accomplished :tada: " is: https://github.com/leanprover-community/mathlib/blob/593b1bb5ff4c241a677ef9a617d404d4b6b06c32/src/tactic/interactive_expr.lean#L331 and the bottom of the file shows the attributes used to override the widgets in core Lean.

Johan Commelin (Jul 30 2020 at 05:45):

So I would copy-paste-edit tactic_view_component
and then issue something like

attribute [vm_override custom_tactic_view_componenent] widget_override.tactic_view_component

Is that right?

Johan Commelin (Jul 30 2020 at 05:46):

I have no idea how vm overrides work

Bryan Gin-ge Chen (Jul 30 2020 at 05:56):

I also don't really know. Maybe @Edward Ayers can help?

Gabriel Ebner (Jul 30 2020 at 07:06):

(deleted)

Gabriel Ebner (Jul 30 2020 at 07:07):

Yes, that should work.

Edward Ayers (Jul 30 2020 at 10:03):

I think it would be better to override tactic.save_info

Edward Ayers (Jul 30 2020 at 10:04):

The idea of tactic_component is it's just a component that lets you access the tactic state

Edward Ayers (Jul 30 2020 at 10:04):

So you shouldn't have to copy that code

Edward Ayers (Jul 30 2020 at 10:05):

I acknoledge that the docs could be better for all of this

Edward Ayers (Jul 30 2020 at 10:08):

This is the second time someone wanted to change the goals accomplished message so we should rewrite interactive_expr.leanso that it reads the goals-accomplished message from a separate component or from an entry in environment options.

Edward Ayers (Jul 30 2020 at 10:10):

EDIT: Sorry I misread tactic_view_component as tactic_component

Johan Commelin (Jul 30 2020 at 10:17):

Isn't there a rule of three? But I'm sure this a third person who doesn't mind asking for this (-;

Patrick Massot (Jul 30 2020 at 10:21):

If Ed has time for this game then I think that offer a copy button is much more important, especially now that VSCode completely prevents any copy-paste from the info view.