## Stream: general

### Topic: VScode extension

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

#### Mario Carneiro (Jul 25 2018 at 10:42):

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

Not here

#### Mario Carneiro (Jul 25 2018 at 10:43):

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

#### Mario Carneiro (Jul 25 2018 at 10:44):

You can set your key bindings yourself btw

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

#### Patrick Massot (Jul 25 2018 at 10:45):

How do you setup keybindings?

#### Mario Carneiro (Jul 25 2018 at 10:46):

file > prefs > key shortcuts

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

#### Mario Carneiro (Jul 25 2018 at 10:47):

this is what emacs does

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

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

#### Johan Commelin (Jul 25 2018 at 10:49):

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

I believe so

Nice

#### Mario Carneiro (Jul 25 2018 at 10:49):

I think vscode does the same in that case

#### Johan Commelin (Jul 25 2018 at 10:49):

Hmm, maybe it does.

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

#### Johan Commelin (Jul 25 2018 at 10:50):

I think vscode does the same in that case

You are right.

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

#### Mario Carneiro (Jul 25 2018 at 10:53):

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

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

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

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

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

#### Patrick Massot (Jul 25 2018 at 10:58):

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

#### Patrick Massot (Jul 25 2018 at 10:58):

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

#### Patrick Massot (Jul 25 2018 at 10:59):

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

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

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

#### Gabriel Ebner (Jul 27 2018 at 20:12):

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

#### Gabriel Ebner (Jul 27 2018 at 20:12):

afk hornet in the room

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

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

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

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

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

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

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

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

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

#### Chris Hughes (Jul 28 2018 at 10:25):

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

#### Chris Hughes (Jul 28 2018 at 10:26):

Maybe I should update lean?

#### Ali Sever (Jul 28 2018 at 10:26):

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

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

#### Ali Sever (Jul 28 2018 at 10:34):

how did you close your lean files?

#### Chris Hughes (Jul 28 2018 at 10:35):

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

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

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

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

#### Chris Hughes (Jul 28 2018 at 10:51):

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

#### Chris Hughes (Jul 28 2018 at 10:55):

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

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

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

#### Chris Hughes (Jul 28 2018 at 15:13):

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

#### Chris Hughes (Jul 28 2018 at 15:14):

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

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

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

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

#### Ali Sever (Jul 28 2018 at 15:41):

Thanks Chris, awesome as always

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

#### Ali Sever (Jul 28 2018 at 17:15):

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

#### Chris Hughes (Jul 28 2018 at 17:16):

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

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

#### Ali Sever (Jul 28 2018 at 17:16):

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

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

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

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

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

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

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

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

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

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

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

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

#### Patrick Massot (Jul 29 2018 at 21:48):

This would be really really helpful

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

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

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

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

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

#### Gabriel Ebner (Jul 30 2018 at 21:12):

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

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

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

#### 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{(\[,:]+)*)

#### Kevin Buzzard (Jul 30 2018 at 21:58):

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

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


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

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

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

#### Kenny Lau (Aug 03 2018 at 08:19):

ctrl+alt+shift+enter

#### Johan Commelin (Aug 03 2018 at 08:20):

What the hack is that supposed to do?

#### Johan Commelin (Aug 03 2018 at 08:20):

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

#### Kenny Lau (Aug 03 2018 at 08:20):

it lets you view all the messages

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

#### Johan Commelin (Aug 03 2018 at 09:12):

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

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

#### Johan Commelin (Aug 10 2018 at 07:30):

@Gabriel Ebner :up:

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

#### Kenny Lau (Aug 10 2018 at 10:31):

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

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

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

Right

#### Gabriel Ebner (Aug 10 2018 at 10:39):

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

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

#### 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!

#### Johan Commelin (Aug 10 2018 at 10:42):

Ok, I should try that out.

#### 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!

#### Gabriel Ebner (Aug 10 2018 at 10:48):

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

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

#### Johan Commelin (Aug 10 2018 at 15:24):

I should prod William about CoCalc.

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

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

#### Kenny Lau (Aug 18 2018 at 21:26):

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

#### Kenny Lau (Aug 18 2018 at 21:31):

wait it works now

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

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

