Zulip Chat Archive

Stream: general

Topic: vscode snippets


view this post on Zulip Johan Commelin (Feb 12 2019 at 13:11):

@Patrick Massot and others: is there some place where we gather useful VScode snippets?

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:11):

No yet afaik

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:11):

I couldn't find them online. Only some examples here on Zulip.

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:11):

@Patrick Massot Would you mind putting yours in a gist, for starters?

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:12):

I think having them inside the extension is controversial, but we could maintain a collection at mathlib

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:12):

Sure, or in the extension repo, in a file that isn't shipped by default.

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:13):

There could be a contrib folder in that repo.

view this post on Zulip Johan Commelin (Feb 12 2019 at 13:13):

But let's start with gists (-;

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:13):

https://gist.github.com/PatrickMassot/27417fad299a48e690ab5609a99baa67

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:17):

Speaking of the VScode extension, what happened to the Lean messages update icon?

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:17):

@Gabriel Ebner

view this post on Zulip Gabriel Ebner (Feb 12 2019 at 13:19):

The Updating ⏸ icon in the top right? Is it broken?

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:20):

update.png

view this post on Zulip Gabriel Ebner (Feb 12 2019 at 13:23):

vscode-updating.png :shrug:

view this post on Zulip Gabriel Ebner (Feb 12 2019 at 13:23):

Windows?

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:23):

Are you talking to me in that last line? :angry_cat:

view this post on Zulip Gabriel Ebner (Feb 12 2019 at 13:23):

Yes.

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:24):

Last windows I used was Windows 98. I'm not even sure you were born at that time

view this post on Zulip Gabriel Ebner (Feb 12 2019 at 13:26):

You had a few machines for students with windows (I think), that's why I asked. But now I'm even more at a loss..

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:27):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VScode.20extension/near/157785947

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:27):

Bryan also had this issue

view this post on Zulip Gabriel Ebner (Feb 12 2019 at 13:28):

Oh, I'm still on 1.30 here. Thanks for the pointer!

view this post on Zulip Patrick Massot (Feb 12 2019 at 13:28):

If it's a VScode bug then at least my students won't see it in our computer labs with no VScode auto-update

view this post on Zulip Gabriel Ebner (Feb 12 2019 at 13:45):

The bug is already fixed in vscode master: https://github.com/Microsoft/vscode/issues/68033 We'll just have to wait for 1.31.1

view this post on Zulip Bryan Gin-ge Chen (Feb 13 2019 at 05:56):

1.31.1 just arrived and it looks like this is fixed!

view this post on Zulip Johan Commelin (Feb 13 2019 at 07:28):

Coming back to the original topic of this thread: I invite everyone who has useful VScode snippets to put them in a gist and post the url here.

view this post on Zulip Bryan Gin-ge Chen (Oct 26 2019 at 12:00):

Bumping this old thread to share something to make working with the "Infer type" hole command slightly easier. It's a snippet triggered by keybind rather than by auto-suggest. This will let you select a Lean expression and then hit "ctrl+'" to surround it with {! !}. You can then display the hole command menu by clicking on the light bulb icon that pops up or hitting your "Quick fix" keybind (cmd+. on mac).

To set this up, paste the following as an element of the array in your keybindings.json (you can get to it by hitting ctrl+shift+p (or cmd+shift+p on a mac) and typing "key j" and selecting "Open keyboard shortcuts (JSON)"):

    {
        "key": "ctrl+'",
        "command": "editor.action.insertSnippet",
        "when": "editorLangId == 'lean'",
        "args": {
            "snippet": "{!${TM_SELECTED_TEXT}!}"
        },
    }

view this post on Zulip Johan Commelin (Oct 26 2019 at 15:19):

@Bryan Gin-ge Chen Thanks, nice snippet!

view this post on Zulip Scott Morrison (Oct 27 2019 at 06:45):

Would this be unreasonable to put in .vscode/settings.json in the mathlib repository?

view this post on Zulip Miguel Raz Guzmán Macedo (Nov 12 2019 at 19:27):

beautiful snippets!
These reaaaally help beginners!


Last updated: May 11 2021 at 23:11 UTC