Skip to content

Issues: ejgallego/coq-lsp

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.

Sign up for GitHub

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

127 Open 130 Closed
127 Open 130 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Incorrect implicit arguments of record/inductive on hover kind: bug Something isn't working
#876 opened Nov 19, 2024 by Alizter
Hover on proof name kind: bug Something isn't working
#875 opened Nov 19, 2024 by Alizter
Update credits kind: bug Something isn't working
#871 opened Nov 12, 2024 by ejgallego 0.2.3
[debug] [ui] Provide an easier way to output a protocol trace. kind: enhancement New feature or request
#868 opened Oct 23, 2024 by ejgallego 0.2.3
Missing of_yojson for FlecheDocument module kind: bug Something isn't working part: lsp server
#862 opened Oct 17, 2024 by blackbird1128 0.2.3
1
name conflict with the lsp package kind: bug Something isn't working part: lsp server
#861 opened Oct 17, 2024 by blackbird1128 0.2.3
1
[user interaction] Proof-general like mode. kind: bug Something isn't working kind: HCI design needs: test-case part: flèche
#860 opened Oct 17, 2024 by ejgallego 0.2.4
0.2.0 crashes frequently kind: bug Something isn't working part: upstream
#857 opened Oct 14, 2024 by dariusf 0.2.3
2
Goto definition doesn't work for record constructors kind: bug Something isn't working part: lsp server
#856 opened Oct 10, 2024 by Alizter
1
Syntax highlighting kind: bug Something isn't working part: client (VSCode)
#854 opened Oct 7, 2024 by Alizter
8 of 13 tasks
4
[web worker] Package manager kind: enhancement New feature or request part: web worker
#852 opened Oct 4, 2024 by ejgallego
[web worker] Add progress bar for worker download kind: enhancement New feature or request part: web worker
#851 opened Oct 4, 2024 by ejgallego
[web worker] Allow users to select different Coq versions kind: enhancement New feature or request part: web worker
#850 opened Oct 4, 2024 by ejgallego
Show Proof window kind: enhancement New feature or request
#836 opened Sep 27, 2024 by Alizter
2
JS Worker Meta Issue kind: meta
#833 opened Sep 27, 2024 by ejgallego
Clarify the difference between VsCoq 1 and VsCoq 2 here? kind: bug Something isn't working part: documentation
#817 opened Sep 2, 2024 by patrick-nicodemus 0.2.3
1
1
Document outline doesn't work with on-demand checking kind: bug Something isn't working
#816 opened Sep 1, 2024 by Alizter
1
"printer interrupted" in goal window kind: bug Something isn't working
#806 opened Jul 14, 2024 by Alizter
5
Heatmap disappears when refocusing tab kind: bug Something isn't working part: client (VSCode)
#805 opened Jul 9, 2024 by Alizter
Slow goal printing in Coq-HoTT theories/Spaces/No/Core.v kind: bug Something isn't working kind: performance part: pp printer
#798 opened Jun 27, 2024 by Alizter
2
Universe information kind: enhancement New feature or request
#797 opened Jun 27, 2024 by Alizter 0.3.0
3
Bug minimizer kind: enhancement New feature or request
#691 opened May 1, 2024 by Alizter
12
Accumulated performance stats on selection hover
#690 opened May 1, 2024 by Alizter
6
Restarting server resets position of goal window kind: bug Something isn't working part: goals and info panel
#678 opened Apr 15, 2024 by Alizter 0.2.3
1
2
[bug] Properly handle proof mode kind: bug Something isn't working kind: upstream kind: upstream-bug part: flèche part: upstream
#656 opened Mar 20, 2024 by ejgallego 0.3.0
ProTip! Find all open issues with in progress development work with linked:pr.