#### 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"?

#### Johan Commelin (Aug 30 2018 at 18:20):

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

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

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

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

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

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

#### Gabriel Ebner (Aug 30 2018 at 18:52):

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

#### Johan Commelin (Aug 30 2018 at 18:56):

Clippy was not really serious...

#### Johan Commelin (Aug 30 2018 at 18:56):

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

#### Johan Commelin (Aug 30 2018 at 18:57):

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

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

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

#### Gabriel Ebner (Aug 31 2018 at 13:03):

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

#### Mario Carneiro (Aug 31 2018 at 13:04):

I think that this is used for natural transformations

#### Gabriel Ebner (Aug 31 2018 at 13:05):

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

#### Johan Commelin (Aug 31 2018 at 13:05):

\hom and \==>

#### Johan Commelin (Aug 31 2018 at 13:06):

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

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

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

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

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

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

#### Johan Commelin (Aug 31 2018 at 13:14):

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

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

#### Gabriel Ebner (Aug 31 2018 at 13:15):

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

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

#### Johan Commelin (Aug 31 2018 at 13:16):

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

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

#### Gabriel Ebner (Aug 31 2018 at 13:16):

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

Exactly

#### Johan Commelin (Aug 31 2018 at 13:17):

Oops, that is silly

#### Johan Commelin (Aug 31 2018 at 13:20):

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

And deployed.

#### Johan Commelin (Aug 31 2018 at 13:25):

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

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


#### Johan Commelin (Aug 31 2018 at 13:27):

That's the silly thing that I'm trying

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

#### Mario Carneiro (Aug 31 2018 at 13:50):

are you going to claim it as a global notation?

#### Johan Commelin (Aug 31 2018 at 13:55):

Of course! We are evil!

#### Mario Carneiro (Aug 31 2018 at 13:56):

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

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

#### Patrick Massot (Aug 31 2018 at 14:28):

Gabriel, why do you hardcode the leader key?

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

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

#### Mario Carneiro (Aug 31 2018 at 14:50):

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

#### Patrick Massot (Aug 31 2018 at 14:50):

only if the abbreviation starts with a space

#### Patrick Massot (Aug 31 2018 at 14:51):

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

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

#### Patrick Massot (Aug 31 2018 at 14:52):

under what kind of circumstances?

#### Mario Carneiro (Aug 31 2018 at 14:53):

λ⟨a,b⟩,  and such

this is wrong

should be a, b

#### Mario Carneiro (Aug 31 2018 at 14:53):

also between rewrite rules and simp rules sometimes

#### Mario Carneiro (Aug 31 2018 at 14:53):

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

#### Patrick Massot (Aug 31 2018 at 14:54):

So switching to comma would improve typography in mathlib!

#### Johan Commelin (Aug 31 2018 at 14:54):

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

#### Johan Commelin (Aug 31 2018 at 14:54):

Or just map your caps lock to \

#### Gabriel Ebner (Aug 31 2018 at 14:55):

I thought French keyboards have a key for §?

no

#### Patrick Massot (Aug 31 2018 at 14:56):

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

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

#### Johan Commelin (Aug 31 2018 at 14:57):

It seems to be Shift + !

#### Gabriel Ebner (Aug 31 2018 at 14:57):

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

#### Patrick Massot (Aug 31 2018 at 14:57):

it's there, but not on direct access

#### Patrick Massot (Aug 31 2018 at 14:57):

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

#### Johan Commelin (Aug 31 2018 at 14:58):

