VScode extension

Stream: general

[Patrick Massot]

@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.

[Mario Carneiro]

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

[Patrick Massot]

Not here

[Mario Carneiro]

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

[Mario Carneiro]

You can set your key bindings yourself btw

[Patrick Massot]

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.

[Patrick Massot]

How do you setup keybindings?

[Mario Carneiro]

file > prefs > key shortcuts

[Johan Commelin]

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?

[Mario Carneiro]

this is what emacs does

[Mario Carneiro]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Mario Carneiro]

I believe so

[Johan Commelin]

Nice

[Mario Carneiro]

I think vscode does the same in that case

[Johan Commelin]

Hmm, maybe it does.

[Gabriel Ebner]

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.

[Johan Commelin]

I think vscode does the same in that case

You are right.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Gabriel Ebner]

"Go back"

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

[Patrick Massot]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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+\

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Gabriel Ebner]

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.

[Patrick Massot]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

afk hornet in the room

[Gabriel Ebner]

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.

[Chris Hughes]

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?

[Simon Hudon]

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?

[Gabriel Ebner]

it opens the file I have open in the right pane

This bug should be fixed with yesterday's update.

[Gabriel Ebner]

[..] 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.

[Chris Hughes]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Chris Hughes]

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

[Chris Hughes]

Maybe I should update lean?

[Ali Sever]

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

[Chris Hughes]

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

[Ali Sever]

how did you close your lean files?

[Chris Hughes]

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

[Kevin Buzzard]

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.

[Gabriel Ebner]

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

[Kevin Buzzard]

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?

[Chris Hughes]

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

[Chris Hughes]

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

[Gabriel Ebner]

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.

[Simon Hudon]

@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.

[Chris Hughes]

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

[Chris Hughes]

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

[Chris Hughes]

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.

[Chris Hughes]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Ali Sever]

Thanks Chris, awesome as always

[Kevin Buzzard]

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.

[Ali Sever]

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

[Chris Hughes]

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

[Kevin Buzzard]

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.

[Ali Sever]

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

[Kenny Lau]

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

[Moses Schönfinkel]

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.

[Moses Schönfinkel]

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.

[Gabriel Ebner]

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

[Moses Schönfinkel]

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

[Moses Schönfinkel]

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.

[Gabriel Ebner]

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.

[Gabriel Ebner]

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

[Moses Schönfinkel]

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.

[Patrick Massot]

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?

[Kevin Buzzard]

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.

[Patrick Massot]

This would be really really helpful

[Patrick Massot]

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

[Gabriel Ebner]

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"

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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..

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Kenny Lau]

ctrl+alt+shift+enter

[Johan Commelin]

What the hack is that supposed to do?

[Johan Commelin]

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

[Kenny Lau]

it lets you view all the messages

[Kenny Lau]

instead of just the one on your line

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

@Gabriel Ebner :up:

[Kevin Buzzard]

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

[Kenny Lau]

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

[Johan Commelin]

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:

[Gabriel Ebner]

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?

[Johan Commelin]

Right

[Gabriel Ebner]

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

[Johan Commelin]

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.

[Gabriel Ebner]

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!

[Johan Commelin]

Ok, I should try that out.

[Johan Commelin]

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!

[Gabriel Ebner]

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

[Kevin Buzzard]

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.

[Johan Commelin]

I should prod William about CoCalc.

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

[Gabriel Ebner]

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.

[Kenny Lau]

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

[Kenny Lau]

wait it works now

[Johan Commelin]

@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:

[Patrick Massot]

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

[Gabriel Ebner]

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

[Johan Commelin]

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

[Johan Commelin]

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...

[Johan Commelin]

[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]

[Chris Hughes]

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.

[Gabriel Ebner]

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.

[Gabriel Ebner]

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.

[Gabriel Ebner]

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

[Johan Commelin]

Clippy was not really serious...

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@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.

[Gabriel Ebner]

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

[Mario Carneiro]

I think that this is used for natural transformations

[Gabriel Ebner]

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

[Johan Commelin]

\hom and \==>

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Sean Leather]

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.

[Gabriel Ebner]

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

[Johan Commelin]

Exactly

[Gabriel Ebner]

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

[Johan Commelin]

Oops, that is silly

[Johan Commelin]

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

[Gabriel Ebner]

And deployed.

[Johan Commelin]

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

[Johan Commelin]

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)

[Johan Commelin]

That's the silly thing that I'm trying

[Johan Commelin]

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

[Mario Carneiro]

are you going to claim it as a global notation?

[Johan Commelin]

Of course! We are evil!

[Mario Carneiro]

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

