Zulip Chat Archive

Stream: general

Topic: vscode infoview overhaul


view this post on Zulip 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:

  1. 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.)
  2. 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 08 2020 at 12:02):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 16:50):

All messages would be fine instead though

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 16:53):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 17 2020 at 16:54):

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

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 16:54):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 17:00):

Ah yeah that clears it up perfectly, thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 17 2020 at 17:02):

:)

view this post on Zulip Edward Ayers (Jun 17 2020 at 17:02):

Glad that people are speaking out

view this post on Zulip Patrick Massot (Jun 17 2020 at 17:06):

We are still very grateful for your work!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 14:54):

Did we lose "pause" functionality?

view this post on Zulip 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)

view this post on Zulip 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..

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jun 25 2020 at 15:29):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jun 25 2020 at 16:26):

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

view this post on Zulip Patrick Massot (Jun 25 2020 at 18:03):

We cannot click the Try this links.

view this post on Zulip Patrick Massot (Jun 25 2020 at 19:19):

The widget view swallows the body of let statements.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:09):

Thanks!

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:09):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 25 2020 at 22:19):

leanprover/vscode-lean#188

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:41):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:45):

It's not blue here.

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:45):

Maybe I have an outdated extension.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:48):

My mathlib is from yesterday afternoon.

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:48):

It may be too old.

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:48):

It's from the bump to 3.16.5 commit.

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:49):

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

view this post on Zulip Gabriel Ebner (Jun 26 2020 at 08:50):

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

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:50):

Then you have an outdated mathlib

view this post on Zulip Rob Lewis (Jun 26 2020 at 08:50):

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

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:50):

It's 3.16.5 now.

view this post on Zulip Patrick Massot (Jun 26 2020 at 08:56):

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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jun 26 2020 at 11:08):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jun 26 2020 at 11:12):

But that's fixed now.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip Edward Ayers (Jun 28 2020 at 18:17):

should be fixed by lean#365

view this post on Zulip 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

view this post on Zulip Rob Lewis (Jun 29 2020 at 18:33):

Any ideas?

view this post on Zulip 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?

view this post on Zulip Alex J. Best (Jun 29 2020 at 18:35):

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

view this post on Zulip Rob Lewis (Jun 29 2020 at 18:35):

Oh, haha, it is. Sorry.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 29 2020 at 19:05):

Is the let bug fixed?

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jun 29 2020 at 19:37):

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

view this post on Zulip Patrick Massot (Jun 29 2020 at 19:47):

Thanks!

view this post on Zulip Patrick Massot (Jun 29 2020 at 19:48):

Is it strange to want to see the let values?

view this post on Zulip Gabriel Ebner (Jun 29 2020 at 19:48):

No, not at all.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Jasmin Blanchette (Jul 06 2020 at 07:17):

The first link of your post gives me a 404.

view this post on Zulip Johan Commelin (Jul 06 2020 at 07:20):

It should be vscode-lean instead of merely vscode.

view this post on Zulip Gabriel Ebner (Jul 06 2020 at 13:44):

Muhaha.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jul 06 2020 at 14:55):

Hopefully this will be fixed by then.

view this post on Zulip 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!

view this post on Zulip Edward Ayers (Jul 06 2020 at 15:05):

Bryan this readme is gorgeous!

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 06 2020 at 15:22):

Isn't the screenshot using some parentheses plugins?

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jul 06 2020 at 15:25):

I think it's fine

view this post on Zulip Patrick Massot (Jul 06 2020 at 15:25):

The new README looks awesome

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Jul 06 2020 at 15:31):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 06 2020 at 16:12):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 06 2020 at 18:01):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Edward Ayers (Jul 06 2020 at 18:03):

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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 18:28):

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

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 18:28):

I see no contents in Lean infoview

view this post on Zulip Bryan Gin-ge Chen (Jul 06 2020 at 18:29):

What version of Lean is your project using?

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 18:29):

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

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 18:29):

What's the most straightforward way to check that?

view this post on Zulip Bryan Gin-ge Chen (Jul 06 2020 at 18:29):

