vscode-lean4

vscode-lean4 copied to clipboard

I would like a user interaction in VSCode that * starts a `lake build` * as errors occur, opens the relevant files in VSCode, but without changing the currently focussed...

kim-em

Feature request: Support Live Share

5

### Proposal [VS Code Live Share](https://code.visualstudio.com/learn/collaboration/live-share) is a feature that allows multiple clients to edit the same file. When using Live Share with Lean, standard LSP functionality (autocomplete, hovers, ..)...

Vtec234

### Proposal It would be nice to have an action to de-select everything in the info view, hopefully with an assigned default key-binding. Currently this is not crucial. But several...

PatrickMassot

Autocomplete not working, vscode falls back to the default.

2

### Description I would have expected lean4 vscode extension to let me autocomplete existing theorem names and imports, but this is not the case - vscode falls back to its...

iczelia

### Description Watching [this video at this timecode](https://www.youtube.com/watch?v=FPiykrdPe6U&t=1154s) on my phone, I couldn't read the infoview. This makes me think that the selected text colors may not be perfectly following...

david-christiansen

### Description I need to program stuff with mingw, so I open vscode on mingw, once 1 window has been opened in mingw, all other windows will inherit this context,...

Kreijstal

Suggest adding a `.vscode/settings.json`

2

Many Lean projects have a `.vscode/settings.json`: ``` { "editor.insertSpaces": true, "editor.tabSize": 2, "editor.rulers" : [100], "files.encoding": "utf8", "files.eol": "\n", "files.insertFinalNewline": true, "files.trimFinalNewlines": true, "files.trimTrailingWhitespace": true, } ``` These do some...

kim-em

Infoview does not load (ARM64)

6

Hello, I just installed the VS code lean4 extension, but the "Lean Infoview" is blank. I am using an ARM64 build of Windows 11, but I have the x64 build...

PDeets

This occured [on the Lean Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Trouble.20installing.20lean4). There's a good chance that this is not an extension error. It's worth investigating whether we can somehow trigger this error on Windows.

mhuisi

Merge vscode-lean4-code-actions?

1

Hi @Vtec234 @gebner ! I've published a new [VSCode extension for code actions](https://marketplace.visualstudio.com/items?itemName=denis-gorbachev.lean4-code-actions&ssr=false). Mario suggested merging this extension into `vscode-lean4` in [the Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VSCode.20extension.20for.20Lean.20code.20actions). Pros: * Users won't need to...

DenisGorbachev