[Johan Commelin]

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

[Patrick Massot]

Gabriel, why do you hardcode the leader key?

[Gabriel Ebner]

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.

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

only if the abbreviation starts with a space

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

under what kind of circumstances?

[Mario Carneiro]

λ⟨a,b⟩, and such

[Patrick Massot]

this is wrong

[Patrick Massot]

should be a, b

[Mario Carneiro]

also between rewrite rules and simp rules sometimes

[Mario Carneiro]

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

[Patrick Massot]

So switching to comma would improve typography in mathlib!

[Johan Commelin]

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

[Johan Commelin]

Or just map your caps lock to \

[Gabriel Ebner]

I thought French keyboards have a key for §?

[Patrick Massot]

no

[Patrick Massot]

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

[Gabriel Ebner]

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

[Johan Commelin]

It seems to be Shift + !

[Gabriel Ebner]

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

[Patrick Massot]

it's there, but not on direct access

[Patrick Massot]

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

[Johan Commelin]

Make ù the leader (-;

[Patrick Massot]

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

[Edward Ayers]

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

[Gabriel Ebner]

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

[Patrick Massot]

what is a code formatter?

[Edward Ayers]

what is a code formatter?

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

[Edward Ayers]

Basically it adds and removes spaces until the code looks nice

[Patrick Massot]

that would be really nice

[Kevin Buzzard]

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

[Edward Ayers]

I think that you can in theory perform arbitrary textual transformations

[Gabriel Ebner]

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.

[Bryan Gin-ge Chen]

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.

[Patrick Massot]

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

[Ali Sever]

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?

[Ali Sever]

@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.

[Kenny Lau]

2018-09-04.png

[Kevin Buzzard]

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

[Kenny Lau]

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

[Johan Commelin]

Also, why did you put that in this thread?

[Kenny Lau]

because it's about VScode

[Patrick Massot]

I guess Kenny wants to complain about syntax highlighting

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

set_option class.instance_max_depth 5

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

[Bryan Gin-ge Chen]

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

[Kenny Lau]

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

[Johan Commelin]

Alternative: Tab or Shift-Tab

[Patrick Massot]

also works with Tab and Shift-Tab

[Kenny Lau]

oh right

[Johan Commelin]

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

[Kevin Buzzard]

Did you try \G?

[Kevin Buzzard]

that's even more bizarre

[Johan Commelin]

Right, that should clearly expand to α.

[Patrick Massot]

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

[Kevin Buzzard]

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 :-)

[Kevin Buzzard]

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

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

[Bryan Gin-ge Chen]

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.

[Kenny Lau]

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.

[Kenny Lau]

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

[Chris Hughes]

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?

[Kenny Lau]

I always save my file after I type every word

[Kenny Lau]

the latter

[Kenny Lau]

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

[Kenny Lau]

2018-09-07-2.png

[Kenny Lau]

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

[Kenny Lau]

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

[Chris Hughes]

What happens if you open from a file explorer?

[Kenny Lau]

it is also empty

[Kenny Lau]

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

[Kenny Lau]

hmm, it does show filter.univ_sets.

[Kenny Lau]

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

[Chris Hughes]

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

[Kevin Buzzard]

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.

[Kenny Lau]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Olli]

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

[Bryan Gin-ge Chen]

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...

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Kenny Lau]

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

[Keeley Hoek]

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

[Bryan Gin-ge Chen]

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

[Keeley Hoek]

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)?

[Sebastian Ullrich]

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.

[Kenny Lau]

2018-09-13.png
misplaced red underscore

[Kenny Lau]

code:

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

[Kenny Lau]

line 1 is normal, line 2 is not

[Kevin Buzzard]

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 :-)

[Patrick Massot]

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

[Gabriel Ebner]

"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.

[Gabriel Ebner]

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

[Johan Commelin]

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

[Gabriel Ebner]

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.

[Gabriel Ebner]

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

[Johan Commelin]

Lean is pretty sane. :big_smile:

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Keeley Hoek]

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 :'(

[Gabriel Ebner]

Does \\n work?

[Kenny Lau]

But my example has bo calligraphic characters!

[Keeley Hoek]

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

[Kenny Lau]

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

[Mario Carneiro]

Is your cursor unusually slow?

[Mario Carneiro]

or typing

[Mario Carneiro]

Or is it just lean being behind VSCode

[Kenny Lau]

the cursor is fine, and so is my typing

[Kenny Lau]

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

[Mario Carneiro]

That latter problem has hit me many times

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

so that the partial results take longer to compile

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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"

[Kevin Buzzard]

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

[Patrick Massot]

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

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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.

