Zulip Chat Archive

Stream: general

Topic: VSCode Extension


view this post on Zulip Kenny Lau (Dec 04 2020 at 12:24):

Can we make the indentation 2 spaces globally?

view this post on Zulip Gabriel Ebner (Dec 04 2020 at 12:52):

Yes, it is possible to do this in the editor.tabSize setting.

view this post on Zulip Kenny Lau (Dec 04 2020 at 13:22):

Can we make it automatically come with the Lean extension?

view this post on Zulip Mario Carneiro (Dec 04 2020 at 13:24):

it should be in mathlib's vscode settings

view this post on Zulip Mario Carneiro (Dec 04 2020 at 13:24):

setting the user's default tab size just for installing the extension seems rude

view this post on Zulip Kenny Lau (Dec 04 2020 at 13:32):

because Kevin said that "whenever I start a new project I always have to change spaces from 4 to 2"

view this post on Zulip Eric Wieser (Dec 04 2020 at 13:36):

can we set the default tab size for just all lean code?

view this post on Zulip Eric Wieser (Dec 04 2020 at 13:36):

I feel like pushing mathlib convention on all lean users isn't that rude

view this post on Zulip Mario Carneiro (Dec 04 2020 at 13:43):

well lots of people use vscode for more than just lean

view this post on Zulip Reid Barton (Dec 04 2020 at 13:43):

oh it's not per-mode or whatever?

view this post on Zulip Julian Berman (Dec 04 2020 at 13:43):

there has to be a per-filetype indent setting in vscode, there is in any other editor

view this post on Zulip Julian Berman (Dec 04 2020 at 13:44):

maybe it uses editorconfig

view this post on Zulip Julian Berman (Dec 04 2020 at 13:45):

that's what vscode-python looks like it might use

view this post on Zulip Jason Rute (Dec 04 2020 at 13:46):

https://stackoverflow.com/questions/34247939/how-to-set-per-filetype-tab-size

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 13:47):

Can this be done via the VS Code extension? I am always terrified to edit a json file.

view this post on Zulip Julian Berman (Dec 04 2020 at 13:48):

@Jason Rute that's on the user side

view this post on Zulip Julian Berman (Dec 04 2020 at 13:48):

but yeah there's got to be a way to do so in the extension's side

view this post on Zulip Julian Berman (Dec 04 2020 at 13:50):

(which I'm not finding... hrm, but it has to be here.)

view this post on Zulip Eric Wieser (Dec 04 2020 at 14:11):

I think we already do it in the extension

view this post on Zulip Julian Berman (Dec 04 2020 at 14:11):

ok phew was driving me nuts -- I think you were right it's the same setting, but it looks like you put it in the contributes section in vscode-lean's package.json: https://stackoverflow.com/questions/44790042/in-a-vs-code-extension-is-there-a-way-to-set-the-configuration-options-for-the

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 14:13):

OK I just tested by making a new Lean project and opening it in VS Code and I am 4 spaces. Have I got some dodgy setting overriding the extension's setting?

view this post on Zulip Eric Wieser (Dec 04 2020 at 14:17):

Opened leanprover/vscode-lean#236, not tested

view this post on Zulip Julian Berman (Dec 04 2020 at 14:18):

haha you beat me

view this post on Zulip Julian Berman (Dec 04 2020 at 14:18):

https://github.com/Julian/vscode-lean/commit/e02c6437a30e58af36619d9f313720ca0f312587

view this post on Zulip Julian Berman (Dec 04 2020 at 14:18):

also not tested

view this post on Zulip Julian Berman (Dec 04 2020 at 14:18):

yeah looks same

view this post on Zulip Eric Wieser (Dec 04 2020 at 14:18):

Related: https://github.com/leanprover-community/mathlib/issues/3186#issuecomment-660972623

view this post on Zulip Gabriel Ebner (Dec 04 2020 at 14:37):

Thanks! I haven't tested it either.

