Zulip Chat Archive

Stream: general

Topic: VScode extension


view this post on Zulip Patrick Massot (Jul 25 2018 at 10:41):

@Gabriel Ebner could we get two variants of F12, one creating a new tab if a new file needs to be opened, and one replacing the content of the current tab, as it currently does? Also, could we get key bindings for "Go back" and "Restart Lean"? And maybe one for "Create a comment below the current line, containing what is currently in the Lean messages view"? About Lean messages, each time I press Ctrl+Shift+Enter to open this tab, it also opens a copy of the file I'm currently editing. It's annoying and I think it wasn't like this before.

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:42):

alt-left should be a key binding for "go back"

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:43):

Not here

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:43):

I also noticed the bug with ctrl-shift-enter opening a copy over the message view

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:44):

You can set your key bindings yourself btw

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:45):

It makes me think I would really love to know a way to ask VScode to trigger translation immediately rather than waiting for a blank space of movement. It would really help to type words containing several special unicode characters.

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:45):

How do you setup keybindings?

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:46):

file > prefs > key shortcuts

view this post on Zulip Johan Commelin (Jul 25 2018 at 10:47):

It makes me think I would really love to know a way to ask VScode to trigger translation immediately rather than waiting for a blank space of movement. It would really help to type words containing several special unicode characters.

But how would you deal with prefixes? Such as \t vs \to?

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:47):

this is what emacs does

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:48):

I think if you type \t you get the triangle but underlined, and typing o changes it to an arrow

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:48):

I don't need it to be automatic, I want to be able to ask for it before VScode decides it should do it anyway

view this post on Zulip Johan Commelin (Jul 25 2018 at 10:49):

Sweet. So if I would type \Zp would that give me ℤp?

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:49):

I believe so

view this post on Zulip Johan Commelin (Jul 25 2018 at 10:49):

Nice

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:49):

I think vscode does the same in that case

view this post on Zulip Johan Commelin (Jul 25 2018 at 10:49):

Hmm, maybe it does.

view this post on Zulip Gabriel Ebner (Jul 25 2018 at 10:49):

could we get two variants of F12,

ctrl+k f12 the default keybinding does not work here

But you can assign "open definition to the side" to whatever keybinding you like.

view this post on Zulip Johan Commelin (Jul 25 2018 at 10:50):

I think vscode does the same in that case

You are right.

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:52):

could we get two variants of F12, one creating a new tab if a new file needs to be opened, and one replacing the content of the current tab, as it currently does?

Currently F12 and other navigation commands only replace the content of the current tab if you are viewing a file in temporary mode, indicated with italics in the tab title

view this post on Zulip Mario Carneiro (Jul 25 2018 at 10:53):

you can clear temporary mode by clicking on the title or editing anywhere

view this post on Zulip Gabriel Ebner (Jul 25 2018 at 10:53):

"Go back"

ctrl+alt+- is the default keybinding. I usually use the vim keybindings, where it is ctrl+t as expected.

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:54):

Thanks for pointing out "open definition to the side". But it opens in the area containing Lean messages :(

view this post on Zulip Gabriel Ebner (Jul 25 2018 at 10:55):

Ctrl+Shift+Enter to open this tab, it also opens a copy of the file I'm currently editing

Oh, that seems to be a new bug with vscode 1.25. https://github.com/leanprover/vscode-lean/issues/77

view this post on Zulip Gabriel Ebner (Jul 25 2018 at 10:56):

Thanks for pointing out "open definition to the side". But it opens in the area containing Lean messages :(

You can split the editor first with ctrl+\

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:58):

Thanks, but this creates a whole new zone, not a new tab in the current group

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:58):

Oh, that italic filename is a really subtle clue. I never noticed it

view this post on Zulip Patrick Massot (Jul 25 2018 at 10:59):

It's lunchtime, but I'm happy I've learned a lot of VScode tricks

view this post on Zulip Gabriel Ebner (Jul 25 2018 at 12:25):

Create a comment below the current line, containing what is currently in the Lean messages view

https://github.com/leanprover/vscode-lean/commit/d3ae4b1a1108cb0eb1cefc645b6602a307b4d4be

I'm currently having a bit of trouble publishing the vscode extension, so you'll have to wait a bit for the update.

view this post on Zulip Patrick Massot (Jul 25 2018 at 14:27):

Thanks! Hopefully this example could serve as a pattern for other stuff like that (I have nothing specific in mind).

view this post on Zulip Gabriel Ebner (Jul 27 2018 at 20:12):

I just pushed the update. Please tell me if I broke anything.

view this post on Zulip Gabriel Ebner (Jul 27 2018 at 20:12):

afk hornet in the room

view this post on Zulip Gabriel Ebner (Jul 27 2018 at 20:58):

I managed to escape. The only new feature is "ctrl+shift+p copy contents to comment", which copies the current content of the info view to a comment below the current line, as requested by @Patrick Massot.

view this post on Zulip Chris Hughes (Jul 27 2018 at 21:01):

One slightly annoying new feature of VSCode, is that when I click "Display Goal", it opens the file I have open in the right pane. Is there a way to do anything about that?

view this post on Zulip Simon Hudon (Jul 27 2018 at 21:01):

I've added a feature in emacs (taken from company-coq) to use diff to compare the actual / expected types in error messages. Any chance I might convince you to add it to VS code or help me implement it for VS code?

view this post on Zulip Gabriel Ebner (Jul 28 2018 at 07:35):

it opens the file I have open in the right pane

This bug should be fixed with yesterday's update.

view this post on Zulip Gabriel Ebner (Jul 28 2018 at 07:57):

[..] use diff to compare the actual / expected types in error messages. Any chance I might convince you to add it to VS code or help me implement it for VS code?

Sure, I am happy about new features. How did you extract the expected/actual type from the error message? Regex?

If you want to implement it yourself, look at how _lean.revealPosition is implemented in the info view (this handles the click on the message title and scrolls to the corresponding position in the file): https://github.com/leanprover/vscode-lean/blob/b872639347221a0146bf4e98234ee55e3d634b30/src/infoview.ts#L375
I think we can add a link to the diff right next to it. You can show the diff with workspace.openTextDocument and window.showTextDocument. Feel free to add a diff library to the dependencies.

view this post on Zulip Chris Hughes (Jul 28 2018 at 10:10):

I tried installing the lean VScode update, and now opening VScode instantly freezes my computer. Anyone else experiencing this problem?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 10:13):

If I find the extension in VS code I am only offered "disable" and "uninstall". I seem to be on version 0.11.11 (and on Ubuntu)

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 10:23):

I have extension auto-update on. Which version of the extension are you having problems with? You're talking about a Windows machine right?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 10:24):

More to the point -- the bug is fixed for me and I have no problems with the extension. So I guess I upgraded safely. Anyone on Windows having the same problems with...Chris? Are you on 0.11.11? Oh -- you can't even tell?

view this post on Zulip Chris Hughes (Jul 28 2018 at 10:25):

I'm using the latest version of the extension and 20th April nightly for lean.

view this post on Zulip Chris Hughes (Jul 28 2018 at 10:26):

Maybe I should update lean?

view this post on Zulip Ali Sever (Jul 28 2018 at 10:26):

I reloaded lean, and now mine is crashing too. Thanks a lot Chris

view this post on Zulip Chris Hughes (Jul 28 2018 at 10:32):

It doesn't hang provided I don't open a lean file. I am on 0.11.11

view this post on Zulip Ali Sever (Jul 28 2018 at 10:34):

how did you close your lean files?

view this post on Zulip Chris Hughes (Jul 28 2018 at 10:35):

Reinstall VSCode, and delete the folders containing the information about which lean files I had open

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 10:47):

As a temporary measure you can uninstall the lean extension and then try and figure out how to install an older version. I can't reproduce here on linux; things are working fine for me. Can you switch logging on somehow? This might happen to every Windows user who has auto-update on.

view this post on Zulip Gabriel Ebner (Jul 28 2018 at 10:48):

I just tried to reproduce on windows, but everything works for me. (elan is completely broken for me though)

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 10:49):

Chris can you switch on some debugging output, have the current extension loaded, and then open a Lean file? What happens exactly after you open a lean file? You said your computer freezes? What OS are you using? Win7 or Win10?

view this post on Zulip Chris Hughes (Jul 28 2018 at 10:51):

Win10. My computer totally freezes, I can't even move my mouse.

view this post on Zulip Chris Hughes (Jul 28 2018 at 10:55):

What do you mean by "switch on some debugging output"?

view this post on Zulip Gabriel Ebner (Jul 28 2018 at 11:15):

If everything else fails, can you try to reinstall vscode and lean completely. I am really at a loss here, there are almost no changes between vscode-lean 0.11.9 and 0.11.11, and none that look in any way dangerous. I am running the lean 3.4.1 release on windows 10 and vscode 1.25.1 here.

view this post on Zulip Simon Hudon (Jul 28 2018 at 12:13):

@Gabriel Ebner
If you want to implement it yourself, look at how _lean.revealPosition is implemented in the info view

Thanks! I'll have a look.

Sure, I am happy about new features. How did you extract the expected/actual type from the error message? Regex?

What I did is split the error message into lines and find the line that says "has type:" and I take everything until I find the line announcing the expected type.

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:13):

@Ali Sever I managed to revert my version of the VScode extension. This is how.

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:14):

1. Go into windows command line and type code --disable-extensions

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:15):

2. Open VScode, save everything and uninstall the lean extension. Also disable automatic updates of extensions using ... in the top right of the extensions pane.

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:22):

3. Download the version 0.11.9 os the VScode extension from https://jroesch.gallery.vsassets.io/_apis/public/gallery/publisher/jroesch/extension/lean/0.11.9/assetbyname/Microsoft.VisualStudio.Services.VSIXPackage

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:22):

4. Change the file extension of the downloaded file to .VSIX

view this post on Zulip Chris Hughes (Jul 28 2018 at 15:23):

Go into VScode extension click ... in the top right of the extensions pane and install from VSIX usingthe file you downloaded.

view this post on Zulip Ali Sever (Jul 28 2018 at 15:41):

Thanks Chris, awesome as always

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 17:08):

So I just tried upgrading on a Win10 machine and I've got it working. It did crash VS code -- but a restart of VS code (twice) got it working in the end. It didn't take down the OS.

view this post on Zulip Ali Sever (Jul 28 2018 at 17:15):

by restart do you mean literally close the program and reopen it?

view this post on Zulip Chris Hughes (Jul 28 2018 at 17:16):

I couldn't do that because my computer was frozen.

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 17:16):

The program (but not the OS) hung -- it became unresponsive. I restarted the program twice and got it working. I don't use Windows usually so I don't know if this is normal after an upgrade.

view this post on Zulip Ali Sever (Jul 28 2018 at 17:16):

My pc doesnt freeze, but only the toolbar at the top of VS code works

view this post on Zulip Kenny Lau (Jul 29 2018 at 03:36):

So I opened task manager and discovered that VSCode is quick to take up all of the CPU and memory

view this post on Zulip Moses Schönfinkel (Jul 29 2018 at 07:05):

