Zulip Chat Archive

Stream: general

Topic: VSCode Extension

Kenny Lau (Dec 04 2020 at 12:24):

Can we make the indentation 2 spaces globally?

Gabriel Ebner (Dec 04 2020 at 12:52):

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

Kenny Lau (Dec 04 2020 at 13:22):

Can we make it automatically come with the Lean extension?

Mario Carneiro (Dec 04 2020 at 13:24):

it should be in mathlib's vscode settings

Mario Carneiro (Dec 04 2020 at 13:24):

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

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"

Eric Wieser (Dec 04 2020 at 13:36):

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

Eric Wieser (Dec 04 2020 at 13:36):

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

Mario Carneiro (Dec 04 2020 at 13:43):

well lots of people use vscode for more than just lean

Reid Barton (Dec 04 2020 at 13:43):

oh it's not per-mode or whatever?

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

Julian Berman (Dec 04 2020 at 13:44):

maybe it uses editorconfig

Julian Berman (Dec 04 2020 at 13:45):

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

Jason Rute (Dec 04 2020 at 13:46):

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

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.

Julian Berman (Dec 04 2020 at 13:48):

@Jason Rute that's on the user side

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

Julian Berman (Dec 04 2020 at 13:50):

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

Eric Wieser (Dec 04 2020 at 14:11):

I think we already do it in the extension

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

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?

Eric Wieser (Dec 04 2020 at 14:17):

Opened leanprover/vscode-lean#236, not tested

Julian Berman (Dec 04 2020 at 14:18):

haha you beat me

Julian Berman (Dec 04 2020 at 14:18):

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

Julian Berman (Dec 04 2020 at 14:18):

also not tested

Julian Berman (Dec 04 2020 at 14:18):

yeah looks same

Eric Wieser (Dec 04 2020 at 14:18):

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

Gabriel Ebner (Dec 04 2020 at 14:37):

Thanks! I haven't tested it either.

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.

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?

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!

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

Oliver Nash (Jan 03 2021 at 10:54):

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

Kevin Buzzard (Jan 03 2021 at 10:55):

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

Oliver Nash (Jan 03 2021 at 10:55):

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

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.

Yakov Pechersky (Jan 03 2021 at 10:56):

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

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.

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.

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

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.

Patrick Lutz (Jan 03 2021 at 17:42):

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

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!

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 :-)

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.

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: Dec 20 2023 at 11:08 UTC