view this post on Zulip Yakov Pechersky (Dec 04 2020 at 14:58):

A relevant VSCode option is that it can infer the tab-size from the file, no matter the file extension. And the default, file-insensitive tab-ext size is 4. So once you do 4, it infers 4 for the rest of the file.

view this post on Zulip Oliver Nash (Jan 03 2021 at 10:50):

Our VSCode extension supports the Unicode "square with quill" brackets and but it does not play nicely with the logic to autogenerate a right bracket when the user has just input a left bracket. This came up in @Patrick Lutz 's PR
here

The shortcuts are listed here. At the moment if the user enters \liel then is inserted but no is autoinserted. However if the user enters the alternative \[- then is inserted but so is a non-matching regular square bracket ].

Is there any chance this would be easy to fix?

view this post on Zulip Gabriel Ebner (Jan 03 2021 at 10:51):

Here's the list of brackets: https://github.com/leanprover/vscode-lean/blob/master/language-configuration.json
PRs welcome!

view this post on Zulip Gabriel Ebner (Jan 03 2021 at 10:52):

Oh, I think it's already there. Here's a second list of brackets (with special support for \liel, etc.):
https://github.com/leanprover/vscode-lean/blob/master/src/input.ts#L94-L100

view this post on Zulip Oliver Nash (Jan 03 2021 at 10:54):

Thanks. So it looks like I should add something like [this.leader + 'f[--]']: '⁅⁆', to hackyReplacements here?

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 10:55):

Wooah! Was I the only one who didn't know \<> produces a matching \< \> pair?

view this post on Zulip Oliver Nash (Jan 03 2021 at 10:55):

I can confirm there was at least one other such person!

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 10:55):

Without even having to press tab or space or anything -- it just makes them both and sticks the cursor in the middle.

view this post on Zulip Yakov Pechersky (Jan 03 2021 at 10:56):

And \f<> does the same for french assumption quotes.

view this post on Zulip Oliver Nash (Jan 03 2021 at 11:06):

I have just generated a PR. I have no idea how to test locally but maybe that's OK for something so small.

view this post on Zulip Oliver Nash (Jan 03 2021 at 11:08):

Oh I just found this old PR so I'm fairly confident what I've done should be OK.

view this post on Zulip Gabriel Ebner (Jan 03 2021 at 11:21):

Oliver Nash said:

I have no idea how to test locally but maybe that's OK for something so small.

You can follow the instructions here: https://github.com/leanprover/vscode-lean#development
In short: run npm i, open vscode-lean in vscode, and press F5

view this post on Zulip Oliver Nash (Jan 03 2021 at 12:11):

Oh, thanks. I should have RTFM. I have now tested this locally and can confirm it works.

view this post on Zulip Patrick Lutz (Jan 03 2021 at 17:42):

@Oliver Nash This is very nice, thanks for doing it

view this post on Zulip Oliver Nash (Jan 03 2021 at 18:40):

@Patrick Lutz Delighted to help. It was a good exercise for me to learn a bit about contributing to the extension. I’m looking forward to your PR landing btw. Really nice work!

view this post on Zulip Oliver Nash (Jan 04 2021 at 09:33):

@Gabriel Ebner Thank you very much for Release 0.6.19. I was not expecting an entire release just for my ⁅⁆ fix so this is very welcome surprise :-)

view this post on Zulip Henning Dieterichs (Jan 04 2021 at 09:52):

Btw. I submitted a PR that touches this logic and generalizes it! (see here: https://github.com/leanprover/vscode-lean/pull/240) There is still a minor bug, I will fix it soon.

view this post on Zulip Henning Dieterichs (Jan 04 2021 at 09:53):

Without even having to press tab or space or anything -- it just makes them both and sticks the cursor in the middle.

The PR also implements a new feature that longest abbreviations are replaced automatically with the last character of the abbreviation:
103356122-5a9efb00-4ab0-11eb-8d29-3d84cb146787.gif


Last updated: May 08 2021 at 10:12 UTC