Skip to content
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

[ fix ] show warnings and persist for session #225

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

dunhamsteve
Copy link
Contributor

Warnings don't show up in the LSP. This is due to a couple of reasons - Idris doesn't have warnings when reading from .ttc files and buildDeps rereads the main module from .ttc after building everything, effectively losing the warning information.

I've made two changes here. I replaced the call to buildDeps with the first couple of lines from buildDeps. The comments in buildDeps say that it is re-reading in a clean context, but it looks like buildMods clears the context before each module, so I think we're ok there.

Second, I added a cache for the warnings for each file. I'm clearing it for a given file when the LSP is notified that the file has changed. This lets us retain the warnings if the file hasn't changed. They're not persisted when the LSP is restarted.

So, we now have warnings and they persist when switching between files (in vscode), but not when restarting everything. (They'll show up again when a file is changed.) This was a compromise to make the fix less invasive (we're not changing Idris itself), but after an evening working with these changes in place I've found them useful. This change can be removed if we ever add warnings to ttc / ttm files.

Copy link
Member

@mattpolzin mattpolzin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if this is going to quite do the trick. As noted in my comment, things stopped working for me with these changes. Undoing the change that removes builDeps gets the server working again, but there's no change to the old behavior: in Neovim, I see all warnings for the current file as long as there is also an error somewhere in the file but as soon as all errors are fixed, all warnings disappear.

Comment on lines -231 to +232
errs <- catch
(buildDeps fname)
errs <- catch (do mods <- getBuildMods EmptyFC [] fname
buildMods EmptyFC 1 (length mods) mods)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Best I can tell, this change breaks the LSP server (as a Neovim user, at least). No useful errors coming out of it from a cursor look over the LSP logs, just a lack of the LSP reporting anything actionable to the editor so you never get highlighting (or, naturally, any other LSP features).

I double checked by undoing only this line's change and saw the server work (again, this is in Neovim).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's odd. Maybe vim is interacting with the LSP differently than vscode. vscode is working for me.

I'm not able to reproduce this locally in nvim, but I realized I've got edwin's idris2-vim, which I don't think is LSP based. I'll see if I can get nvim set up with LSP and sort out the issue. Marking this PR as draft for now. Thanks for taking a look.

(I'm also not using LSP with emacs, but I don't know if anybody does for Idris.)

Copy link
Contributor Author

@dunhamsteve dunhamsteve Oct 14, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok, I see something now in vscode. The testing that I did last night was with a file that had a coverage error in addition to warnings. I did see the warnings, the warnings went away if I fixed them, and the editor functions work, but not if I try it with an error-free file, the LSP functionality is not there. Maybe the block that reloads the file in case of error is fixing something. I'll investigate.

@dunhamsteve dunhamsteve marked this pull request as draft October 14, 2024 02:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants