-
Notifications
You must be signed in to change notification settings - Fork 52
Issues: leanprover/vscode-lean4
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
installation fails if a startup script in the terminal asks for input
bug
Something isn't working
#558
opened Dec 17, 2024 by
bryangingechen
Feature Request: File icon for '.lean' files
enhancement
New feature or request
#552
opened Dec 4, 2024 by
shilangyu
Incorrect highlighting if deprecation message contains Something isn't working
]
character
bug
#515
opened Aug 7, 2024 by
TwoFX
3 tasks done
Backslash for unicode breaks down often in recent version of lean4
bug
Something isn't working
#489
opened Jun 29, 2024 by
Qiu233
Triggering an eager replacement with a new abbreviation does not track new abbreviation in LoogleView
bug
Something isn't working
#479
opened Jun 21, 2024 by
mhuisi
Right-clicking almost anywhere in the editor makes "Lean Infoview" focused
bug
Something isn't working
#438
opened Apr 30, 2024 by
ge9
Stale dependency diagnostic does not show up under 'Messages' after opening VS Code
bug
Something isn't working
#424
opened Mar 27, 2024 by
mhuisi
feature request: "go to next problem" should work on errors in imported files
#396
opened Feb 15, 2024 by
kim-em
feature request: in VSCode, open downstream files with errors
RFC
Request for comments
#397
opened Feb 15, 2024 by
kim-em
HTML-ish content in docstrings causes incorrect highlighting after them
bug
Something isn't working
#369
opened Dec 5, 2023 by
david-christiansen
Autocomplete not working, vscode falls back to the default.
bug
Something isn't working
#357
opened Nov 13, 2023 by
kspalaiologos
Illegible colors in infoview on selection
bug
Something isn't working
#353
opened Nov 8, 2023 by
david-christiansen
Extension doesn't play nice with msys2
bug
Something isn't working
#346
opened Oct 30, 2023 by
Kreijstal
Suggest adding a Request for comments
.vscode/settings.json
low priority
RFC
#325
opened Sep 17, 2023 by
kim-em
'Error updating' infoview error in fresh install on Windows 10
bug
Something isn't working
hard to reproduce
#322
opened Sep 7, 2023 by
mhuisi
Having both
\centerdot
(aka \.
) and \cdot
can be unnecessarily confusing.
#308
opened Jul 1, 2023 by
eddyb
Previous Next
ProTip!
What’s not been updated in a month: updated:<2024-11-25.