[Scott Morrison]

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.

[Kevin Buzzard]

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

[Scott Morrison]

Probably not.

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kenny Lau]

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 -/.

[Kenny Lau]

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

[Kenny Lau]

and I need to close and reopen VSCode

[Gabriel Ebner]

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

[Kevin Buzzard]

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".

[Kevin Buzzard]

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

[Gabriel Ebner]

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

[Simon Hudon]

That's a very lisp-y answer

[Kenny Lau]

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

[Johan Commelin]

@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...

[Johan Commelin]

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

[Gabriel Ebner]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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?

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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...

[Johan Commelin]

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.

[Neil Strickland]

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.

[Johan Commelin]

"subproof completed"?

[Neil Strickland]

Yes, that's probably good.

[Kevin Buzzard]

"Achievement unlocked". And a little happy sound.

[Kenny Lau]

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

[Johan Commelin]

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

[Edward Ayers]

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.

[Johan Commelin]

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

[Edward Ayers]

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.

[Bryan Gin-ge Chen]

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

[Edward Ayers]

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

[Johan Commelin]

@Bryan Gin-ge Chen Thanks for doing this!

[Edward Ayers]

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

[Gabriel Ebner]

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.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Gabriel Ebner]

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?

[Joseph Corneli]

calvin.png

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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 })

[Bryan Gin-ge Chen]

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.

[Johan Commelin]

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...

[Johan Commelin]

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

[Johan Commelin]

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.

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

I think this goal might have been accomplished!

[Patrick Massot]

Yes, I noticed that when helping students on Friday.

[Scott Morrison]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

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

[Floris van Doorn]

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

[Johan Commelin]

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?

[Edward Ayers]

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?

[Johan Commelin]

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.

[Johan Commelin]

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.

[Edward Ayers]

Ah I see.

[Johan Commelin]

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

[Edward Ayers]

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

[Edward Ayers]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Edward Ayers]

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.

[Johan Commelin]

I already have GitLens info there...

[Johan Commelin]

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.

[Bryan Gin-ge Chen]

How about as (yet) another status bar item?

[Johan Commelin]

That might work, yes

[Jesse Michael Han]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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?

[Bryan Gin-ge Chen]

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.

[Edward Ayers]

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.

[Edward Ayers]

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

[Gabriel Ebner]

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

[Wojciech Nawrocki]

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?

[Wojciech Nawrocki]

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

[Kevin Buzzard]

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
}

[Bryan Gin-ge Chen]

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.

[Wojciech Nawrocki]

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

[Kevin Buzzard]

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

[Rob Lewis]

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

[Bryan Gin-ge Chen]

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?

[Wojciech Nawrocki]

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)

[Wojciech Nawrocki]

@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 ? :)

[Bryan Gin-ge Chen]

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...

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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

[Johan Commelin]

Merci!

[Johan Commelin]

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

[Scott Morrison]

Anyone want to try this out?

[Scott Morrison]

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

[Kevin Buzzard]

vscode.png

[Kevin Buzzard]

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

[Scott Morrison]

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.

[Kevin Buzzard]

so we can both edit a Lean file

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

MWE:

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

Now use library_search or whatever to fill the hole.

[Gabriel Ebner]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Jesse Michael Han]

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) :^)

[Jesse Michael Han]

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

[Kenny Lau]

colouration_bug.png

[Kenny Lau]

the part in the red rectangle is coloured in yellow

[Kenny Lau]

but it should be just white

[Bryan Gin-ge Chen]

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

PR (merged in 0.14.2)

[Kenny Lau]

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

[Alexander Bentkamp]

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

[Keeley Hoek]

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

[Kenny Lau]

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

[Kenny Lau]

[Mario Carneiro]

what's invalid about it?

[Kenny Lau]

@Mario Carneiro unexpected token and invalid expression, unexpected token

[Kenny Lau]

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

[Bryan Gin-ge Chen]

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.

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

oh thanks

[Kenny Lau]

hidden in plain sight

[Kenny Lau]

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?

[Andrew Ashworth]

editor.wordSeparators

[Kenny Lau]

thanks

[Kenny Lau]

[Kenny Lau]

the angle brackets strike back

[Kenny Lau]

is this one governed by a different system?

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

that has since been fixed

[Kenny Lau]

so what should I do?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

so there's nothing I can do?

[Mario Carneiro]

you can PR to vscode-lean

[Mario Carneiro]

it's a bug in the syntax/language definition

[Kenny Lau]

done

[Mario Carneiro]

did you test it?

[Mario Carneiro]

if you downloaded the repo you should be able to hit f5 to start the extension

