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.

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

Jump to bottom

[ fix ] show warnings and persist for session #225

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

[ fix ] show warnings and persist for session #225

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
50ac83a
[ fix ] show warnings and persist for session
dunhamsteve Oct 12, 2024
b08ab3f
Reload ttf/ttm if file compiles successfully
dunhamsteve Oct 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion src/Server/Configuration.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module Server.Configuration
import public Libraries.Data.PosMap
import public Libraries.Data.NameMap

import Core.Core
import Core.FC
import Core.Name
import Data.SortedMap
Expand Down Expand Up @@ -69,6 +70,8 @@ record LSPConfiguration where
completionCache : SortedMap DocumentURI (SortedMap Completion.Info.NameCategory (List Entry))
||| Virtual file content caches
virtualDocuments : SortedMap DocumentURI (Int, String) -- Version content
||| Warnings cache
warningDocuments : SortedMap DocumentURI (List Warning)
||| Insert only function name for completions
briefCompletions : Bool

Expand All @@ -94,5 +97,6 @@ defaultConfig =
, nextRequestId = 0
, completionCache = empty
, virtualDocuments = empty
, briefCompletions = False
, warningDocuments = empty
, briefCompletions = False
}
41 changes: 26 additions & 15 deletions src/Server/ProcessMessage.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,34 +228,45 @@ loadURI conf uri version = do
update LSPConf ({ virtualDocuments $= insert uri (fromMaybe 0 version, res ++ "\n") })
-- A hack to solve some interesting edge-cases around missing newlines ^^^^^^^
setSource res
errs <- catch
(buildDeps fname)
errs <- catch (do mods <- getBuildMods EmptyFC [] fname
buildMods EmptyFC 1 (length mods) mods)
Comment on lines -231 to +232
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 •
edited
Loading

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.

(\err => do
logE Server "Caught error which shouldn't be leaked while loading file: \{show err}"
pure [err])
-- FIXME: the compiler always dumps the errors on stdout, requires
-- a compiler change.
-- NOTE on catch: It seems the compiler sometimes throws errors instead
-- of accumulating them in the buildDeps.
unless (null errs) $ do
update LSPConf ({ errorFiles $= insert uri })
-- ModTree 397--308 loads data into context from ttf/ttm if no errors
-- In case of error, we reprocess fname to populate metadata and syntax
logI Channel "Rebuild \{fname} due to errors"
modIdent <- ctxtPathToNS fname
let msgPrefix : Doc IdrisAnn = pretty0 ""
let buildMsg : Doc IdrisAnn = pretty0 modIdent
clearCtxt; addPrimitives
put MD (initMetadata (PhysicalIdrSrc modIdent))
ignore $ ProcessIdr.process msgPrefix buildMsg fname modIdent

if (null errs) then do
-- this was previously in buildDeps, broken out so we have access
-- to warnings
clearCtxt; addPrimitives
modIdent <- ctxtPathToNS fname
put MD (initMetadata (PhysicalIdrSrc modIdent))
mainttc <- getTTCFileName fname "ttc"
readAsMain mainttc
-- Load the associated metadata for interactive editing
mainttm <- getTTCFileName fname "ttm"
readFromTTM mainttm
else do
update LSPConf ({ errorFiles $= insert uri })
modIdent <- ctxtPathToNS fname
let msgPrefix : Doc IdrisAnn = pretty0 ""
let buildMsg : Doc IdrisAnn = pretty0 modIdent
clearCtxt; addPrimitives
put MD (initMetadata (PhysicalIdrSrc modIdent))
ignore $ ProcessIdr.process msgPrefix buildMsg fname modIdent
resetProofState
let caps = (publishDiagnostics <=< textDocument) . capabilities $ conf
update LSPConf ({ quickfixes := [], cachedActions := empty, cachedHovers := empty })
traverse_ (findQuickfix caps uri) errs
defs <- get Ctxt
session <- getSession
let warnings = if session.warningsAsErrors then [] else reverse (warnings defs)
-- use cached warnings if file hasn't changed
warnings <- gets LSPConf (fromMaybe warnings . lookup uri . warningDocuments)
update LSPConf { warningDocuments $= insert uri warnings }

sendDiagnostics caps uri version warnings errs
defs <- get Ctxt
put Ctxt ({ options->dirs->extra_dirs := extraDirs } defs)
Expand Down Expand Up @@ -587,7 +598,7 @@ handleNotification TextDocumentDidSave params = whenActiveNotification $ \conf =

handleNotification TextDocumentDidChange params = whenActiveNotification $ \conf => do
logI Channel "Received didChange notification for \{show params.textDocument.uri}"
update LSPConf ({ dirtyFiles $= insert params.textDocument.uri})
update LSPConf ({ dirtyFiles $= insert params.textDocument.uri, warningDocuments $= delete params.textDocument.uri })
whenJust !(gets LSPConf (lookup params.textDocument.uri . virtualDocuments)) $ \(v,content) => do
case changeVirtualContent params.contentChanges content of
Left e => do
Expand Down
Loading