I've been playing around with this and I can do #eval, #check just fine, but the second I type lemma or theorem, Lean eats all my memory and hits disc to the point the system can't recover. Surprisingly enough example doesn't crash it.

view this post on Zulip Moses Schönfinkel (Jul 29 2018 at 07:15):

Actually it's VS Code that does that (unsurprisingly), because when I close the lean subprocess of VS-code parent, it doesn't fix anything.

view this post on Zulip Gabriel Ebner (Jul 29 2018 at 07:20):

Do you also get the high memory usage with the info view closed (the tab "Lean Messages")?

view this post on Zulip Moses Schönfinkel (Jul 29 2018 at 07:20):

Yes, it doesn't matter whether the info window is open or not. Just to clarify I'm on win 10.

view this post on Zulip Moses Schönfinkel (Jul 29 2018 at 07:24):

I run this off of an HDD, if that helps it completely thrashes the hard drive as well, but this may very well be just a side-effect of memory om-nom.

view this post on Zulip Gabriel Ebner (Jul 29 2018 at 07:26):

Yes, that's just swapping and it's because of the high memory usage. The operating system just moves some stuff from RAM to HDD in order to make space.

view this post on Zulip Gabriel Ebner (Jul 29 2018 at 07:27):

Just to make sure: in the task manager, how much memory does the lean subprocess use compared to the rest of vscode?

view this post on Zulip Moses Schönfinkel (Jul 29 2018 at 07:29):

Negligable if I can even get it to update. The thing is, when I type lemma and I close VS within a second, it recovers. When I type lemma and I close just the lean subprocess of the tree, it doesn't recover. It's gigabytes of memory instantly for VSCode and some dozens of megabytes for lean.

view this post on Zulip Patrick Massot (Jul 29 2018 at 21:43):

I managed to escape. The only new feature is "ctrl+shift+p copy contents to comment", which copies the current content of the info view to a comment below the current line, as requested by @Patrick Massot.

Sorry I'm slow since my family returned from vacations. It works great! Next wish: do you think you could get VScode to offer to fold namespaces and sections like it folds statements and proofs?

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 21:47):

If VS code is capable of knowing which namespace we're in then I would find it super-helpful if this could be displayed in some way -- I sometimes find my cursor in the middle of a large file really wanting to know what namespace I'm in.

view this post on Zulip Patrick Massot (Jul 29 2018 at 21:48):

This would be really really helpful

view this post on Zulip Patrick Massot (Jul 29 2018 at 21:48):

What I'm asking for is easier, but having a substitute to what you're asking for is part of the motivation

view this post on Zulip Gabriel Ebner (Jul 30 2018 at 20:50):

Call for testers: if you are on windows and experience hangs, could you please try this build of vscode-lean: https://1drv.ms/u/s!Au1u53SHpLowhTXMzMxSQI2Jy20o
To install, go to the extension tab, click the three dots, and select "Install from VSIX"

view this post on Zulip Mario Carneiro (Jul 30 2018 at 21:03):

I went through the commits one at a time and the problem is https://github.com/leanprover/vscode-lean/commit/3dc37df of all things

view this post on Zulip Mario Carneiro (Jul 30 2018 at 21:04):

the commit does a bit more than just adding abbreviation as a keyword as it claims; some additional stuff is added to the keyword recognition stuff at the end and I suspect it is triggering a memory leak in the regex parser

view this post on Zulip Mario Carneiro (Jul 30 2018 at 21:08):

More specifically, the regex ([^ \t\n\r{(\[,:]*(,\s*)?)* at the end has the form (a*b?)* which can loop

view this post on Zulip Gabriel Ebner (Jul 30 2018 at 21:12):

Thanks so much for finding this commit!!! I reverted it and published a new version.

view this post on Zulip Gabriel Ebner (Jul 30 2018 at 21:13):

The regex was actually supposed to highlight the bar in mutual def foo, bar. I did not expect a platform-dependent bug in the regex engine here..

view this post on Zulip Mario Carneiro (Jul 30 2018 at 21:17):

I don't think you have to completely revert it; there is nothing wrong with adding abbreviation to the list, only the regex needs to be tweaked so that it doesn't match an infinite number of empty strings

view this post on Zulip Mario Carneiro (Jul 30 2018 at 21:22):

I think this should work for matching a, b in def a, b (the final capturing group): ([^ \t\n\r{(\[,:]+(,\s*[^ \t\n\r{(\[,:]+)*)

view this post on Zulip Kevin Buzzard (Jul 30 2018 at 21:58):

Thanks Mario! This caused my users a certain amount of grief today

view this post on Zulip Johan Commelin (Aug 03 2018 at 07:21):

Gabriel, here is another thing that might be useful. If I have snippet like:

instance : group X :=
{ -- cursor is here
}

view this post on Zulip Johan Commelin (Aug 03 2018 at 07:22):

Then the window displaying the goals knows exactly what is wrong: I need to supply zero and mul and stuff like that.

view this post on Zulip Johan Commelin (Aug 03 2018 at 07:23):

So it would be nice if the autocomplete would show exactly those options. Now I often find myself clicking on the { to see in the Goal Window which stuff I still need to supply.

view this post on Zulip Johan Commelin (Aug 03 2018 at 07:23):

Alternatively, maybe some snippet on steroids could just fill them all in (with sorry's). But my snippet-fu is non-existent.

view this post on Zulip Kenny Lau (Aug 03 2018 at 08:19):

ctrl+alt+shift+enter

view this post on Zulip Johan Commelin (Aug 03 2018 at 08:20):

What the hack is that supposed to do?

view this post on Zulip Johan Commelin (Aug 03 2018 at 08:20):

Is there a way to ask VScode "Hey, what does the shortcut do?"?

view this post on Zulip Kenny Lau (Aug 03 2018 at 08:20):

it lets you view all the messages

view this post on Zulip Kenny Lau (Aug 03 2018 at 08:20):

instead of just the one on your line

view this post on Zulip Kevin Buzzard (Aug 03 2018 at 09:09):

The window on the bottom which displays the errors and warnings is the place to look for this. Sometimes you have to pull it into existence

view this post on Zulip Johan Commelin (Aug 03 2018 at 09:12):

Cool! I didn't know I could pull something up there!

view this post on Zulip Johan Commelin (Aug 10 2018 at 07:30):

In VScode, if I select some text that is to be replaced, and I start typing a string the expected behaviour occurs. Except... Except when I start the replacement string with a \, then it is not expanded into a unicode character. So if I select "foobar" and then type \lam x y, I don't get a cool lambda.

view this post on Zulip Johan Commelin (Aug 10 2018 at 07:30):

@Gabriel Ebner :up:

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 10:30):

I deal with this by writing what I want beforehand and copying it with ctrl-x into the whatever-that-thing-is-called buffer so I can use ctrl-v to paste when I'm replacing

view this post on Zulip Kenny Lau (Aug 10 2018 at 10:31):

I deal with this by selecting "foobar", deleting the text, and then type \.

view this post on Zulip Johan Commelin (Aug 10 2018 at 10:34):

Right, I use both those way to deal with it. Still, I thought I would mention it, because maybe there is an easy fix. And sometimes I forget to deal with, and then :cry:

view this post on Zulip Gabriel Ebner (Aug 10 2018 at 10:38):

I'm not sure I understand this correctly. You write foobar and then want λ x, f instead. So instead of deleting foobar, you select it and then start typing \lam x, f?

view this post on Zulip Johan Commelin (Aug 10 2018 at 10:38):

Right

view this post on Zulip Gabriel Ebner (Aug 10 2018 at 10:39):

This shouldn't be too hard to add. I just never used an editor like that.

view this post on Zulip Johan Commelin (Aug 10 2018 at 10:40):

For me it would usually be ciw\lam x ,y... still need to look at lean.vim and all those other plugins for the LSP.

view this post on Zulip Gabriel Ebner (Aug 10 2018 at 10:41):

I'm a vim addict as well. There is a pretty good vim plugin for vscode that I'm using: https://github.com/VSCodeVim/Vim .
And ciw\lam x ,y works as expected!

view this post on Zulip Johan Commelin (Aug 10 2018 at 10:42):

Ok, I should try that out.

view this post on Zulip Johan Commelin (Aug 10 2018 at 10:43):

Otoh, if I get actual vim working, then I could run lean on a server, and connect via mosh. Then my crappy laptop would have superfast Lean!

view this post on Zulip Gabriel Ebner (Aug 10 2018 at 10:48):

And it should work in the latest version of the vscode extension.

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 12:37):

You could just do this with emacs, right?

I should prod William about CoCalc. I am writing an introductory worksheet for beginning UGs teaching basic logic, using Sphinx and "try it!". I realised that no undergraduate would even be able to do my first maths example sheet unless they know how to construct and destruct or/and etc.

view this post on Zulip Johan Commelin (Aug 10 2018 at 15:24):

I should prod William about CoCalc.

Yes! I would love to hear more updates from CoCalc.

view this post on Zulip Gabriel Ebner (Aug 13 2018 at 16:41):

Gabriel, here is another thing that might be useful. If I have snippet like:

instance : group X :=
{ -- cursor is here
}

Then the window displaying the goals knows exactly what is wrong: I need to supply zero and mul and stuff like that.
So it would be nice if the autocomplete would show exactly those options.

This will probably not happen in Lean 3.

view this post on Zulip Kenny Lau (Aug 18 2018 at 21:26):

Ctrl+A is not working for me (I'm on Windows 10)

view this post on Zulip Kenny Lau (Aug 18 2018 at 21:31):

wait it works now

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:08):

@Gabriel Ebner While in Orsay we had some dreams and fantasies... they're recorded over here: https://github.com/leanprover-community/mathlib/wiki/VScode-wishlist :stuck_out_tongue_wink:

view this post on Zulip Patrick Massot (Aug 30 2018 at 18:17):

some of them would probably need a more detailed description for people who didn't attend the dicussion

view this post on Zulip Gabriel Ebner (Aug 30 2018 at 18:19):

I think I can make sense of most of them. It reads like a wishlist for Lean 4.
What is "help with naming conventions"?

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:20):

"Help with naming conventions": Given a statement, figure out the name.

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:21):

I don't know much about Lean 4. But we also decided that we were to often saying: "That might be easier in Lean 4" etc...

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:23):

[kidding] Oooh, and we want MS Word's Clippy for Lean: "It looks like you are trying to prove something by induction. Would you like me to write the skeleton of the proof for you?" [/kidding]

view this post on Zulip Chris Hughes (Aug 30 2018 at 18:23):

Can I add pp option to display types of proofs in your goal or local context as well. Maybe target types of coercions as well.

view this post on Zulip Gabriel Ebner (Aug 30 2018 at 18:45):

I'm just saying that most points on the list are either infeasible right now, or shouldn't go into the vscode extension.
If you want to start experimenting right now, I think the naming convention automation is the lowest hanging fruit. You can implement #how_do_you_call ∀ x y, x < y → x - y = 0 as a user command for example.

view this post on Zulip Gabriel Ebner (Aug 30 2018 at 18:51):

The next best is maybe "turn current goal into lemma". You can do this as a tactic that outputs the text for the lemma as an error message. The user can then copy&paste it where they want. Last time I talked with Rob and Johannes there was the suggestion to parse tags like <insert-above>lemma foo : a → b := sorry</insert-above> in the error messages, but imho that's a bit too hacky unless there is a significant need for it.

view this post on Zulip Gabriel Ebner (Aug 30 2018 at 18:52):

For the other "clippy" and refactoring stuff, I'd really wait.

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:56):

Clippy was not really serious...

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:56):

The turn goal into lemma tactic would be really cool I think.

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:57):

And I might even be able to write it with a bit of help.

view this post on Zulip Johan Commelin (Aug 30 2018 at 18:57):

#how_do_you_call would be awesome, and I have no clue whatsoever how to write it.

view this post on Zulip Johan Commelin (Aug 31 2018 at 12:55):

@Gabriel Ebner Currently \func points to an arrow that is frozen by core. We thought that it might be useful to point it to instead, so that we can use that arrow for functors in the category lib.

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:03):

Ah I see, is already used for the relators. Another unused option is , written \==>.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 13:04):

I think that this is used for natural transformations

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:05):

