Zulip Chat Archive

Stream: general

Topic: vscode-lean 0.11.0


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 21 2018 at 20:28):

can you also type ⟦⟧ using \[[?

view this post on Zulip Chris Hughes (Apr 21 2018 at 20:37):

No, it seems.

view this post on Zulip Patrick Massot (Apr 21 2018 at 20:48):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 21 2018 at 20:55):

I didn't see a reload button

view this post on Zulip Patrick Massot (Apr 21 2018 at 20:55):

I'll search more

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Apr 21 2018 at 20:56):

I'm updated

view this post on Zulip Gabriel Ebner (Apr 22 2018 at 06:49):

can you also type ⟦⟧ using \[[?

You can, as of a minute ago.

view this post on Zulip Patrick Massot (Apr 22 2018 at 09:08):

Thank you!

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Apr 23 2018 at 14:31):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Patrick Massot (May 08 2018 at 15:59):

colored_tactic_state.png

view this post on Zulip Patrick Massot (May 08 2018 at 15:59):

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

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

view this post on Zulip Patrick Massot (May 08 2018 at 16:01):

Which is called in InfoProvider.renderGoal

view this post on Zulip Patrick Massot (May 08 2018 at 16:01):

@Gabriel Ebner What do you think about that?

view this post on Zulip Mario Carneiro (May 08 2018 at 16:01):

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

view this post on Zulip Patrick Massot (May 08 2018 at 16:02):

Indeed it couldn't be less pure

view this post on Zulip Patrick Massot (May 08 2018 at 16:02):

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

view this post on Zulip Mario Carneiro (May 08 2018 at 16:02):

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

view this post on Zulip Patrick Massot (May 08 2018 at 16:03):

But Gabriel told me the syntax highlighter is not available here

view this post on Zulip Patrick Massot (May 08 2018 at 16:03):

Yes, a classification function would help

view this post on Zulip Patrick Massot (May 08 2018 at 16:03):

At least make things more modular

view this post on Zulip Patrick Massot (May 08 2018 at 16:04):

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

view this post on Zulip Gabriel Ebner (May 08 2018 at 16:04):

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

view this post on Zulip Mario Carneiro (May 08 2018 at 16:04):

don't forget the case line of tactic state

view this post on Zulip Patrick Massot (May 08 2018 at 16:05):

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

view this post on Zulip Mario Carneiro (May 08 2018 at 16:05):

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

view this post on Zulip Patrick Massot (May 08 2018 at 16:06):

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

view this post on Zulip Gabriel Ebner (May 08 2018 at 16:06):

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

view this post on Zulip Gabriel Ebner (May 08 2018 at 16:06):

The CSS is in infoview.css

view this post on Zulip Patrick Massot (May 08 2018 at 16:07):

    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>`;
    }

view this post on Zulip Patrick Massot (May 08 2018 at 16:09):

Reading infoview.css is very interesting

view this post on Zulip Patrick Massot (May 08 2018 at 16:09):

Indeed it should be very easy to use

view this post on Zulip Gabriel Ebner (May 08 2018 at 16:33):

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

view this post on Zulip Patrick Massot (May 08 2018 at 16:35):

Wow, you're fast

view this post on Zulip Patrick Massot (May 08 2018 at 16:35):

I was working on it

view this post on Zulip Patrick Massot (May 08 2018 at 16:35):

But not fast enough :wink:

view this post on Zulip Patrick Massot (May 08 2018 at 16:36):

I didn't know about the m flag in replace

view this post on Zulip Patrick Massot (May 08 2018 at 16:37):

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

view this post on Zulip Patrick Massot (May 08 2018 at 16:38):

There can be space before the colon

view this post on Zulip Patrick Massot (May 08 2018 at 16:38):

when several variables share a common type

view this post on Zulip Patrick Massot (May 08 2018 at 16:39):

bug.png

view this post on Zulip Patrick Massot (May 08 2018 at 16:39):

But I do like this orange

view this post on Zulip Patrick Massot (May 08 2018 at 16:41):

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

view this post on Zulip Patrick Massot (May 08 2018 at 16:41):

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

view this post on Zulip Gabriel Ebner (May 08 2018 at 16:47):

Should be fixed now.

view this post on Zulip Patrick Massot (May 08 2018 at 16:52):

Nice!

view this post on Zulip Patrick Massot (May 08 2018 at 16:54):

oh oh...

view this post on Zulip Patrick Massot (May 08 2018 at 16:54):

New bug

view this post on Zulip Patrick Massot (May 08 2018 at 16:54):

I also had that one at some point

view this post on Zulip Patrick Massot (May 08 2018 at 16:55):

bug2.png

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (May 08 2018 at 16:56):

It's spreading!

view this post on Zulip Sebastian Ullrich (May 08 2018 at 16:57):

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

view this post on Zulip Sebastian Ullrich (May 08 2018 at 16:57):

:)

view this post on Zulip 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, '🎉 ');
}

view this post on Zulip Patrick Massot (May 08 2018 at 16:58):

I should really try Lean in spacemacs at some point

view this post on Zulip Patrick Massot (May 08 2018 at 16:59):

I don't why I'm affraid

view this post on Zulip Sebastian Ullrich (May 08 2018 at 16:59):

I should really write a Lean spacemacs layer at some point

view this post on Zulip Patrick Massot (May 08 2018 at 17:00):

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

view this post on Zulip Patrick Massot (May 08 2018 at 17:00):

Like, we wouldn't have to regex the output

view this post on Zulip Patrick Massot (May 08 2018 at 17:01):

It could be useful also to build more powerful IDEs

view this post on Zulip Patrick Massot (May 08 2018 at 17:02):

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

view this post on Zulip Sebastian Ullrich (May 08 2018 at 17:04):

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

view this post on Zulip Patrick Massot (May 08 2018 at 17:08):

Ok, I see you already discussed this quite a bit

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 08 2018 at 19:42):

Great

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 09 2018 at 06:57):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (May 09 2018 at 07:29):

Have a look at my latest preprint for instance

view this post on Zulip Patrick Massot (May 09 2018 at 07:29):

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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (May 09 2018 at 07:31):

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

view this post on Zulip Patrick Massot (May 09 2018 at 07:31):

I forgot I kept that experiment in the regex I posted

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 09 2018 at 07:48):

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

view this post on Zulip Mario Carneiro (May 09 2018 at 07:48):

At least put it after the words "no goals"

view this post on Zulip Gabriel Ebner (May 09 2018 at 07:50):

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

view this post on Zulip Patrick Massot (May 09 2018 at 15:54):

bug2.png

This also happen in conversion mode...

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 23 2018 at 19:35):

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

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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).

view this post on Zulip Johan Commelin (May 25 2018 at 10:00):

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

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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