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
Initial version check does not use Something isn't working
lean
executable from lake
bug
#440
opened May 2, 2024 by
llllvvuu
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
RFC: GUI button to download cache for a specific file
RFC
Request for comments
#416
opened Mar 20, 2024 by
YaelDillies
Support Request for comments
${workspaceFolder}
and similar variables in lean4.toolchainPath
RFC
#400
opened Feb 23, 2024 by
eric-wieser
feature request: "go to next problem" should work on errors in imported files
#396
opened Feb 15, 2024 by
semorrison
feature request: in VSCode, open downstream files with errors
RFC
Request for comments
#397
opened Feb 15, 2024 by
semorrison
Extension does not respect elan override when first started
bug
Something isn't working
#388
opened Jan 16, 2024 by
tydeu
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
Display a warning if "lean4.toolchainPath" is set?
RFC
Request for comments
#326
opened Sep 20, 2023 by
semorrison
Suggest adding a Request for comments
.vscode/settings.json
low priority
RFC
#325
opened Sep 17, 2023 by
semorrison
Waiting for Lean server to start confusing message
enhancement
New feature or request
#323
opened Sep 7, 2023 by
PatrickMassot
'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!
Mix and match filters to narrow down what you’re looking for.