## Stream: general

### Topic: vscode-lean 0.11.0

#### Gabriel Ebner (Apr 21 2018 at 17:26):

I just pushed a new update for the vscode extension. A few bugfixes and features have accumulated over the last few months:

• The new visibleRanges API in vscode is supported now. Per default, we no longer check the whole file on every keystroke, but only the currently visible lines (and the rest of the file above). This new API is only present in vscode >=1.22 (released in March), no idea if it works with older vscode versions. Please complain (or upgrade) if you run into any troubles.
• You can now input ⦃⦄ using \{{
• Fewer complaints about leanpkg.path changes.

#### Mario Carneiro (Apr 21 2018 at 20:28):

can you also type ⟦⟧ using \[[?

No, it seems.

#### Patrick Massot (Apr 21 2018 at 20:48):

How do you check what version of the extension is used? How do you upgrade?

#### Chris Hughes (Apr 21 2018 at 20:54):

I clicked on extensions on the left pane, and I clicked the reload button. Try typing \{{ and if it turns into special brackets, you have the upgrade.

#### Patrick Massot (Apr 21 2018 at 20:55):

I didn't see a reload button

I'll search more

#### Chris Hughes (Apr 21 2018 at 20:55):

I have a feeling it might do it automatically if you restart, so I would try the brackets thing.

#### Patrick Massot (Apr 21 2018 at 20:56):

Ok, I've found a menu containg "search updates" (or something like this, this part is in French here)

I'm updated

#### Gabriel Ebner (Apr 22 2018 at 06:49):

can you also type ⟦⟧ using \[[?

You can, as of a minute ago.

Thank you!

#### Patrick Massot (Apr 22 2018 at 09:33):

Very easy suggestion: make a command (usable through Ctrl-p like the Restart server command) that opens up https://github.com/leanprover/vscode-lean/blob/master/translations.json in a new tab (not fetching it from the web, opening the one which is actually used on the current install)

#### Patrick Massot (Apr 23 2018 at 14:31):

What about having syntax highlighting in the Lean message window? Would that be complicated to do?

#### Gabriel Ebner (Apr 23 2018 at 14:52):

If "message window" is the info view (with the pause button on the top right), then this is a bit complicated. Unfortunately we do not have any programmatic access to vscode's syntax highlighter. AFAIK there is also no pure javascript package that can use these syntax highlighting files. I'll keep it in mind though.

#### Patrick Massot (Apr 23 2018 at 14:53):

Yes this is what I meant. We do spend quite some time staring at this window, and it's a bit austere.

#### Patrick Massot (May 08 2018 at 15:58):

If "message window" is the info view (with the pause button on the top right), then this is a bit complicated. Unfortunately we do not have any programmatic access to vscode's syntax highlighter. AFAIK there is also no pure javascript package that can use these syntax highlighting files. I'll keep it in mind though.

I just played a bit with this. Here is what I currently see in my VScode:

#### Patrick Massot (May 08 2018 at 15:59):

colored_tactic_state.png

#### Patrick Massot (May 08 2018 at 15:59):

I think it's already useful (to me at least)

#### Patrick Massot (May 08 2018 at 16:00):

It's super low tech and unreliable, based on:

function formatTacticState(s: string): string {
return s
.replace(/^(\d+ goals)/g, '<strong style="color:#569cd6;">$1</strong> :') .replace(/^([^ ][^:\n⊢]*) :/g, '<strong style="color:#dcdc00;">$1</strong> :')
}


#### Patrick Massot (May 08 2018 at 16:09):

Reading infoview.css is very interesting

#### Patrick Massot (May 08 2018 at 16:09):

Indeed it should be very easy to use

#### Gabriel Ebner (May 08 2018 at 16:33):

The colorization has been deployed. Please complain if the fancy colors distract you too much.

Wow, you're fast

#### Patrick Massot (May 08 2018 at 16:35):

I was working on it

#### Patrick Massot (May 08 2018 at 16:35):

But not fast enough :wink:

#### Patrick Massot (May 08 2018 at 16:36):

I didn't know about the m flag in replace

#### Patrick Massot (May 08 2018 at 16:38):

There can be space before the colon

#### Patrick Massot (May 08 2018 at 16:38):

when several variables share a common type

bug.png

#### Patrick Massot (May 08 2018 at 16:39):

But I do like this orange

#### Patrick Massot (May 08 2018 at 16:41):

Also, you forgot the | showing current goal in conversion mode

#### Patrick Massot (May 08 2018 at 16:41):

In my current version I gave it the same formatting as the ⊢

#### Gabriel Ebner (May 08 2018 at 16:47):

Should be fixed now.

Nice!

oh oh...

New bug

#### Patrick Massot (May 08 2018 at 16:54):

I also had that one at some point

bug2.png

#### Patrick Massot (May 08 2018 at 16:56):

I can see you are too much used to proved software. In the real world you need to test your software with real world data

#### Sebastian Ullrich (May 08 2018 at 16:57):

In Emacs, all flycheck errors are now highlighted with the Lean syntax highlighter btw

:)

#### Patrick Massot (May 08 2018 at 16:57):

For the record, before you told us you 0.11.2 was out, the state of my regexs was:

function formatTacticState(s: string): string {
return s
.replace(/^(\d+ goals)/g, '<strong class="goals-number">$1</strong> :') .replace(/^([^ ][^:\n⊢]*) :/g, '<strong class="context-element">$1</strong> :')
.replace(/\n([^ ⊢][^:\n⊢]*) :/g, '\n<strong class="context-element">$1</strong> :') .replace(/^case ([^\n]*)/g, '<strong class="case">case$1</strong> :')
.replace(/\ncase ([^\n]*)/g, '\n<strong class="case">case \$1</strong> :')
.replace(/^⊢/g, '<strong class="goal">⊢</strong>')
.replace(/\n⊢/g, '\n<strong class="goal">⊢</strong>')
.replace(/^\|/g, '<strong class="goal">|</strong>')
.replace(/\n\|/g, '\n<strong class="goal">|</strong>')
.replace(/no goals/g, '🎉 ');
}


#### Patrick Massot (May 08 2018 at 16:58):

I should really try Lean in spacemacs at some point

#### Patrick Massot (May 08 2018 at 16:59):

I don't why I'm affraid

#### Sebastian Ullrich (May 08 2018 at 16:59):

I should really write a Lean spacemacs layer at some point

#### Patrick Massot (May 08 2018 at 17:00):

Sebastian, do you have plans to make more structured tactic state output in Lean 4?

#### Patrick Massot (May 08 2018 at 17:00):

Like, we wouldn't have to regex the output

#### Patrick Massot (May 08 2018 at 17:01):

It could be useful also to build more powerful IDEs

#### Patrick Massot (May 08 2018 at 17:02):

(where we could click on stuff in the tactic state and see cool things happen)

#### Sebastian Ullrich (May 08 2018 at 17:04):

@Patrick Massot https://github.com/leanprover/lean/issues/1693

#### Patrick Massot (May 08 2018 at 17:08):

Ok, I see you already discussed this quite a bit

#### Patrick Massot (May 08 2018 at 17:08):

Is this in the Lean 4 TODO list then? I guess the priority is not super high

#### Sebastian Ullrich (May 08 2018 at 17:46):

We're currently more focused on the structured traces (https://github.com/leanprover/lean/issues/1692) since that influences how we write Lean-in-Lean code. I suspect structured term output will come a bit later.

Great

#### Gabriel Ebner (May 09 2018 at 06:34):

I can see you are too much used to proved software. In the real world you need to test your software with real world data

:smile: We don't have a single test in vscode-lean. But the new bug is fixed now.

#### Kevin Buzzard (May 09 2018 at 06:57):

Patrick do you test your theorems about manifolds with real world data?

#### Patrick Massot (May 09 2018 at 07:29):

Of course I do! How else could we get confidence in our theorems until proof assistants are ready for the real battlefield?

#### Patrick Massot (May 09 2018 at 07:29):

Have a look at my latest preprint for instance

#### Patrick Massot (May 09 2018 at 07:29):

The main result is checked against the canonical contact structures on spheres and projective spaces

#### Patrick Massot (May 09 2018 at 07:31):

Conclusions were already known to hold for spheres and known not to hold for projective spaces (with the nice corollary that the hypothesis of the theorem does not hold for projective spaces, something that we have no other way to prove at the moment)

#### Patrick Massot (May 09 2018 at 07:31):

Oh crap, my VScode doesn't like the tada unicode in the Tactic state window

#### Patrick Massot (May 09 2018 at 07:31):

I forgot I kept that experiment in the regex I posted

#### Gabriel Ebner (May 09 2018 at 07:34):

I tried it and the tada emoji works here, but I have a font installed for it.

#### Gabriel Ebner (May 09 2018 at 07:38):

I have just enabled the highlighting for error messages as well. It looks a bit weird for #print results, but I think it's a definite improvement for failed tactics.

#### Mario Carneiro (May 09 2018 at 07:48):

I recommend against seriously using the tada emoji in the vscode extension

#### Mario Carneiro (May 09 2018 at 07:48):

At least put it after the words "no goals"

#### Gabriel Ebner (May 09 2018 at 07:50):

Yes, it comes right after the two words. But I'll remove it.

#### Patrick Massot (May 09 2018 at 15:54):

bug2.png

This also happen in conversion mode...

#### Patrick Massot (May 13 2018 at 20:18):

Here is tricky new bug: #reduce λ x, x. Maybe we should try to detect information reduce result on top

#### Patrick Massot (May 23 2018 at 19:35):

@Gabriel Ebner Same remark about detecting class instance trace (and probably also other kinds of traces?)

#### Gabriel Ebner (May 24 2018 at 09:47):

We skip all information messages now. I kind of liked it that trace_state was colorized, but we can't distinguish it from a class trace.

#### Johan Commelin (May 25 2018 at 09:50):

I have no clue at all if this is possible: can you show matching parens in the goal. (So if I select one, the other gets some highlighting?)

#### Gabriel Ebner (May 25 2018 at 09:51):

It's possible. But we'd have to implement the highlight code ourselves (it's just an html page with javascript).

#### Johan Commelin (May 25 2018 at 10:00):

Ok, but there is probably some js lib doing this already, right?

#### Gabriel Ebner (May 25 2018 at 10:16):

I didn't find anything off-the-shelf after a quick search. But it shouldn't be too hard. Listen to mouse move events, if we're over a (, [, or { inside a <pre>, then look for a matching paren and put a <span class='paren-highlighted'> around it, and remove previous .paren-highlighted spans.

#### Mario Carneiro (May 25 2018 at 10:48):

@Gabriel Ebner I have vscode-lean github downloaded and hooked up to my VSCode install, but I forget how to compile the extension from source. Could you remind me (and possibly put the instructions on the README)?

#### Gabriel Ebner (May 25 2018 at 10:50):

The easiest way is to open the extension in vscode and press F5. This will compile it and start a new vscode window with the development version of the extension. This is also documented in the README: https://github.com/leanprover/vscode-lean#development

Last updated: May 10 2021 at 19:16 UTC