Make ù the leader (-;

#### Patrick Massot (Aug 31 2018 at 15:00):

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

#### Edward Ayers (Aug 31 2018 at 15:02):

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

#### Gabriel Ebner (Aug 31 2018 at 15:03):

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

#### Patrick Massot (Aug 31 2018 at 15:04):

what is a code formatter?

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

#### Edward Ayers (Aug 31 2018 at 15:05):

Basically it adds and removes spaces until the code looks nice

#### Patrick Massot (Aug 31 2018 at 15:07):

that would be really nice

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

#### Edward Ayers (Aug 31 2018 at 15:17):

I think that you can in theory perform arbitrary textual transformations

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

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

#### Patrick Massot (Aug 31 2018 at 15:50):

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

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

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

2018-09-04.png

#### Kevin Buzzard (Sep 04 2018 at 09:31):

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

#### Kenny Lau (Sep 04 2018 at 09:34):

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


#### Johan Commelin (Sep 04 2018 at 09:34):

Also, why did you put that in this thread?

#### Patrick Massot (Sep 04 2018 at 09:39):

I guess Kenny wants to complain about syntax highlighting

#### Kevin Buzzard (Sep 04 2018 at 10:00):

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

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

#### Bryan Gin-ge Chen (Sep 04 2018 at 13:38):

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

#### 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+[

#### Johan Commelin (Sep 05 2018 at 18:26):

Alternative: Tab or Shift-Tab

#### Patrick Massot (Sep 05 2018 at 18:26):

also works with Tab and Shift-Tab

oh right

#### 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 (-;

#### Kevin Buzzard (Sep 05 2018 at 18:30):

Did you try \G?

#### Kevin Buzzard (Sep 05 2018 at 18:30):

that's even more bizarre

#### Johan Commelin (Sep 05 2018 at 18:32):

Right, that should clearly expand to α.

#### Patrick Massot (Sep 05 2018 at 18:34):

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

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

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

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

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

#### Kenny Lau (Sep 07 2018 at 13:42):

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

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

#### Kenny Lau (Sep 07 2018 at 13:44):

I always save my file after I type every word

the latter

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

2018-09-07-2.png

#### Kenny Lau (Sep 07 2018 at 13:46):

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

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

#### Chris Hughes (Sep 07 2018 at 13:51):

What happens if you open from a file explorer?

it is also empty

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

#### Kenny Lau (Sep 08 2018 at 08:40):

hmm, it does show filter.univ_sets.

#### Kenny Lau (Sep 08 2018 at 08:40):

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

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

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

#### Kenny Lau (Sep 08 2018 at 21:28):

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

#### Mario Carneiro (Sep 08 2018 at 21:33):

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

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

#### Olli (Sep 08 2018 at 21:53):

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

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

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

#### Bryan Gin-ge Chen (Sep 08 2018 at 22:52):

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

#### Kenny Lau (Sep 09 2018 at 12:57):

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

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

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

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

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

#### Kenny Lau (Sep 13 2018 at 07:26):

2018-09-13.png
misplaced red underscore

#### Kenny Lau (Sep 13 2018 at 07:27):

code:

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


#### Kenny Lau (Sep 13 2018 at 07:27):

line 1 is normal, line 2 is not

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

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

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

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

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

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

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

#### Johan Commelin (Sep 13 2018 at 12:51):

Lean is pretty sane. :big_smile:

#### 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!

#### Johan Commelin (Sep 13 2018 at 12:52):

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

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

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

#### Johan Commelin (Sep 13 2018 at 12:53):

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

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

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

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

Does \\n work?

#### Kenny Lau (Sep 13 2018 at 14:08):

But my example has bo calligraphic characters!

#### Keeley Hoek (Sep 13 2018 at 14:18):

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

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

or typing

#### Mario Carneiro (Sep 30 2018 at 08:25):

Or is it just lean being behind VSCode

#### Kenny Lau (Sep 30 2018 at 08:25):

the cursor is fine, and so is my typing

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

#### Mario Carneiro (Sep 30 2018 at 08:27):

That latter problem has hit me many times

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

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

#### Mario Carneiro (Sep 30 2018 at 08:29):

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

#### Mario Carneiro (Sep 30 2018 at 08:29):

so that the partial results take longer to compile

#### Kenny Lau (Sep 30 2018 at 08:33):

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

#### Mario Carneiro (Sep 30 2018 at 08:33):

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

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

#### Kevin Buzzard (Oct 02 2018 at 15:22):

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

#### Patrick Massot (Oct 02 2018 at 15:49):

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

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

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

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

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

Probably not.

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

#### Patrick Massot (Oct 03 2018 at 09:41):

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

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

#### Kenny Lau (Oct 11 2018 at 15:25):

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

#### Kenny Lau (Oct 11 2018 at 15:25):

and I need to close and reopen VSCode

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

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

#### Kevin Buzzard (Oct 13 2018 at 10:28):

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

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

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

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

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

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

#### Johan Commelin (Nov 15 2018 at 10:04):

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

#### Johan Commelin (Nov 15 2018 at 10:04):

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

#### Johan Commelin (Nov 15 2018 at 10:05):

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

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

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

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

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

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

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

#### Johan Commelin (Feb 13 2019 at 12:53):

"subproof completed"?

#### Neil Strickland (Feb 13 2019 at 12:54):

Yes, that's probably good.

#### Kevin Buzzard (Feb 13 2019 at 12:55):

"Achievement unlocked". And a little happy sound.

#### Kenny Lau (Feb 13 2019 at 13:29):

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

#### Johan Commelin (Feb 13 2019 at 13:34):

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

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

#### Johan Commelin (Feb 13 2019 at 15:58):

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

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

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

#### Edward Ayers (Feb 13 2019 at 16:10):

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

#### Johan Commelin (Feb 13 2019 at 16:14):

@Bryan Gin-ge Chen Thanks for doing this!

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

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

#### Bryan Gin-ge Chen (Feb 13 2019 at 16:33):

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

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

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

calvin.png

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

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

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

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

#### Johan Commelin (Feb 13 2019 at 17:33):

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

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

#### Bryan Gin-ge Chen (Feb 21 2019 at 15:29):

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

#### 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!

#### Patrick Massot (Mar 23 2019 at 20:48):

Yes, I noticed that when helping students on Friday.

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

#### Johan Commelin (Mar 25 2019 at 08:58):

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

#### Johan Commelin (Mar 25 2019 at 08:58):

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

#### Johan Commelin (Mar 25 2019 at 08:59):

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

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

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

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


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

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

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

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

Ah I see.

#### Johan Commelin (Mar 27 2019 at 19:56):

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

#### Edward Ayers (Mar 27 2019 at 19:56):

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

#### Edward Ayers (Mar 27 2019 at 19:57):

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

#### Johan Commelin (Mar 27 2019 at 19:57):

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

#### Johan Commelin (Mar 27 2019 at 19:58):

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

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

#### Johan Commelin (Mar 27 2019 at 20:01):

I already have GitLens info there...

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

#### Bryan Gin-ge Chen (Mar 27 2019 at 20:03):

How about as (yet) another status bar item?

#### Johan Commelin (Mar 27 2019 at 20:04):

That might work, yes

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

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

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

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

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

#### Edward Ayers (Mar 28 2019 at 11:16):

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

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

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

#### Wojciech Nawrocki (Mar 31 2019 at 14:09):

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

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


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

#### Wojciech Nawrocki (Mar 31 2019 at 15:08):

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

#### Kevin Buzzard (Mar 31 2019 at 15:09):

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

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

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

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

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

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

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

#### Johan Commelin (Apr 01 2019 at 06:00):

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

Merci!

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

#### Scott Morrison (Apr 02 2019 at 22:14):

Anyone want to try this out?

#### Scott Morrison (Apr 02 2019 at 22:15):

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

vscode.png

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

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

#### Kevin Buzzard (Apr 02 2019 at 22:42):

so we can both edit a Lean file

#### Kevin Buzzard (Apr 02 2019 at 22:42):

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

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

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

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

#### 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 {! !}.

#### Johan Commelin (Apr 23 2019 at 13:34):

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

#### Johan Commelin (Apr 23 2019 at 13:35):

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

#### Johan Commelin (Apr 23 2019 at 13:35):

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

#### Johan Commelin (Apr 23 2019 at 13:35):

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

#### Kevin Buzzard (Apr 23 2019 at 13:36):

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

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

#### Jesse Michael Han (Apr 23 2019 at 14:30):

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

#### Kenny Lau (Jun 10 2019 at 01:59):

colouration_bug.png

#### Kenny Lau (Jun 10 2019 at 02:00):

the part in the red rectangle is coloured in yellow

#### Kenny Lau (Jun 10 2019 at 02:00):

but it should be just white

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

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

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

#### Keeley Hoek (Jul 04 2019 at 11:19):

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

#### Kenny Lau (Jul 11 2019 at 20:53):

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

#### Kenny Lau (Jul 11 2019 at 21:06):

@Mario Carneiro unexpected token and invalid expression, unexpected token

#### Kenny Lau (Jul 11 2019 at 21:06):

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


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

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

#### Mario Carneiro (Dec 05 2019 at 03:12):

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

oh thanks

#### Kenny Lau (Dec 05 2019 at 03:15):

hidden in plain sight

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

#### Andrew Ashworth (Dec 27 2019 at 02:27):

editor.wordSeparators

thanks

#### Kenny Lau (Dec 31 2019 at 10:42):

the angle brackets strike back

#### Kenny Lau (Dec 31 2019 at 10:42):

is this one governed by a different system?

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

#### Mario Carneiro (Dec 31 2019 at 10:44):

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

#### Mario Carneiro (Dec 31 2019 at 10:45):

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

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

#### Mario Carneiro (Dec 31 2019 at 10:48):

that has since been fixed

#### Kenny Lau (Dec 31 2019 at 10:50):

so what should I do?

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

#### Mario Carneiro (Dec 31 2019 at 10:50):

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

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

#### Kenny Lau (Dec 31 2019 at 10:51):

so there's nothing I can do?

#### Mario Carneiro (Dec 31 2019 at 10:51):

you can PR to vscode-lean

#### Mario Carneiro (Dec 31 2019 at 10:52):

it's a bug in the syntax/language definition

done

did you test it?

#### Mario Carneiro (Dec 31 2019 at 10:55):

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

#### Kenny Lau (Dec 31 2019 at 10:57):

I'm not sure how to test it

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

#### Kenny Lau (Dec 31 2019 at 10:59):

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

#### Kenny Lau (Dec 31 2019 at 10:59):

because I'm unable to locate the file

#### Mario Carneiro (Dec 31 2019 at 11:00):

didn't you just modify the file?

#### Mario Carneiro (Dec 31 2019 at 11:00):

src/extension.ts

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

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

#### Mario Carneiro (Dec 31 2019 at 11:04):

it won't affect your current instance

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

#### Kenny Lau (Dec 31 2019 at 11:06):

ah, ~/.vscode/extensions

#### Kenny Lau (Dec 31 2019 at 11:06):

that's the info I needed

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

#### Kenny Lau (Dec 31 2019 at 11:07):

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

#### Kenny Lau (Dec 31 2019 at 11:07):

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

#### Mario Carneiro (Dec 31 2019 at 11:07):

You may need to uninstall vscode-lean first

#### Mario Carneiro (Dec 31 2019 at 11:07):

but lean and mathlib are unaffected

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

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

#### Kevin Buzzard (Jan 31 2020 at 03:24):

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

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

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

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

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

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

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

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

#### 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!

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

#### 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!

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

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

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

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

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

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

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

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

#### Gabriel Ebner (Feb 03 2020 at 10:09):

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

$ 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 (Feb 03 2020 at 10:10): People are used to $..$ from Zulip too. #### 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.

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

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

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

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

#### Rob Lewis (Feb 03 2020 at 15:01):

Thanks very much @Greg Langmead !

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

#### Bryan Gin-ge Chen (Feb 04 2020 at 11:25):

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

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

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

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

#### Sebastien Gouezel (Feb 05 2020 at 07:39):

Amazing, thanks a lot!

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

#### Kevin Buzzard (Apr 13 2020 at 09:51):

Press the space bar :-)

#### Gabriel Ebner (Apr 13 2020 at 09:54):

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

#### Kenny Lau (Apr 13 2020 at 09:56):

oh wow I never knew that

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

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

#### Patrick Massot (May 05 2020 at 20:29):

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

#### Johan Commelin (May 12 2020 at 12:45):

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

#### Kevin Buzzard (May 12 2020 at 12:49):

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

#### Kevin Buzzard (May 12 2020 at 12:49):

I'd definitely be in favour.

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

#### Mario Carneiro (May 12 2020 at 12:55):

and apparently \supseteq

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

#### Mario Carneiro (May 12 2020 at 13:10):

I get this for writing initial segments of \supseteq:

\supseteq
σ⊆⊇⊃⊃⊃⊇⊇


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