vscode-lean 0.11.0

Stream: general

[Gabriel Ebner]

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]

can you also type ⟦⟧ using \[[?

[Chris Hughes]

No, it seems.

[Patrick Massot]

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

[Chris Hughes]

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]

I didn't see a reload button

[Patrick Massot]

I'll search more

[Chris Hughes]

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

[Patrick Massot]

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

[Patrick Massot]

I'm updated

[Gabriel Ebner]

can you also type ⟦⟧ using \[[?

You can, as of a minute ago.

[Patrick Massot]

Thank you!

[Patrick Massot]

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]

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

[Gabriel Ebner]

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]

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

[Patrick Massot]

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]

colored_tactic_state.png

[Patrick Massot]

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

[Patrick Massot]

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> :')
        .replace(/\n([^ ⊢][^:\n⊢]*) :/g, '\n<strong style="color:#dcdc00;">$1</strong> :')
        .replace(/\n⊢/g, '\n<strong style="color:#569cd6;">⊢</strong>');
}

[Patrick Massot]

Which is called in InfoProvider.renderGoal

[Patrick Massot]

@Gabriel Ebner What do you think about that?

[Mario Carneiro]

I would object to this on purity grounds, but TBH the standard syntax highlighter isn't much better

[Patrick Massot]

Indeed it couldn't be less pure

[Patrick Massot]

And the next Lean file I'll open will probably tell me I missed some edge case

[Mario Carneiro]

You can probably parse a tactic print string pretty reliably by classifying the lines that don't start with whitespace

[Patrick Massot]

But Gabriel told me the syntax highlighter is not available here

[Patrick Massot]

Yes, a classification function would help

[Patrick Massot]

At least make things more modular

[Patrick Massot]

With the above method, trying to catch anything new would likely break things

[Gabriel Ebner]

This looks great! I'll just make sure it is also readable with a white background.

[Mario Carneiro]

don't forget the case line of tactic state

[Patrick Massot]

There should be away to have proper CSS interacting with the selected theme instead of hardcoded colors

[Mario Carneiro]

presumably it's as simple as just <span class="x">

[Patrick Massot]

The question is not there: where should we put classes definitions?

[Gabriel Ebner]

@Patrick Massot did you just put the <strong> inside the <pre>?

[Gabriel Ebner]

The CSS is in infoview.css

[Patrick Massot]

    private renderGoal() {
        if (!this.curGoalState || this.displayMode !== DisplayMode.OnlyState) { return ''; }
        return `<div id="goal"><h1>Tactic State</h1><pre>${formatTacticState(escapeHtml(this.curGoalState))}</pre></div>`;
    }

[Patrick Massot]

Reading infoview.css is very interesting

[Patrick Massot]

Indeed it should be very easy to use

[Gabriel Ebner]

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

[Patrick Massot]

Wow, you're fast

[Patrick Massot]

I was working on it

[Patrick Massot]

But not fast enough :wink:

[Patrick Massot]

I didn't know about the m flag in replace

[Patrick Massot]

https://github.com/leanprover/vscode-lean/commit/8a1e35e6495593620fbaacad5ff98929c15c7793#diff-66e057b4386ca2dfc39356a2fbecb4f2R354 is not good

[Patrick Massot]

There can be space before the colon

[Patrick Massot]

when several variables share a common type

[Patrick Massot]

bug.png

[Patrick Massot]

But I do like this orange

[Patrick Massot]

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

[Patrick Massot]

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

[Gabriel Ebner]

Should be fixed now.

[Patrick Massot]

Nice!

[Patrick Massot]

oh oh...

[Patrick Massot]

New bug

[Patrick Massot]

I also had that one at some point

[Patrick Massot]

bug2.png

[Patrick Massot]

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]

It's spreading!

[Sebastian Ullrich]

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

[Sebastian Ullrich]

:)

[Patrick Massot]

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]

I should really try Lean in spacemacs at some point

[Patrick Massot]

I don't why I'm affraid

[Sebastian Ullrich]

I should really write a Lean spacemacs layer at some point

[Patrick Massot]

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

[Patrick Massot]

Like, we wouldn't have to regex the output

[Patrick Massot]

It could be useful also to build more powerful IDEs

[Patrick Massot]

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

[Sebastian Ullrich]

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

[Patrick Massot]

Ok, I see you already discussed this quite a bit

[Patrick Massot]

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

[Sebastian Ullrich]

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.

[Patrick Massot]

Great

[Gabriel Ebner]

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]

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

[Patrick Massot]

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

[Patrick Massot]

Have a look at my latest preprint for instance

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

I forgot I kept that experiment in the regex I posted

[Gabriel Ebner]

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

[Gabriel Ebner]

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]

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

[Mario Carneiro]

At least put it after the words "no goals"

[Gabriel Ebner]

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

[Patrick Massot]

bug2.png

This also happen in conversion mode...

[Patrick Massot]

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

[Patrick Massot]

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

[Gabriel Ebner]

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]

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]

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

[Johan Commelin]

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

[Gabriel Ebner]

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]

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

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