issues
search
leanprover
/
vscode-lean4
Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
170
stars
49
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
doc: update manual
#550
mhuisi
closed
1 week ago
0
refactor: use `LeanEditorProvider` everywhere
#549
mhuisi
closed
1 week ago
0
moogle 2.0 + leandocsearch
#548
jesse-michael-han
opened
2 weeks ago
0
feat: sticky notifications for extension startup errors
#547
mhuisi
closed
1 week ago
0
feat: add subtle spinner while infoview is loading
#546
mhuisi
closed
3 weeks ago
0
chore: replace webview-ui-toolkit
#545
mhuisi
closed
3 weeks ago
0
feat: detachable infoview
#544
mhuisi
closed
3 weeks ago
0
feat: restart file button in 'fetch cache for focused file' command
#543
mhuisi
closed
1 month ago
0
feat: better progress ux
#542
mhuisi
closed
1 month ago
0
RFC: Math in hovers
#541
Vtec234
opened
1 month ago
1
doc: list default settings and how to override them in the manual
#540
mhuisi
closed
1 month ago
0
Extension makes unhelpful automatic whitespace edits
#539
Coda-Coda
closed
1 month ago
2
A small bug report: potential conflict with Harmonic Lean 4
#538
Rustastra
closed
1 month ago
1
fix: add another missing file to bundle
#537
mhuisi
closed
1 month ago
0
fix: bundle moogleview static folder
#536
mhuisi
closed
1 month ago
0
fix: widget persistence
#535
Vtec234
closed
1 month ago
1
feat: improve Markdown popup rendering
#534
Vtec234
closed
1 month ago
0
RFC: Mac installation clarification
#533
fpvandoorn
opened
1 month ago
0
feat: improve 'Download Project' UI
#532
mhuisi
closed
1 month ago
0
Documentation recourses broken
#531
fpvandoorn
closed
1 month ago
1
"Download project" flow is confusing
#530
TwoFX
closed
1 month ago
2
Welcome page doesn't open
#529
fpvandoorn
closed
1 week ago
4
Add Moogle 1.0 support to VSCode extension
#528
jesse-michael-han
closed
1 month ago
1
fix: leading bang is a word separator
#527
mhuisi
closed
2 months ago
0
chore: remove rial symbol
#525
mhuisi
closed
2 months ago
0
chore: update actions/upload-artifact
#524
kim-em
closed
2 months ago
0
feat(abbreviations.json): add double parens abbreviations
#523
Julian
closed
2 months ago
0
RFC: Remove character '﷼' from abbreviations
#522
adomasbaliuka
closed
2 months ago
0
chore: change extension display name
#521
mhuisi
closed
3 months ago
0
chore: use text variant of ✝︎
#520
joneugster
closed
2 months ago
0
chore: use emoji-variant for ❌️
#519
joneugster
closed
3 months ago
1
export index.production.min.js
#518
onriv
closed
1 month ago
0
InfoView not working Xubuntu 22.04
#517
solmersa
opened
3 months ago
1
Incorrect highlighting if deprecation message contains `]` character
#515
TwoFX
opened
3 months ago
1
fix: [lean4web] dispose webviewPanel in InfoProvider.dispose
#514
abentkamp
opened
4 months ago
0
TMP
#513
joneugster
closed
4 months ago
0
fix: initial commit not working on fresh Git install
#512
mhuisi
closed
4 months ago
0
fix: filter menu button collapsing goal state
#511
mhuisi
closed
3 months ago
2
Initial commit does not work in fresh install of Git
#510
mhuisi
closed
4 months ago
0
feat: fetch mathlib build cache for focused file command
#509
mhuisi
closed
4 months ago
0
feat: [lean4web] add option to change selectionMoveMove
#508
abentkamp
opened
4 months ago
0
feat: download project presets
#507
mhuisi
closed
4 months ago
0
offer curated suggestions for "Download project" (beyond the current Mathlib suggestion)
#506
kim-em
closed
4 months ago
0
Tactic state collapses when filters are opened
#505
Vtec234
closed
3 months ago
0
fix: [lean4web] replace require-style imports
#504
abentkamp
opened
4 months ago
0
doc: use image urls for everything
#503
mhuisi
closed
4 months ago
0
doc: attempt to fix broken marketplace links
#502
mhuisi
closed
4 months ago
0
doc: update old docs
#501
mhuisi
closed
4 months ago
0
fix: infoview performance
#500
mhuisi
closed
4 months ago
5
Pinned locations are tracked incorrectly
#499
Vtec234
closed
4 months ago
2
Next