[Kenny Lau]

I'm not sure how to test it

[Mario Carneiro]

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

[Kenny Lau]

as in, I don't know how to modify the file locally

[Kenny Lau]

because I'm unable to locate the file

[Mario Carneiro]

didn't you just modify the file?

[Mario Carneiro]

src/extension.ts

[Kenny Lau]

but I edited it online and I don't know where is the file that my vscode is using

[Mario Carneiro]

if you get the repo and open it in vscode and hit f5, it will compile and run the extension in a new session

[Mario Carneiro]

it won't affect your current instance

[Mario Carneiro]

If you want to fix your current instance, you can copy the repo folder (after building it) into ~/.vscode/extensions

[Kenny Lau]

ah, ~/.vscode/extensions

[Kenny Lau]

that's the info I needed

[Mario Carneiro]

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

[Kenny Lau]

would there be any issue if I modify ~/.vscode/extensions directly?

[Kenny Lau]

you know how if I modify mathlib I need to recompile everything

[Mario Carneiro]

You may need to uninstall vscode-lean first

[Mario Carneiro]

but lean and mathlib are unaffected

[Mario Carneiro]

vscode-lean doesn't handle any of that, it just calls a thing on your machine called "lean"

[Greg Langmead]

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.

[Kevin Buzzard]

@Patrick Massot @Mohammad Pedramfar @Bryan Gin-ge Chen ?

[Greg Langmead]

I'm happy to get on the learning curve of the plugin and pitch in, if I can.

[Bryan Gin-ge Chen]

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.

[Rob Lewis]

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.

[Rob Lewis]

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.

[Greg Langmead]

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

[Rob Lewis]

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.

[Bryan Gin-ge Chen]

@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.

[Sebastien Gouezel]

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!

[Gabriel Ebner]

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.

[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.

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!

[Greg Langmead]

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.

[Bryan Gin-ge Chen]

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).]

[Greg Langmead]

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.

[Greg Langmead]

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.

[Greg Langmead]

@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.

[Greg Langmead]

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.

[Rob Lewis]

@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: $\mathbb{R}$ ?

[Johan Commelin]

@Rob Lewis Otoh, everyone is pretty used to $ foo $, and I don't think we'll actually hit many false positives.

[Johan Commelin]

We can always print regular $-signs by escaping them.

[Johan Commelin]

Can we check if there are "regular text $" occuring in mathlib right now? I doubt it.

[Gabriel Ebner]

The only occurrence I can see is `foo $ bar $ baz 10`

[Rob Lewis]

$ 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.

[Rob Lewis]

People are used to $$..$$ from Zulip too.

[Johan Commelin]

$ 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.

[Greg Langmead]

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.

[Greg Langmead]

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:

[Greg Langmead]

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

[Rob Lewis]

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.

[Rob Lewis]

Thanks very much @Greg Langmead !

[Sebastien Gouezel]

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?

[Bryan Gin-ge Chen]

I think it's possible. I will try to find time to add it.

[Bryan Gin-ge Chen]

@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.

[Sebastien Gouezel]

I just tried it on #1952, and I get a nicely formatted equation, but also a weird docstring.

[Bryan Gin-ge Chen]

@Sebastien Gouezel Thanks for the example! I think it's fixed now: https://observablehq.com/@bryangingechen/github-lean-doc-preview?url=%221952%22

[Sebastien Gouezel]

Amazing, thanks a lot!

[Kenny Lau]

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 (ℕ).

[Kevin Buzzard]

Press the space bar :-)

[Gabriel Ebner]

If we're already talking about workarounds, you can always press TAB to trigger the conversion.

[Kenny Lau]

oh wow I never knew that

[Kenny Lau]

I was like, why isn't there any way to trigger the conversion without moving my damn cursor

[Patrick Massot]

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?

[Patrick Massot]

https://github.com/leanprover/vscode-lean/releases

[Johan Commelin]

What do people think of add shortcuts \inf for \glb and \sup for \lub?

[Kevin Buzzard]

When I was learning lattices I typed \inf and \sup so many times!

[Kevin Buzzard]

I'd definitely be in favour.

[Bhavik Mehta]

Would there be a clash with \infty? (I haven't needed to use it but perhaps those who have wouldn't like this)

[Mario Carneiro]

and apparently \supseteq

[Gabriel Ebner]

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?

[Mario Carneiro]

I get this for writing initial segments of \supseteq:

\supseteq
 σ⊆⊇⊃⊃⊃⊇⊇

[Mario Carneiro]

I think ⊇ must be registered as both \sup and \supseteq for this behavior to occur