What does version say in leanpkg.toml?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"}```

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 18:32):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Edward Ayers (Jul 06 2020 at 18:37):

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

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Jul 06 2020 at 18:39):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jul 06 2020 at 18:48):

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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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.)

view this post on Zulip Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:15):

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

view this post on Zulip Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:16):

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

view this post on Zulip 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?

view this post on Zulip Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:19):

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

view this post on Zulip 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:?)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Jul 09 2020 at 04:31):

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

view this post on Zulip Miguel Raz Guzmán Macedo (Jul 09 2020 at 04:34):

Only on April fools, and once.

Just to keep people on their toes.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 09 2020 at 08:05):

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

view this post on Zulip 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?

view this post on Zulip Edward Ayers (Jul 09 2020 at 09:39):

how did it fail?

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jul 09 2020 at 09:41):

You can also add your own inline styles if you prefer

view this post on Zulip Edward Ayers (Jul 09 2020 at 09:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"]

view this post on Zulip Edward Ayers (Jul 09 2020 at 10:03):

The other source of widget docs is here

view this post on Zulip 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")

view this post on Zulip Patrick Massot (Jul 09 2020 at 10:08):

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

view this post on Zulip Patrick Massot (Jul 09 2020 at 10:08):

Thanks!

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 09 2020 at 10:18):

Yes, Ed knows. It will be fixed eventually.

view this post on Zulip Kenny Lau (Jul 09 2020 at 10:20):

ok thanks

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 30 2020 at 04:50):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 30 2020 at 05:46):

I have no idea how vm overrides work

view this post on Zulip Bryan Gin-ge Chen (Jul 30 2020 at 05:56):

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

view this post on Zulip Gabriel Ebner (Jul 30 2020 at 07:06):

(deleted)

view this post on Zulip Gabriel Ebner (Jul 30 2020 at 07:07):

Yes, that should work.

view this post on Zulip Edward Ayers (Jul 30 2020 at 10:03):

I think it would be better to override tactic.save_info

view this post on Zulip 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

view this post on Zulip Edward Ayers (Jul 30 2020 at 10:04):

So you shouldn't have to copy that code

view this post on Zulip Edward Ayers (Jul 30 2020 at 10:05):

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

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jul 30 2020 at 10:10):

EDIT: Sorry I misread tactic_view_component as tactic_component

view this post on Zulip 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 (-;

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Jul 30 2020 at 10:21):

it prevents copy paste from the infoview!?

view this post on Zulip Patrick Massot (Jul 30 2020 at 10:33):

Yes, I think several people complained about this recently.

view this post on Zulip Patrick Massot (Jul 30 2020 at 10:34):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/can't.20copy.20in.20widget.20mode

view this post on Zulip Johan Commelin (Jul 30 2020 at 10:40):

Edward Ayers said:

it prevents copy paste from the infoview!?

Not for me

view this post on Zulip Johan Commelin (Jul 30 2020 at 10:41):

It's just that the cover on hover and the cover on select are almost the same

view this post on Zulip Johan Commelin (Jul 30 2020 at 10:41):

So you don't really see that you are selecting something

view this post on Zulip Edward Ayers (Jul 30 2020 at 11:08):

#3633

image.png

view this post on Zulip Gabriel Ebner (Jul 30 2020 at 11:08):

Wow, is this new?

view this post on Zulip Edward Ayers (Jul 30 2020 at 11:08):

fresh from my keyboard

view this post on Zulip Gabriel Ebner (Jul 30 2020 at 11:09):

I think we need to update mathlib's fork of the expression widgets.

view this post on Zulip Edward Ayers (Jul 30 2020 at 11:09):

The above is using the mathlib version rn

view this post on Zulip Gabriel Ebner (Jul 30 2020 at 11:11):

doesnt_show_for_me.png

view this post on Zulip Edward Ayers (Jul 30 2020 at 11:12):

have you co'd #3633 ?

view this post on Zulip Gabriel Ebner (Jul 30 2020 at 11:13):

Ah, I should've read the line above your screenshot. :smile:


Last updated: May 10 2021 at 00:31 UTC