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.
Warnings don't show up in the LSP. This is due to a couple of reasons - Idris doesn't have warnings when reading from
.ttcfiles andbuildDepsrereads the main module from .ttc after building everything, effectively losing the warning information.I've made two changes here. I replaced the call to
buildDepswith the first couple of lines frombuildDeps. The comments inbuildDepssay that it is re-reading in a clean context, but it looks likebuildModsclears 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.