Yes, that would've been my next question. What about morphisms and natural transformations?

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:05):

\hom and \==>

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:06):

It is really \func that's been messed up. For the rest we have nice solutions.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:07):

Really the thing for relators should have been local notation. Then you wouldn't have to do anything.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:07):

Now we are kindly asking you to point \func to this goofy arrow that looks enough like what we want.

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:10):

I definitely agree on the local notation part. I'd just like to avoid changing existing abbreviations if possible.

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:11):

You can easily add the arrow yourself: just add a new line with "func": "⟹", to this json file https://github.com/leanprover/vscode-lean/blob/master/translations.json#L1290 and make a PR.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:12):

Right... I'm currently doing something slightly related... writing a Python script that turns that file into Compose-key sequences.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:14):

So I should not overwrite \functor? But adding \func is ok?

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:14):

I feel like we need a separate repository for this file and all associated scripts soon. I have also written a converter: https://github.com/gebner/m17n-lean

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:15):

As I said, I'd rather avoid overwriting. But I'm happy either way.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:16):

I guess no-one is using that abbreviation at the moment. So I'dd rather overwrite. Chances are way higher that someone will write \functor when doing categories.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:16):

https://github.com/jcommelin/vscode-lean/pull/1

view this post on Zulip Sean Leather (Aug 31 2018 at 13:16):

I feel like we need a separate repository for this file and all associated scripts soon. I have also written a converter: https://github.com/gebner/m17n-lean

I've thought something similar, in particular for providing a single source for VS Code, Emacs, and Vim keybindings.

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:16):

Ok, then. You can still get the old arrow with \r= etc.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:17):

Exactly

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:17):

@Johan Commelin You made a PR to your own fork.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:17):

Oops, that is silly

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:20):

https://github.com/leanprover/vscode-lean/pull/85

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 13:23):

And deployed.

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:25):

@Scott Morrison Voila! You can update the arrow for functors in your lib!

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:26):

import fileinput
import re

pat = re.compile('"(.*)":"(.*)"', re.MULTILINE)

for line in fileinput.input():
    m = pat.match(line)
    pre = m.group(1)
    suf = m.group(2)
    hooked_pre = [ '<' + c + '>' for c in list(pre) ]
    s = '<Multi_key> ' + ' '.join(hooked_pre) + ' : "' + suf + '"    # ' + pre
    print(s)

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:27):

That's the silly thing that I'm trying

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:45):

@Gabriel Ebner By the way, if the original arrow becomes unfrozen in Lean 4, then we might want to switch back...

view this post on Zulip Mario Carneiro (Aug 31 2018 at 13:50):

are you going to claim it as a global notation?

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:55):

Of course! We are evil!

view this post on Zulip Mario Carneiro (Aug 31 2018 at 13:56):

I'm only allowing the notations in category theory now because the arrows are bizarre

view this post on Zulip Johan Commelin (Aug 31 2018 at 13:59):

Any arrow that is not bizarre can be local. That's fine with me. We'll be locally evil.

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:28):

Gabriel, why do you hardcode the leader key?

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 14:49):

Leader = backslash? It used to be backslash in emacs, and I just copied that. There is no fundamental reason why it has to be a backslash. What do you have in mind, §? We can easily support that with a configuration option. I don't know whether we could support "right-control" as a leader key at all.

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:50):

Yes, I mean leader as in vim terminology. The point is that \ is very inconvenient on a French keyboard. In vim I always use comma for that

view this post on Zulip Mario Carneiro (Aug 31 2018 at 14:50):

wouldn't comma give you a lot of false positives?

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:50):

only if the abbreviation starts with a space

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:51):

comma is always followed by space (at least in France)

view this post on Zulip Mario Carneiro (Aug 31 2018 at 14:51):

it's usually followed by a space in mathlib, but there are a significant fraction with no space

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:52):

under what kind of circumstances?

view this post on Zulip Mario Carneiro (Aug 31 2018 at 14:53):

λ⟨a,b⟩, and such

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:53):

this is wrong

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:53):

should be a, b

view this post on Zulip Mario Carneiro (Aug 31 2018 at 14:53):

also between rewrite rules and simp rules sometimes

view this post on Zulip Mario Carneiro (Aug 31 2018 at 14:53):

I agree, I try to keep a space after a comma but not everyone does

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:54):

So switching to comma would improve typography in mathlib!

view this post on Zulip Johan Commelin (Aug 31 2018 at 14:54):

You could map your CAPS LOCK key to §, and then use that as a leader.

view this post on Zulip Johan Commelin (Aug 31 2018 at 14:54):

Or just map your caps lock to \

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 14:55):

I thought French keyboards have a key for §?

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:55):

no

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:56):

https://fr.wikipedia.org/wiki/Fichier:Clavier-Azerty-France.svg

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 14:56):

Oh, so wikipedia has been lying to me. I thought it is right next to shift. https://en.wikipedia.org/wiki/AZERTY#/media/File:Azerty_fr.svg

view this post on Zulip Johan Commelin (Aug 31 2018 at 14:57):

It seems to be Shift + !

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 14:57):

That picture also shows § right next to the right shift key?

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:57):

it's there, but not on direct access

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:57):

it's better than \ which is really hard to type, but comma is direct access

view this post on Zulip Johan Commelin (Aug 31 2018 at 14:58):

Make ù the leader (-;

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:00):

indeed this would also probably be fine (this character is used in only one word)

view this post on Zulip Edward Ayers (Aug 31 2018 at 15:02):

On a different subject: are there any plans to add a code formatter to vscode extension?

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 15:03):

I think there are plans to add a code formatter to Lean 4.

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:04):

what is a code formatter?

view this post on Zulip Edward Ayers (Aug 31 2018 at 15:05):

what is a code formatter?

You slam a button and it adds spaces in the proper places and enforces some style guide things.

view this post on Zulip Edward Ayers (Aug 31 2018 at 15:05):

Basically it adds and removes spaces until the code looks nice

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:07):

that would be really nice

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 15:16):

Presumably it only works for code which can be made to look nice by addition and removal of spaces

view this post on Zulip Edward Ayers (Aug 31 2018 at 15:17):

I think that you can in theory perform arbitrary textual transformations

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 15:38):

Coming soon to a vscode near you. I'm on vacation now, @Sebastian Ullrich can publish updates to the vscode extension if there's anything urgent.

view this post on Zulip Bryan Gin-ge Chen (Aug 31 2018 at 15:41):

On a different subject: are there any plans to add a code formatter to vscode extension?

There's also an open issue on the lean repository related to this here.

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:50):

Thank you very much Gabriel! Together with the TAB thing it really makes Leaning more comfortable

view this post on Zulip Ali Sever (Sep 02 2018 at 08:52):

My windows updated and now vscode says lean doesn't work. I tried using lean --version and I got "segmentation fault". Even if I use PATH ***, I can't get lean --version to work. Any suggestions?

view this post on Zulip Ali Sever (Sep 03 2018 at 17:23):

@Mario Carneiro Hi Mario, I recently had an issue with a windows insider update which completely prevented me from using lean. Kevin told me that I should warn you about this, since there's a chance that whatever caused this might be in the next windows update (which google says is on October 10th). I'm afraid I can't help you much about the error, but I've put everything I know here https://github.com/leanprover/lean/issues/1972.

view this post on Zulip Kenny Lau (Sep 04 2018 at 09:12):

2018-09-04.png

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 09:31):

Do you know about ``` ? It makes your code easier to cut and paste ;-)

view this post on Zulip Kenny Lau (Sep 04 2018 at 09:34):

variables (A : Type*)
class MWE extends has_zero A

view this post on Zulip Johan Commelin (Sep 04 2018 at 09:34):

Also, why did you put that in this thread?

view this post on Zulip Kenny Lau (Sep 04 2018 at 09:35):

because it's about VScode

view this post on Zulip Patrick Massot (Sep 04 2018 at 09:39):

I guess Kenny wants to complain about syntax highlighting

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 10:00):

Oh I see. He's as cryptic as ever :-)

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2018 at 13:08):

set_option class.instance_max_depth 5

This one looks weird too (with class colored differently from .instance_max_depth

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2018 at 13:38):

I've submitted a PR for Kenny and my examples.

view this post on Zulip Kenny Lau (Sep 05 2018 at 18:25):

I just discovered that you can indent a bunch of lines by highlighting them and then pressing ctrl+], and de-indent by ctrl+[

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:26):

Alternative: Tab or Shift-Tab

view this post on Zulip Patrick Massot (Sep 05 2018 at 18:26):

also works with Tab and Shift-Tab

view this post on Zulip Kenny Lau (Sep 05 2018 at 18:26):

oh right

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:29):

Also, you should learn Vim, so that you can be disgusted by Ctrl-[ being a shortcut for something silly like that (-;

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 18:30):

Did you try \G?

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 18:30):

that's even more bizarre

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:32):

Right, that should clearly expand to α.

view this post on Zulip Patrick Massot (Sep 05 2018 at 18:34):

Same with \R (for rings) and \M (for modules), they should expand to α

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 18:43):

I am writing some Noetherian code and of course using Mario's work on Noetherian modules, and you can tell exactly who wrote each line because of this convention :-)

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 18:54):

Same with \R (for rings) and \M (for modules), they should expand to α

or maybe \beta, depending on...um...a random choice I guess

view this post on Zulip Bryan Gin-ge Chen (Sep 05 2018 at 23:31):

Has anyone had any luck with the "Bracket pair colorizer" extension that's suggested in the readme? It doesn't seem to work (on lean files) right out of the box (perhaps because lean doesn't appear on the Prism.js list of languages), though I like how it looks on other filetypes.

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:41):

I opened my file called dfinsupp_quotient.lean in VSCode, and then closed it, and then rebuilt Lean, and then rebuilt mathlib, and then opened it again in VSCode, but its content was suddenly gone.

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:42):

my file is independent from mathlib, it's in my own sandbox

view this post on Zulip Chris Hughes (Sep 07 2018 at 13:43):

Sounds like you didn't save. Did you open if from a file explorer, or just open VScode, and it was there because it was the last thing you were looking at?

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:44):

I always save my file after I type every word

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:44):

the latter

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:45):

also, now, whenever I open VSCode a second tab would magically appear, and the name of the tab would be "null", and whenever I click on "null" it would disappear

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:46):

2018-09-07-2.png

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:46):

whenever I click on the tab "null", the tab "null" itself would disappear

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:47):

I don't really mind spending the next day retyping everything, I just want to make sure that it won't happen again

view this post on Zulip Chris Hughes (Sep 07 2018 at 13:51):

What happens if you open from a file explorer?

view this post on Zulip Kenny Lau (Sep 07 2018 at 13:51):

it is also empty

view this post on Zulip Kenny Lau (Sep 08 2018 at 08:37):

Ctrl+space does not show the defining fields of a structure/inductive/class, such as filter.univ_sets

view this post on Zulip Kenny Lau (Sep 08 2018 at 08:40):

hmm, it does show filter.univ_sets.

view this post on Zulip Kenny Lau (Sep 08 2018 at 08:40):

But I do remember there are some things that Ctrl+Space doesn't show

view this post on Zulip Chris Hughes (Sep 08 2018 at 09:28):

Sometimes it doesn't show things in a namespace that you have open if you type finset.x instead of x

view this post on Zulip Kevin Buzzard (Sep 08 2018 at 10:15):

In my experience sometimes it doesn't show something, and then you hit escape and then ctrl-space again, and then it shows them, although I noted this behaviour months ago and cannot say for sure that it still occurs.

view this post on Zulip Kenny Lau (Sep 08 2018 at 21:28):

Is there a quick way to change (lorem ipsum dolor) to {lorem ipsum dolor} etc?

view this post on Zulip Mario Carneiro (Sep 08 2018 at 21:33):

you can use Select to Bracket (no default key command)

view this post on Zulip Bryan Gin-ge Chen (Sep 08 2018 at 21:49):

The vim incantation %r}``r{ would do this, but unfortunately it doesn't work in the VScode vim extension yet (maybe soon?).

view this post on Zulip Olli (Sep 08 2018 at 21:53):

VSCode's vim extension has a feature from vim-surround enabled by default, so cs)} works

view this post on Zulip Bryan Gin-ge Chen (Sep 08 2018 at 22:47):

Cool, I didn't know that! However, on my macOS system, the "surround" commands don't work when the lean extension is enabled. They do work on my windows machine (and when I disable the lean extension, or on non-lean files). Very strange...

view this post on Zulip Bryan Gin-ge Chen (Sep 08 2018 at 22:48):

When I type cs on my mac with the lean extension enabled, it deletes the whole line and puts me in insert mode.

view this post on Zulip Bryan Gin-ge Chen (Sep 08 2018 at 22:52):

Oh wait it's working now. No idea what's going on.

view this post on Zulip Kenny Lau (Sep 09 2018 at 12:57):

Is there a way to see which file is being compiled?

view this post on Zulip Keeley Hoek (Sep 10 2018 at 03:50):

When an identifier that ends with number has an error message, only the part up to the number is underlined. Moreover, clicking an identifier which ends with a number will not highlight its usages in the rest of the open file, as usually happens

view this post on Zulip Bryan Gin-ge Chen (Sep 10 2018 at 03:56):

The same things happen with dots, though maybe the current highlighting behavior is preferable in that case.

view this post on Zulip Keeley Hoek (Sep 12 2018 at 17:14):

Is there a fundamental reason why the partial tactic.trace ... output of a tactic is only displayed in the editor after tactic execution has completed (commonly, failed)?

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 17:26):

Yeah, the current server protocol doesn't really allow for another (efficient) option. I've thought about this, but it's not clear at all how this could work especially when we move to storing messages in an immutable Lean data structure.

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:26):

2018-09-13.png
misplaced red underscore

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:27):

code:

example : nat := (_)
example : nat := (_ : nat)

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:27):

line 1 is normal, line 2 is not

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 08:03):

Ned Summers showed me examples of this which were really crazy -- he seemed to be able to move the red line an arbitrary amount to the left :-)

view this post on Zulip Patrick Massot (Sep 13 2018 at 08:03):

I guess this has nothing to do with VScode. The problem should be in lean server mode, no?

view this post on Zulip Gabriel Ebner (Sep 13 2018 at 12:38):

"Moving error messages an arbitrary amount to the left" is a known bug in the presence of calligraphic characters. Please just don't write errors when using calligraphic (or fraktur) characters.

view this post on Zulip Gabriel Ebner (Sep 13 2018 at 12:39):

The problem is that vscode counts the number of utf-16 words (2 bytes), while lean counts the number of Unicode codepoints (can be larger than 2 bytes).

view this post on Zulip Johan Commelin (Sep 13 2018 at 12:44):

Ouch... does it make sense to report this bug to VScode? Or is it not worth it?

view this post on Zulip Gabriel Ebner (Sep 13 2018 at 12:48):

It's by design I think. The language server protocol specifies this behavior explicitly. There is an issue in the github repo, but I am not sure if they'll ever change it. Note that JavaScript also uses this utf-16 indexing for strings.

view this post on Zulip Gabriel Ebner (Sep 13 2018 at 12:49):

There is another possible bug. Vscode and lean also disagree on what line endings are recognized. Vscode recognizes \r, but lean doesn't.

view this post on Zulip Johan Commelin (Sep 13 2018 at 12:51):

Lean is pretty sane. :big_smile:

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 12:51):

Indeed Ned was doing category theory and there were calligraphic C's everywhere. Rather took me by surprise when I first saw it!

view this post on Zulip Johan Commelin (Sep 13 2018 at 12:52):

Could you do a man-in-the-middle on the Lean - VScode communication?

view this post on Zulip Johan Commelin (Sep 13 2018 at 12:52):

Somehow VScode is able to deal with Unicode characters, even if they use more then 2 bytes.

view this post on Zulip Johan Commelin (Sep 13 2018 at 12:53):

If the Lean extension would be able to detect this behaviour, you could manually adjust the coordinates of the red line.

view this post on Zulip Johan Commelin (Sep 13 2018 at 12:53):

Admittedly this is very hacky, and probably not really worth it.

view this post on Zulip Gabriel Ebner (Sep 13 2018 at 12:56):

Yes that's the way to fix it. You need to manually translate all the positions in Vscode.

view this post on Zulip Gabriel Ebner (Sep 13 2018 at 12:57):

The way you encode calligraphic characters in utf-16 is two use 2 2-byte words. In utf-8 you need 4 bytes.

view this post on Zulip Keeley Hoek (Sep 13 2018 at 13:04):

Every time I have to write a newline character in a string I have to do it twice because it always autocorrects into a reverse set inclusion :'(

view this post on Zulip Gabriel Ebner (Sep 13 2018 at 13:26):

Does \\n work?

view this post on Zulip Kenny Lau (Sep 13 2018 at 14:08):

But my example has bo calligraphic characters!

view this post on Zulip Keeley Hoek (Sep 13 2018 at 14:18):

@Gabriel Ebner can I pay you real money? :D awesome

view this post on Zulip Kenny Lau (Sep 30 2018 at 08:24):

sometimes in the middle of the proof, when I type something (say abcde), then after I finish, I see the state after typing a, and then after typing b, and then after typing c, and then after typing d, and then after typing e, resulting in the situation that I have to wait a while before I can see the result

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:24):

Is your cursor unusually slow?

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:25):

or typing

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:25):

Or is it just lean being behind VSCode

view this post on Zulip Kenny Lau (Sep 30 2018 at 08:25):

the cursor is fine, and so is my typing

view this post on Zulip Kenny Lau (Sep 30 2018 at 08:26):

oh and sometimes after I type something, suddenly the whole file is starting to compile and I have to wait a while again

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:27):

That latter problem has hit me many times

view this post on Zulip Kenny Lau (Sep 30 2018 at 08:28):

returning to the previous problem, if I copy and paste abcde, then I see the end result instantaneously, so it isn't lean being behind VSCode either

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:28):

I believe sometimes when you mouse over something vscode makes an info request which requires lean to open and compile a new file

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:29):

It might be that the cost of error reporting is high?

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:29):

so that the partial results take longer to compile

view this post on Zulip Kenny Lau (Sep 30 2018 at 08:33):

shouldn't it stop compiling when I enter a new letter?

view this post on Zulip Mario Carneiro (Sep 30 2018 at 08:33):

it should, but it may also take some time for the interrupt to be accepted

view this post on Zulip Kenny Lau (Oct 02 2018 at 15:21):

oh and sometimes after I type something, suddenly the whole file is starting to compile and I have to wait a while again

I really hope they can remove this "feature"

view this post on Zulip Kevin Buzzard (Oct 02 2018 at 15:22):

Is this a Windows-only feature? I am not sure I have experienced it on linux.

view this post on Zulip Patrick Massot (Oct 02 2018 at 15:49):

I think I never saw this (I'm also using Linux)

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2018 at 16:27):

If you're referring to the fact that the info view window goes blank for long periods while typing (inconsistently depending on the type of input?), I've also experienced this on both Mac and Windows and I complained about it here. I wasn't able to figure out how to fix the underlying issue, but as a workaround, I submitted a PR which allows you to assign a keystroke to toggle pausing the infoview. So now I just hit my keybind for lean.infoview.toggleUpdatingbefore typing, and hit it again when I'm done, which feels somewhat better.

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2018 at 16:30):

Has anyone had any luck with the "Bracket pair colorizer" extension that's suggested in the readme? It doesn't seem to work (on lean files) right out of the box (perhaps because lean doesn't appear on the Prism.js list of languages), though I like how it looks on other filetypes.

As an update, the new version of that extension, "Bracket Pair Colorizer 2" currently works out of the box with Lean, though it's still in alpha.

view this post on Zulip Scott Morrison (Oct 02 2018 at 21:59):

I've definitely seen Kenny's issue on macOS. I think the diagnosis is that your mouse has accidentally hovered over something, VS Code has decided to open a file in the background in order to provide a tooltip, and this has caused a cascade of recompilations.

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 07:15):

I only ever run lean with a complete bunch of .olean files for all of mathlib. Does this behaviour still occur in this situation?

view this post on Zulip Scott Morrison (Oct 03 2018 at 08:58):

Probably not.

view this post on Zulip Kevin Buzzard (Oct 03 2018 at 09:41):

Then this might be the reason I don't see this behaviour in my set-up (i.e. nothing to do with the OS)

view this post on Zulip Patrick Massot (Oct 03 2018 at 09:41):

It's clearly much easier to work on something else than mathlib, for this reason

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:23):

Whenever I type /-, I automatically get -/, which is inconvenient at times. Before yesterday, it is smarter, in the sense that when I don't want -/ it really doesn't give me -/.

view this post on Zulip Kenny Lau (Oct 11 2018 at 15:25):

sometimes when I'm in (checking visible lines and above mode), everything suddenly stops updating

view this post on Zulip Kenny Lau (Oct 11 2018 at 15:25):

and I need to close and reopen VSCode

view this post on Zulip Gabriel Ebner (Oct 11 2018 at 16:32):

Known bug in the lean C++ code. That's why the default changed back to "visible files" a few months back.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 10:26):

Is this a bug in VS Code? I'm using Ubuntu 18.04. vscodebug1.png vscodebug2.png vscodebug3.png

After I hover over "U" in the git stuff, my output when I hover over "+" is corrupted. I can get it back by hovering over e.g. "discard changes".

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 10:28):

curses, did not capture mouse, sorry. Hover over "U" in git pane to open this menu.

view this post on Zulip Gabriel Ebner (Oct 13 2018 at 10:31):

Probably a bug in electron (vscode uses electron (= essentially a distribution of the chrome (well, chromium) web browser) as the gui library). https://bugs.chromium.org/p/chromium/issues/detail?id=442111

view this post on Zulip Simon Hudon (Oct 13 2018 at 11:28):

That's a very lisp-y answer

view this post on Zulip Kenny Lau (Nov 05 2018 at 14:57):

I tried to open a lean file from explorer (I'm using Windows) and then I discovered that my workspace is gone

view this post on Zulip Johan Commelin (Nov 15 2018 at 09:53):

@Gabriel Ebner How hard would it be to implement a toggle that enables/disables whether Lean is interactive. Sometimes I would like to disable the interactivity to paste a chunk of "almost-Lean" (for example from the goal window) and massage it into Lean-code. After that, I would reenable interactivity, so that the code would be sent of to the server.
In this way, you wouldn't have the server constantly choking on the almost-Lean code, of which you already know that it won't parse...

view this post on Zulip Johan Commelin (Nov 15 2018 at 09:53):

This might be a first step towards a "Turn this goal into a lemma" functionality in VScode

view this post on Zulip Gabriel Ebner (Nov 15 2018 at 10:00):

Well, the two features are completely independent.
For the "pause" feature, I think the easiest way would be prevent syncing the file contents here: https://github.com/leanprover/vscode-lean/blob/d70dfa121bc616100c14bc0fd24400b9962922da/src/sync.ts#L36 You'd probably also want to disable autocompletion, hover, go-to-definition, etc. in that mode.
Add a command to toggle the pause flag, and when unsetting it, resync all files. There is theoretically also an option in the roi setting (press on the Lean item in the status bar, and then select "nothing"); but the server still recompiles stuff for autocompletion etc.

view this post on Zulip Johan Commelin (Nov 15 2018 at 10:04):

Right, they are completely independent, but they would work together pretty well.

view this post on Zulip Johan Commelin (Nov 15 2018 at 10:04):

I think stuff like autocompletion could still be useful in the "pause" mode.

view this post on Zulip Johan Commelin (Nov 15 2018 at 10:05):

At least when you are working on "almost-Lean" code.

view this post on Zulip Johan Commelin (Nov 15 2018 at 10:06):

Otherwise I could also just edit inside a comment block. But I would like to have some of the cheaper interaction, like syntax highlighting and autocompletion.

view this post on Zulip Johan Commelin (Nov 15 2018 at 10:07):

Anyway, I have never worked with typescript before, and I have no idea where to start if I would want to modify the VScode extension. But I would certainly like to learn this. Has someone ever twitched work on the Lean-VScode extension?

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2019 at 15:42):

Is anyone else seeing broken pause / continue icons in the tactic state since the latest VS code update (1.31.0)?

view this post on Zulip Johan Commelin (Feb 13 2019 at 12:35):

This is a very minor feature request: In the tactic state, could we always display the number of goals?
Here is my very elaborate motivation for this silly request.
Think of someone who has never seen Lean before. You are demo-ing Lean to them. They are looking closely to the piece of code that you are writing, and suddenly they see in their peripheral vision that the entire tactic state has changed. What happened!!! (Don't worry, nothing happened, we just went from 1 goal to 2 goals, and therefore the entire context of the main goal shifted down one line.)
It's really minor, but I think it decreases the mental discomfort by several epsilons...

view this post on Zulip Johan Commelin (Feb 13 2019 at 12:41):

Also, feedback from my significant other: she thought that "no goals" sounded somewhat depressed. I know we had the :tada: emoji at some point. That was maybe a bit unprofessional. But (related to above) if we display the number of goals all the time, it would already say "0 goals". And maybe on the line below it could say "proof completed". I don't know... better suggestions are welcome. Just trying to make things slightly more intuitive for absolute newbies.

view this post on Zulip Neil Strickland (Feb 13 2019 at 12:51):

I think that that is a good suggestion. However, I would like to modify it for the case where you have finished with the current goal inside a set of curly brackets, but there are more goals waiting outside the curly brackets. I am not sure what would be a good newbie-comprehensible message for that.

view this post on Zulip Johan Commelin (Feb 13 2019 at 12:53):

"subproof completed"?

view this post on Zulip Neil Strickland (Feb 13 2019 at 12:54):

Yes, that's probably good.

view this post on Zulip Kevin Buzzard (Feb 13 2019 at 12:55):

"Achievement unlocked". And a little happy sound.

view this post on Zulip Kenny Lau (Feb 13 2019 at 13:29):

what if there are no goals but the result state contains metavariables

view this post on Zulip Johan Commelin (Feb 13 2019 at 13:34):

Ooh, those are edge cases (-; Just show some unrelated error message :upside_down:

view this post on Zulip Edward Ayers (Feb 13 2019 at 15:57):

I had a look in to doing this: the problem is that the code which governs this behavior is in Lean's C++. So to do this (without changing Lean) one would have to intercept the info-view message in vscode and then add back in the goal count message which is a little kludgy.

view this post on Zulip Johan Commelin (Feb 13 2019 at 15:58):

Hmm, too bad... Thanks for looking into it though!

view this post on Zulip Edward Ayers (Feb 13 2019 at 16:05):

There will be a way to get the number of goals directly from the language server and then display it somewhere else which might make sense.

view this post on Zulip Bryan Gin-ge Chen (Feb 13 2019 at 16:08):

I'm working on a PR for this... it's just doing the "kludgy thing" though.

view this post on Zulip Edward Ayers (Feb 13 2019 at 16:10):

For reference it's line 235 in src/library/tactic/tactic_state.cpp.

view this post on Zulip Johan Commelin (Feb 13 2019 at 16:14):

@Bryan Gin-ge Chen Thanks for doing this!

view this post on Zulip Edward Ayers (Feb 13 2019 at 16:15):

Is anyone else seeing broken pause / continue icons in the tactic state since the latest VS code update (1.31.0)?

I'm seeing this now I've upgraded to vscode 1.31.0 on macOS

view this post on Zulip Gabriel Ebner (Feb 13 2019 at 16:20):

Is anyone else seeing broken pause / continue icons in the tactic state since the latest VS code update (1.31.0)?

I'm seeing this now I've upgraded to vscode 1.31.0 on macOS

This should be fixed in vscode 1.31.1.

view this post on Zulip Bryan Gin-ge Chen (Feb 13 2019 at 16:33):

https://github.com/leanprover/vscode-lean/pull/114

view this post on Zulip Bryan Gin-ge Chen (Feb 13 2019 at 16:36):

I didn't try to implement Neil's suggestion, so for now it just says "proof completed" whenever there are "0 goals".

view this post on Zulip Gabriel Ebner (Feb 13 2019 at 16:47):

I'm not completely against it, but there was a huge community backlash the last time we modified the tactic state output... @Mario Carneiro You expressed a strong opinion against :tada: the last time. Is proof completed and 1 goal more acceptable?

view this post on Zulip Joseph Corneli (Feb 13 2019 at 16:48):

calvin.png

view this post on Zulip Bryan Gin-ge Chen (Feb 13 2019 at 17:09):

I just noticed something else which is that if I have the infoview window selected in a vscode lean and then reopen vscode, the extension auto-opens a webview in column Three, leaving a blank column in the middle.

I think this happens because the editor object that's passed to openPreview is undefined if the previously selected window was the infoview and the default column is set to Three here. Could we fix this by just changing this to Two, or is there a reason it should be Three here? @Gabriel Ebner

view this post on Zulip Mario Carneiro (Feb 13 2019 at 17:30):

I experienced "no goals blues" in office hours yesterday as well. "Proof completed" sounds good, although you also get "no goals" at the end of subgoal blocks (i.e. before })

view this post on Zulip Bryan Gin-ge Chen (Feb 13 2019 at 17:33):

Yeah, that was basically Neil's point. I thought about having it say "(sub)proof completed" instead but then decided that looked ugly and might be more confusing. But I'm open to suggestions.

view this post on Zulip Johan Commelin (Feb 13 2019 at 17:33):

We could display "0 goals: (sub)proof completed" to avoid confusion, where people think the whole proof is done, but it was only a subproof...

view this post on Zulip Johan Commelin (Feb 13 2019 at 17:33):

Lol... (great minds think alike, and all that...)

view this post on Zulip Johan Commelin (Feb 21 2019 at 08:08):

I'm just back from a department retreat in the Black Forest where I gave a talk on Lean for my department. Several people were confused about no goals. ("Soccer matches with 'no goals' are extremely disappointing.") Anyway, some people suggested goals accomplished. I think that is quite good.

view this post on Zulip Bryan Gin-ge Chen (Feb 21 2019 at 15:29):

Sounds good to me, I've updated the PR.

view this post on Zulip Kevin Buzzard (Mar 23 2019 at 20:41):

Anyway, some people suggested goals accomplished. I think that is quite good.

I think this goal might have been accomplished!

view this post on Zulip Patrick Massot (Mar 23 2019 at 20:48):

Yes, I noticed that when helping students on Friday.

view this post on Zulip Scott Morrison (Mar 25 2019 at 08:56):

It looks like this has landed, and I think I'm not that keen on "goals accomplished"... As Keeley pointed out to me, after you write:

example : true := begin
  tactic.set_goals [],
end

"goals accomplished" is a bit overenthusiastic, but "no goals" is completely accurate.

view this post on Zulip Johan Commelin (Mar 25 2019 at 08:58):

Otoh, when "goals accomplished" is accurate, then "no goals" is a bit underenthousiastic.

view this post on Zulip Johan Commelin (Mar 25 2019 at 08:58):

There have been several cases of confusion with beginners...

view this post on Zulip Johan Commelin (Mar 25 2019 at 08:59):

But I understand that what we have now might also cause confusion.

view this post on Zulip Chris Hughes (Mar 25 2019 at 12:38):

There are very occasionally times like this when it is a little misleading.

lemma zero_eq_one : 0 = @has_zero.zero  1 :=
begin
  refl, -- goals accomplished
end

type mismatch at definition 'zero_eq_one', has type 0 = 0 but is expected to have type 0 = 0

view this post on Zulip Johan Commelin (Mar 25 2019 at 12:42):

Even with "no goals" I expect a lot of beginners to be very confused by such a situation.

view this post on Zulip Floris van Doorn (Mar 25 2019 at 15:13):

I'm a fan of the new goals accomplished!

On the topic of confusing messages: if you are in a tactic proof, you will often see that the tactic failed, while you're still in the process of writing a proof. I know beginners who were confused by the actual error messages, they thought that the tactic proof so far gave an error

example : true := begin end
example : true := begin {  } end

give errors

tactic failed, there are unsolved goals
solve1 tactic failed, focused goal has not been solved

Much better would be something like:

There are unsolved goals
Not all goals have been solved

view this post on Zulip Johan Commelin (Mar 26 2019 at 07:33):

Another feature request:
If you hover over a symbol you get a tooltip with the type signature (very helpful!)
If your cursor is on a symbol, you can hit Ctrl-Shift-F10 to peek at the definition (very helpful!)
In emacs-lean you have a little window/line on which you can always see the type signature of the symbol under the cursor. Can we have a similar feature in VScode?

view this post on Zulip Edward Ayers (Mar 27 2019 at 19:54):

How do you find this useful? That is, is it that the emacs window is always immediate or that it doesn't obscure your code?

view this post on Zulip Johan Commelin (Mar 27 2019 at 19:55):

It's just always there. So when I move my cursor (not the mouse) I see exactly what the type signature is of the symbol that I'm on.

view this post on Zulip Johan Commelin (Mar 27 2019 at 19:55):

Since I use the Vim extension, I move the cursor a lot without the mouse, and so I don't get to see the tooltip.

view this post on Zulip Edward Ayers (Mar 27 2019 at 19:55):

Ah I see.

view this post on Zulip Johan Commelin (Mar 27 2019 at 19:56):

I wouldn't mind spending 1 or 2 lines of screen space on this feature.

view this post on Zulip Edward Ayers (Mar 27 2019 at 19:56):

Some duct tape for now is Ctrl-K Ctrl-I

view this post on Zulip Edward Ayers (Mar 27 2019 at 19:57):

How about having the type information appear in the Lean messages screen?

view this post on Zulip Johan Commelin (Mar 27 2019 at 19:57):

Well, the duct tape is also Ctrl-Shift-F10

view this post on Zulip Johan Commelin (Mar 27 2019 at 19:58):

Hmm, maybe it could go there. Don't know what others think of that....

view this post on Zulip Edward Ayers (Mar 27 2019 at 20:00):

You can also get VScode to add non-editable text inside the document. So you could see the type information to the right of the current line.

view this post on Zulip Johan Commelin (Mar 27 2019 at 20:01):

I already have GitLens info there...

view this post on Zulip Johan Commelin (Mar 27 2019 at 20:03):

I don't need an immediate solution. Ctrl-Shift-F10 works fine for now. But if someone wants to hack on a new feature... I'd like to see a small window of 1 or 2 lines high at the bottom of the editor, showing these type signatures.

view this post on Zulip Bryan Gin-ge Chen (Mar 27 2019 at 20:03):

How about as (yet) another status bar item?

view this post on Zulip Johan Commelin (Mar 27 2019 at 20:04):

That might work, yes

view this post on Zulip Jesse Michael Han (Mar 27 2019 at 21:11):

How do you find this useful? That is, is it that the emacs window is always immediate or that it doesn't obscure your code?

the minibuffer occupies exactly one line at the bottom of the window and this is where the type information shows up---this feature is very useful when parsing compressed terms

view this post on Zulip Kevin Buzzard (Mar 27 2019 at 21:19):

I wrote my PhD thesis using emacs nearly 25 years ago and I have been in love with emacs ever since. I use it for everything. I used it for Lean initially, but when I started trying to teach Lean to other people I reluctantly switched to VS Code. I still occasionally get frustrated that I can't do funky text editing in VS Code, the sort of thing I can do with elaborate shortcuts that 25 years of emacs has taught me, but the fact that everyone else uses VS Code has convinced me to switch. If there are advantages in using emacs over VS Code (like some minibuffer feature) then my opinion now is that someone should come up with a coherent way of porting them to VS Code and then perhaps we should try and persuade Gabriel to implement them in the VS Code Lean extension. Gabriel has done a remarkable job maintaining this extension, he is efficient and open to new ideas and fixes bugs quickly. Ctrl-Shift-F10 opens up a massive window for me. How can this be the same as a one-line window displaying whatever it is we're talking about?

view this post on Zulip Kevin Buzzard (Mar 27 2019 at 21:23):

Oh -- the type signature of what is under the cursor? Could we make it display in the same panel as the "Problems / Output / Debug Console / Terminal" panel?

view this post on Zulip Bryan Gin-ge Chen (Mar 27 2019 at 21:43):

I don't see a way to add a new panel at the bottom with the extension API (see e.g. this page) (though I may be missing something). It might be possible to do something like what you want by creating a fake error that follows the cursor around but that feels dirty.

view this post on Zulip Edward Ayers (Mar 28 2019 at 11:15):

I agree that this minibuffer or similar would be really useful for all programming languages instead of hover. I often get in to tooltip hell with Lean. I want to be able to 'pin' tooltip hovers and output window state.

view this post on Zulip Edward Ayers (Mar 28 2019 at 11:16):

Another possibility might be to dump the information to the output pane.

view this post on Zulip Gabriel Ebner (Mar 28 2019 at 11:27):

I think the only way to get a one-line display at the bottom of the screen is to add a status bar item, like the vim extension does:
vscode_statusbar.png

view this post on Zulip Wojciech Nawrocki (Mar 31 2019 at 14:00):

I'm unsure if this has been proposed before, but it would be wonderful if lean-vscode were to support some more advanced features present in editor plugins like Emacs' agda-mode. For example, Case Split which when executed in a sort-of equation compiler context automatically makes cases for each constructor of the selected value. E.g. def foo (n: nat): nat -> case split on n in vscode ->

def foo (n: nat): nat
| zero := _
| (succ n) := _

Would something like this go in lean-vscode or the Lean server? Or perhaps it already exists and I somehow missed it?

view this post on Zulip Wojciech Nawrocki (Mar 31 2019 at 14:09):

Seems in Agda it's handled 99% by the server, the editor extension only forwards commands.

view this post on Zulip Kevin Buzzard (Mar 31 2019 at 14:57):

Snippets might provide a first approximation to what you want. For example when I type split and then play some ctrl-space dance I get Lean to write

split,
{
  sorry
},
{
  sorry
}

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2019 at 15:08):

I think someone would need to write a "hole command" tactic (in lean) for this. I'm not sure how to do this exactly, others may know more.

view this post on Zulip Wojciech Nawrocki (Mar 31 2019 at 15:08):

Indeed, but not so much when there's 30 constructors with different arguments each :|

view this post on Zulip Kevin Buzzard (Mar 31 2019 at 15:09):

I see -- you want one thing to deal with every inductive type.

view this post on Zulip Rob Lewis (Mar 31 2019 at 15:11):

There is a hole command to do this, but it appears not to have made it into the hole command doc file. https://github.com/leanprover-community/mathlib/blob/master/src/tactic/basic.lean#L774

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2019 at 15:51):

Cool! For future reference, one types:

def foo : {! nat -> nat !}

Then with the cursor inside the hole {! ... !}, hit Ctrl+. (or Cmd+. on macOS) to open the "Quick Fix" menu (or click on the light bulb that appears). If you select "Generate a list of equations for a recursive definition." then the above is transformed to:

def foo :   
| nat.zero := _
| (nat.succ n) := _

Is there a way to assign a keyboard shortcut to a particular hole command?

view this post on Zulip Wojciech Nawrocki (Mar 31 2019 at 16:01):

This is almost perfect! Now if only there was a way to specify which argument to split on - for example in nat -> nat -> nat it seems to always just split on the first (and I can't always write a nested match statement since it breaks unification)

view this post on Zulip Wojciech Nawrocki (Mar 31 2019 at 16:11):

@Bryan Gin-ge Chen apparently these are currently implemented as code actions, where the arguments to the Lean server command are contextual on the position in the file etc. Key-bound commands, on the other hand, seem to be unaware of the context. But i'm sure there is some way to pass the context there - @Gabriel Ebner ? :)

view this post on Zulip Bryan Gin-ge Chen (Mar 31 2019 at 16:19):

Hmm, it might be possible by passing args to editor.action.codeAction but I haven't figured out what this would look like for the hole commands...

view this post on Zulip Bryan Gin-ge Chen (Apr 01 2019 at 05:57):

I've just PR'd a status bar item that displays the type information for the term under the cursor. @Johan Commelin

view this post on Zulip Johan Commelin (Apr 01 2019 at 06:00):

Wow! That's a marvelous April Fools day joke!

view this post on Zulip Johan Commelin (Apr 01 2019 at 06:00):

Merci!

view this post on Zulip Johan Commelin (Apr 02 2019 at 19:39):

https://devblogs.microsoft.com/visualstudio/live-share-now-included-with-visual-studio-2019/
Collaborative editing in VScode

view this post on Zulip Scott Morrison (Apr 02 2019 at 22:14):

Anyone want to try this out?

view this post on Zulip Scott Morrison (Apr 02 2019 at 22:15):

https://prod.liveshare.vsengsaas.visualstudio.com/join?922C14F0F9FCDAA4DB4629450DEA18E91EA1

view this post on Zulip Kevin Buzzard (Apr 02 2019 at 22:22):

vscode.png

view this post on Zulip Kevin Buzzard (Apr 02 2019 at 22:22):

Scott and I are "collaborating" in the sense that we're both writing comments in the same mathlib file

view this post on Zulip Scott Morrison (Apr 02 2019 at 22:31):

Kevin and I have been experimenting a bit. I think the advice is to install the "Live Share Extension Pack", as it gives you chat, and (non-working?) audio.

view this post on Zulip Kevin Buzzard (Apr 02 2019 at 22:42):

so we can both edit a Lean file

view this post on Zulip Kevin Buzzard (Apr 02 2019 at 22:42):

and we're using Scott's machine which is fast

view this post on Zulip Kevin Buzzard (Apr 02 2019 at 22:42):

and even though it's on the opposite side of the world from me there seems to be no lag

view this post on Zulip Johan Commelin (Apr 23 2019 at 13:19):

Something seems to be wrong with hole commands... If you have {!}) then executing a hole command eats the final delimiter. (Doesn't have to be ). It can be anything.)

view this post on Zulip Johan Commelin (Apr 23 2019 at 13:21):

MWE:

lemma foobar {X : Type} (x : X) : x = x := ({!})

Now use library_search or whatever to fill the hole.

view this post on Zulip Gabriel Ebner (Apr 23 2019 at 13:31):

I didn't know you could do a hole with only one exclamation mark. Typically it's {! !}.

view this post on Zulip Johan Commelin (Apr 23 2019 at 13:34):

I noticed that the :bulb: already appeared after typing {!}.

view this post on Zulip Johan Commelin (Apr 23 2019 at 13:35):

I see, so with the official {! !} there is no problem.

view this post on Zulip Johan Commelin (Apr 23 2019 at 13:35):

However, that requires me to type more... )-;

view this post on Zulip Johan Commelin (Apr 23 2019 at 13:35):

Let me stress that this is a low priority bug report :stuck_out_tongue_wink:

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 13:36):

ha ha I only ever use {! } -- I used it from the moment I noticed it worked.

view this post on Zulip Jesse Michael Han (Apr 23 2019 at 14:27):

in Emacs I just bound C-c C-SPC to insert a hole template (so that afterwards C-c SPC opens the hole command menu) :^)

view this post on Zulip Jesse Michael Han (Apr 23 2019 at 14:30):

my usage of french quotes also skyrocketed after setting those to C-c C-f

view this post on Zulip Kenny Lau (Jun 10 2019 at 01:59):

colouration_bug.png

view this post on Zulip Kenny Lau (Jun 10 2019 at 02:00):

the part in the red rectangle is coloured in yellow

view this post on Zulip Kenny Lau (Jun 10 2019 at 02:00):

but it should be just white

view this post on Zulip Bryan Gin-ge Chen (Jun 10 2019 at 02:05):

Yeah, the syntax highlighting in the tactic state is not very sophisticated at the moment.

PR (merged in 0.14.2)

view this post on Zulip Kenny Lau (Jul 04 2019 at 06:25):

Is it just me or did the red underlines become orange? It's an interesting change if so

view this post on Zulip Alexander Bentkamp (Jul 04 2019 at 08:07):

@Kenny Lau It might be because of this change in VS Code: https://code.visualstudio.com/updates/v1_36#_updated-warning-colors

view this post on Zulip Keeley Hoek (Jul 04 2019 at 11:19):

For me real errors are still red, and sorries are orange

view this post on Zulip Kenny Lau (Jul 11 2019 at 20:53):

The ctrl+space list doesn't process french quotes, leading to invalid results.

view this post on Zulip Kenny Lau (Jul 11 2019 at 20:54):

view this post on Zulip Mario Carneiro (Jul 11 2019 at 20:55):

what's invalid about it?

view this post on Zulip Kenny Lau (Jul 11 2019 at 21:06):

@Mario Carneiro unexpected token and invalid expression, unexpected token

view this post on Zulip Kenny Lau (Jul 11 2019 at 21:06):

def «äääää».bbbbb :  := 0
#check äääää.bbbbb

view this post on Zulip Bryan Gin-ge Chen (Jul 11 2019 at 21:20):

The list of completions comes directly from the Lean server, so I think this would have to be addressed by a patch to the C++ code somewhere.

view this post on Zulip Kenny Lau (Dec 05 2019 at 03:11):

when I press tab it focuses on another window instead of adding 2 spaces; what should I do to fix that?

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:12):

there is a line on the status bar that says "TAB moves focus", click on it

view this post on Zulip Kenny Lau (Dec 05 2019 at 03:15):

oh thanks

view this post on Zulip Kenny Lau (Dec 05 2019 at 03:15):

hidden in plain sight

view this post on Zulip Kenny Lau (Dec 27 2019 at 02:24):

when I double click on a word to highlight it, the neighbouring angle brackets are also highlighted; how do I tell VSCode that angle brackets are not words?

view this post on Zulip Andrew Ashworth (Dec 27 2019 at 02:27):

editor.wordSeparators

view this post on Zulip Kenny Lau (Dec 27 2019 at 02:38):

thanks

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:42):

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:42):

the angle brackets strike back

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:42):

is this one governed by a different system?

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:42):

(this is the suggestions that come up before you press ctrl+space, which suggests completions solely based on what appeared in the current file)

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:44):

This comes from the vscode language settings for deciding what is a word character

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:45):

https://code.visualstudio.com/api/language-extensions/language-configuration-guide#word-pattern

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:47):

All the bracketing characters seem to be correctly marked as brackets in https://github.com/leanprover/vscode-lean/blob/master/language-configuration.json but there is a comment about the wordPattern saying that it is set in code to work around an issue

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:48):

that has since been fixed

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:50):

so what should I do?

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:50):

Here is the relevant regex: https://github.com/leanprover/vscode-lean/blob/master/src/extension.ts#L88

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:50):

it's an exclusion list, and it doesn't exclude everything it should

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:51):

lean has a definition of what constitutes a valid word character and it includes several unicode ranges but I think most things are not word characters

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:51):

so there's nothing I can do?

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:51):

you can PR to vscode-lean

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:52):

it's a bug in the syntax/language definition

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:54):

done

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:54):

did you test it?

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:55):

if you downloaded the repo you should be able to hit f5 to start the extension

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:57):

I'm not sure how to test it

view this post on Zulip Mario Carneiro (Dec 31 2019 at 10:59):

the word list comes from the words that are present in the file. If you open logic.basic or something you are bound to find a word followed by a close angle bracket

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:59):

as in, I don't know how to modify the file locally

view this post on Zulip Kenny Lau (Dec 31 2019 at 10:59):

because I'm unable to locate the file

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:00):

didn't you just modify the file?

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:00):

src/extension.ts

view this post on Zulip Kenny Lau (Dec 31 2019 at 11:00):

but I edited it online and I don't know where is the file that my vscode is using

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:04):

if you get the repo and open it in vscode and hit f5, it will compile and run the extension in a new session

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:04):

it won't affect your current instance

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:05):

If you want to fix your current instance, you can copy the repo folder (after building it) into ~/.vscode/extensions

view this post on Zulip Kenny Lau (Dec 31 2019 at 11:06):

ah, ~/.vscode/extensions

view this post on Zulip Kenny Lau (Dec 31 2019 at 11:06):

that's the info I needed

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:06):

but assuming the vscode-lean maintainers are around, if the fix works eventually it will make it into the official version and you can just update the official way

view this post on Zulip Kenny Lau (Dec 31 2019 at 11:07):

would there be any issue if I modify ~/.vscode/extensions directly?

view this post on Zulip Kenny Lau (Dec 31 2019 at 11:07):

you know how if I modify mathlib I need to recompile everything

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:07):

You may need to uninstall vscode-lean first

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:07):

but lean and mathlib are unaffected

view this post on Zulip Mario Carneiro (Dec 31 2019 at 11:08):

vscode-lean doesn't handle any of that, it just calls a thing on your machine called "lean"

view this post on Zulip Greg Langmead (Jan 31 2020 at 03:23):

Does anyone have a good idea how to render the markdown part of a .lean file on the fly in vscode, so that it would be more like editing a math document that has code in it and less like a file with two programming languages? It might have to be rendered into a side pane. Related: I'm assuming the markdown we use either already can or soon could support latex or mathjax or something, depending on the downstream processing we're targeting. I didn't find any latex in mathlib however.

view this post on Zulip Kevin Buzzard (Jan 31 2020 at 03:24):

@Patrick Massot @Mohammad Pedramfar @Bryan Gin-ge Chen ?

view this post on Zulip Greg Langmead (Jan 31 2020 at 03:26):

I'm happy to get on the learning curve of the plugin and pitch in, if I can.

view this post on Zulip Bryan Gin-ge Chen (Jan 31 2020 at 03:58):

I think it's possible, though it would be a big project. You might look into how VS Code's Python extension displays Jupyter notebooks, since that also mixes markdown and code.

view this post on Zulip Rob Lewis (Jan 31 2020 at 10:16):

Related: I'm assuming the markdown we use either already can or soon could support latex or mathjax or something, depending on the downstream processing we're targeting. I didn't find any latex in mathlib however.

There was a bit of discussion some time ago about latex in the docs. I think the conclusion was that doing something basic with mathjax would be easy enough, but "real" support would be a lot harder. Not planning to do it myself soon, but I'd be happy to see it added.

view this post on Zulip Rob Lewis (Jan 31 2020 at 10:18):

Adding latex to declaration doc strings is slightly harder, because those are also displayed in VSCode tooltips, so you'd want to process it there too.

view this post on Zulip Greg Langmead (Jan 31 2020 at 14:17):

How are the docs generated from the mathlib source? From my preliminary investigation there would three customers consuming the markdown comments: the generation of the browsable docs, the fancy pane I'm proposing, and the hover panes. For now I'm assuming 1 and 2 can be brought into alignment by using the same third party support for some subset of LaTeX. But the hover panes look like they use a hardcoded more limited subset of markdown and wouldn't get to participate for now, so they'd show the raw LaTeX.

VSCode's own built-in markdown support (which kicks in if you edit a file ending with .md) looks like just the experience I'd love to replicate: https://code.visualstudio.com/docs/languages/markdown.

Last remark for now: another tack that probably requires Lean dev time is to imitate literate Agda and have a whole other file extension like .llean with two els, which would in fact be a markdown document, with lean code in triple-backticked lean blocks like we use here on zulip. We'd then create an extention to markdown to render the lean, and we'd extend lean to ignore everything outside the lean blocks: https://agda.readthedocs.io/en/v2.5.3/tools/literate-programming.html

view this post on Zulip Rob Lewis (Jan 31 2020 at 14:54):

How are the docs generated from the mathlib source?

https://github.com/leanprover-community/doc-gen
A metaprogram imports all of mathlib and builds a json file with doc strings, type info, line numbers, module doc strings, etc. Then this gets fed into a Python script that builds the HTML, including processing the markdown.

I have no idea how much control the VSCode extension gives us over the hover panes.

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

@Rob Lewis VSCode's extension API isn't too flexible with regards to the hover panes. Basically we have to implement a "HoverProvider" which returns "Hover" objects. These contain "MarkdownString"s which VS Code then processes with its own markdown interpreter. (You can see what vscode-lean currently does here). Nonetheless, it does seem to be possible to put LaTeX inside the hover windows: see these screenshots from the "LaTeX-Workshop" extension wiki.

@Greg Langmead It seems like what you want is a kind of "rich text" editor, where a single editor window would display both chunks of rendered markdown as well as bits of (interactively interpreted) Lean code. Leaving aside the details of any future "Literate Lean" format, let me expand on my comment from last night. I believe you could implement this in a VS Code extension but since VS Code doesn't currently let us customize the editor UI to that extent, you would have to write your own editor in a web view. I haven't dug too deep into vscode-python's Jupyter notebook support, but I am pretty sure that is what they do (probably using monaco in their webview). It looks like VS Code is in the process of adding a custom editor API which would help such custom editors better integrate into VS Code (e.g. saving and undoing); note that this won't help with the "front-end" work that would need to be done.

If you just want to be able to preview the markdown in module / docstring comments in Lean files while editing them in the usual editor, that would be a lot easier. There are two features that seem much easier to me (though I won't have time to tackle them in the near future):

  • The hover provider could detect whether the user is hovering over a module / docstring comment and then pop up a hover window with that comment rendered in markdown
  • When the cursor is placed inside a comment, the infoview window could render that comment in markdown

Note that there's also a fourth consumer of the comments here: https://observablehq.com/@bryangingechen/github-lean-doc-preview (though I'm not sure how widely used this is). Possibly some of the comment parsing code there would be useful for the extension features I just described? Though for performance it would probably make more sense to edit Lean so that the Lean server tells us whether a certain position is inside a comment.

view this post on Zulip Sebastien Gouezel (Jan 31 2020 at 17:54):

Note that there's also a fourth consumer of the comments here: https://observablehq.com/@bryangingechen/github-lean-doc-preview (though I'm not sure how widely used this is).

Just to mention that I use it to check all of my PRs, and that I find it extremely useful. Thanks a lot for this!

view this post on Zulip Gabriel Ebner (Jan 31 2020 at 19:05):

Nonetheless, it does seem to be possible to put LaTeX inside the hover windows

OMG, this is a gorgeous hack! They render latex into an svg image, and then include a link to the generated image (where the url is a data url that includes a base64 encoding of the image). So, we could of course do exactly the same thing in vscode-lean.

view this post on Zulip Greg Langmead (Jan 31 2020 at 22:46):

It seems like what you want is a kind of "rich text" editor, where a single editor window would display both chunks of rendered markdown as well as bits of (interactively interpreted) Lean code.

The pony is to have a perfectly typeset document with interactive code blocks, with all the affordances of the code editor like following definitions and search and whatnot. That's too ambitious and in fact exceeds most LaTeX environments people use. And I wouldn't want to do it with VSCode as it basically supersedes the entire UI paradigm of VSCode so it's a new app.

And I don't think I want to hover over the docstring and only then see the rendered version in some ephemeral floating window. I think I want it to be the way I do LaTeX. Two panes: left pane is raw source (mix of lean and docstrings) and the right pane is a read-only fully rendered version. I'm not sure, I should go try to make it and see if it's helpful!

Secondarily, when docstrings do appear in hovers, we could render LaTeX in them, maybe using the trick you showed which @Gabriel Ebner likes!

view this post on Zulip Greg Langmead (Jan 31 2020 at 22:57):

The pony is to have a perfectly typeset document with interactive code blocks

But ObservableHQ comes really close to this from another direction. It has the rich document, but the lean code blocks are islands and can't be navigated between (I assume). And it's not backed by a single text file on my computer, it's some other document format, so it is probably more like the PDF of this story.

view this post on Zulip Bryan Gin-ge Chen (Jan 31 2020 at 23:55):

Two panes: left pane is raw source (mix of lean and docstrings) and the right pane is a read-only fully rendered version.

OK, I think I see. Do you want the Lean code in the right pane to be interactive in some way as well? What do you have in mind for the current "info view" panel that displays stuff like tactic state?

[ObservableHQ] has the rich document, but the lean code blocks are islands and can't be navigated between (I assume).

The Observable Lean editor currently does support splitting a Lean file into multiple editor cells, and I think adding something like inter-editor navigation via keyboard shortcuts or clicking on buttons would definitely be doable.

[An ObservableHQ notebook is] not backed by a single text file on my computer, it's some other document format

ObservableHQ documents are backed by (internal, undocumented) JSON source files which are then compiled to Javascript modules that can then be run in an HTML document. These compiled modules can be downloaded from the notebook editor on observablehq.com. It's then not too hard to embed notebooks to run on other webpages; you can even host them in github gists. However, running them "offline" does require starting a local web server (due to browser security restrictions). [At the moment ObservableHQ.com's compiler is not open source, but there is an "unofficial" version here (full disclosure: I have contributed some code to this project, though I am not the primary maintainer).]

view this post on Zulip Greg Langmead (Feb 01 2020 at 21:39):

Yeah the observable format looks to be some reasonable fixed format using standard languages, and easy to download out of the system, which is very cool. I will definitely try using it as a delivery vehicle for whatever geometry formalization I come up with. Having a converter between .lean and such a notebook would reduce the friction considerably.

Speaking of converters I looked more at the VSCode extension APIs and I'm still a little confused on what is the best approach, but all approaches will require a Lean to markdown converter which knows how to parse the comments and docstrings, and wraps the code in triple-backticks. Once we had that, we would either dynamically create a webview in lean and imitate their markdown plugin to populate it and keep its scrolling in sync, OR perhaps we could handoff the markdown directly to that extension somehow like with their virtual document system.

view this post on Zulip Greg Langmead (Feb 01 2020 at 21:52):

Or just use https://github.com/leanprover-community/doc-gen to convert to HTML and put it in the webview, and make whatever enhancements we need to that repo so it's all shared in one place, with no markdown intermediary.

view this post on Zulip Greg Langmead (Feb 03 2020 at 02:25):

@Rob Lewis Here's a PR for the doc-gen: https://github.com/leanprover-community/doc-gen/pull/9. All it changes is to add the MathJax incantation in the header, plus one change to its settings to allow $..$ delimiters since these are off by default. I ran doc-gen locally and confirmed that I could simply add math to a doc string and it was passed through into json_export.txt and then the html.

view this post on Zulip Greg Langmead (Feb 03 2020 at 02:29):

I'm thinking the easiest change to make to the VSCode extension is to add a command that opens your browser to the right URL under https://leanprover-community.github.io/mathlib_docs/ if you're looking at a mathlib file. It raises questions like whether that's the same version as the one you have locally which I have not answered yet. But it seems easier than doing an on the fly HTML conversion of the lean, since both doc-gen and format_lean need to talk to lean in some nontrivial way that I'm not yet sure I could replicate from within the plugin.

view this post on Zulip Rob Lewis (Feb 03 2020 at 10:05):

@Greg Langmead thanks for the PR! I'm happy to merge it, with the one concern I just commented on: I think $..$ is off by default because it leads to lots of false positives when mixed with regular text. "Subscriptions cost $10-$15 / mo" and all that. Pretty sure Zulip uses $$..$$ which I'll test here: R\mathbb{R} ?

view this post on Zulip Johan Commelin (Feb 03 2020 at 10:07):

@Rob Lewis Otoh, everyone is pretty used to $ foo $, and I don't think we'll actually hit many false positives.

view this post on Zulip Johan Commelin (Feb 03 2020 at 10:07):

We can always print regular $-signs by escaping them.

view this post on Zulip Johan Commelin (Feb 03 2020 at 10:08):

Can we check if there are "regular text $" occuring in mathlib right now? I doubt it.

view this post on Zulip Gabriel Ebner (Feb 03 2020 at 10:09):

The only occurrence I can see is `foo $ bar $ baz 10`

view this post on Zulip Rob Lewis (Feb 03 2020 at 10:09):

$ is used in code as well. How well does MathJax avoids code blocks? If it inserts itself in f $ g $ h x it's a non-starter.

view this post on Zulip Rob Lewis (Feb 03 2020 at 10:10):

People are used to $$..$$ from Zulip too.

view this post on Zulip Johan Commelin (Feb 03 2020 at 10:11):

$ is used in code as well. How well does MathJax avoids code blocks? If it inserts itself in f $ g $ h x it's a non-starter.

I completely agree with that.

view this post on Zulip Greg Langmead (Feb 03 2020 at 14:47):

To echo some of the discussion from github: I just updated the PR so that we do indeed process single and double dollar signs, which is good since it's what people will expect. I added some configuration to prevent MathJax from processing a few additional css classes Rob is using to structure the presentation of Lean. And MathJax avoids pre and code tags, so together these should prevent Lean's own dollar signs from interfering.

view this post on Zulip Greg Langmead (Feb 03 2020 at 14:50):

Here are some points to MathJax info for those, like me, who have never heavily used it but who may be, like me, concerned about its differences from real LaTeX:

view this post on Zulip Greg Langmead (Feb 03 2020 at 14:54):

It supports macros, which I didn't know: http://docs.mathjax.org/en/latest/input/tex/macros.html
It supports the ams package's symbols: http://docs.mathjax.org/en/latest/input/tex/extensions/ams.html
It supports amscd commutative diagrams: http://docs.mathjax.org/en/latest/input/tex/extensions/amsCd.html

view this post on Zulip Rob Lewis (Feb 03 2020 at 15:00):

This is merged, so feel free to start using it in your doc strings! Remember it won't show up in VSCode tooltips at the moment, just in the generated docs.

view this post on Zulip Rob Lewis (Feb 03 2020 at 15:01):

Thanks very much @Greg Langmead !

view this post on Zulip Sebastien Gouezel (Feb 04 2020 at 10:14):

Note that there's also a fourth consumer of the comments here: https://observablehq.com/@bryangingechen/github-lean-doc-preview (though I'm not sure how widely used this is).

Now that mathjax is activated on mathlib doc, would it also be possible to activate it there to have as close to possible outputs, or is it too complicated in the observable framework?

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2020 at 11:25):

I think it's possible. I will try to find time to add it.

view this post on Zulip Bryan Gin-ge Chen (Feb 05 2020 at 06:28):

@Sebastien Gouezel I think I got it working. Here's a test that looks at one of the commits from Kevin's recent mv_polynomial doc PR. Some of the lists are screwed up since they weren't formatted correctly with markdown bullets originally, but the included LaTeX seems to be rendered OK.

view this post on Zulip Sebastien Gouezel (Feb 05 2020 at 06:50):

I just tried it on #1952, and I get a nicely formatted equation, but also a weird docstring.

view this post on Zulip Bryan Gin-ge Chen (Feb 05 2020 at 07:35):

@Sebastien Gouezel Thanks for the example! I think it's fixed now: https://observablehq.com/@bryangingechen/github-lean-doc-preview?url=%221952%22

view this post on Zulip Sebastien Gouezel (Feb 05 2020 at 07:39):

Amazing, thanks a lot!

view this post on Zulip Kenny Lau (Apr 13 2020 at 09:40):

Issue 154: backslash does not convert when typing the provided closing bracket

To reproduce this issue, type (\N).

  • After (, a matching closing bracket is provided just after the text cursor.
  • After \, there is an underline denoting that conversion is to take place.
  • After N, the underline is on both characters \N. At this point, moving the cursor anywhere or pressing space or typing another \ will cause the conversion into ; however:
  • After ), no conversion takes place and the underline disappears, and one is left with (\N), instead of the expected (ℕ).

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 09:51):

Press the space bar :-)

view this post on Zulip Gabriel Ebner (Apr 13 2020 at 09:54):

If we're already talking about workarounds, you can always press TAB to trigger the conversion.

view this post on Zulip Kenny Lau (Apr 13 2020 at 09:56):

oh wow I never knew that

view this post on Zulip Kenny Lau (Apr 13 2020 at 09:56):

I was like, why isn't there any way to trigger the conversion without moving my damn cursor

view this post on Zulip Patrick Massot (May 05 2020 at 20:28):

Bryan Gin-ge Chen said:

Is anyone else seeing broken pause / continue icons in the tactic state since the latest VS code update (1.31.0)?

And this is now FIXED! This was probably the record number of releases of the VScode extension in one day, isn't it?

view this post on Zulip Patrick Massot (May 05 2020 at 20:29):

https://github.com/leanprover/vscode-lean/releases

view this post on Zulip Johan Commelin (May 12 2020 at 12:45):

What do people think of add shortcuts \inf for \glb and \sup for \lub?

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:49):

When I was learning lattices I typed \inf and \sup so many times!

view this post on Zulip Kevin Buzzard (May 12 2020 at 12:49):

I'd definitely be in favour.

view this post on Zulip Bhavik Mehta (May 12 2020 at 12:53):

Would there be a clash with \infty? (I haven't needed to use it but perhaps those who have wouldn't like this)

view this post on Zulip Mario Carneiro (May 12 2020 at 12:55):

and apparently \supseteq

view this post on Zulip Gabriel Ebner (May 12 2020 at 13:04):

I don't remember the algorithm in vscode. Would there still be a clash if you type \sups, or is it that \sup would no longer be an abbreviation for , or would \sup simply not work?

view this post on Zulip Mario Carneiro (May 12 2020 at 13:10):

I get this for writing initial segments of \supseteq:

\supseteq
 σ⊆⊇⊃⊃⊃⊇⊇

view this post on Zulip Mario Carneiro (May 12 2020 at 13:11):

I think must be registered as both \sup and \supseteq for this behavior to occur


Last updated: May 08 2021 at 04:14 UTC