From 15334f69d7f70ce27fd61212c1ac91a4646cb653 Mon Sep 17 00:00:00 2001 From: russoul Date: Wed, 27 Nov 2024 16:52:30 +0400 Subject: [PATCH 01/10] Support multi-ipkg setup --- src/Server/Configuration.idr | 5 +- src/Server/Main.idr | 29 ++++++---- src/Server/ProcessMessage.idr | 106 ++++++++++++++++++++++++---------- 3 files changed, 96 insertions(+), 44 deletions(-) diff --git a/src/Server/Configuration.idr b/src/Server/Configuration.idr index a295f1a..f6d1e60 100644 --- a/src/Server/Configuration.idr +++ b/src/Server/Configuration.idr @@ -71,6 +71,8 @@ record LSPConfiguration where virtualDocuments : SortedMap DocumentURI (Int, String) -- Version content ||| Insert only function name for completions briefCompletions : Bool + ||| Maybe specified .ipkg file + ipkgFile : Maybe String ||| Server default configuration. Uses standard input and standard output for input/output. export @@ -94,5 +96,6 @@ defaultConfig = , nextRequestId = 0 , completionCache = empty , virtualDocuments = empty - , briefCompletions = False + , briefCompletions = False + , ipkgFile = Nothing } diff --git a/src/Server/Main.idr b/src/Server/Main.idr index c4979f2..3caece8 100644 --- a/src/Server/Main.idr +++ b/src/Server/Main.idr @@ -71,12 +71,12 @@ parseHeaderPart h = do Nothing => pure $ Right Nothing handleMessage : Ref LSPConf LSPConfiguration - => Ref Ctxt Defs - => Ref UST UState - => Ref Syn SyntaxInfo - => Ref MD Metadata - => Ref ROpts REPLOpts - => Core () + => Ref Ctxt Defs + => Ref UST UState + => Ref Syn SyntaxInfo + => Ref MD Metadata + => Ref ROpts REPLOpts + => Core () handleMessage = do inputHandle <- gets LSPConf inputHandle Right (Just l) <- parseHeaderPart inputHandle @@ -150,13 +150,21 @@ runServer : Ref LSPConf LSPConfiguration => Core () runServer = handleMessage >> runServer -startServer : IO () -startServer = +processCommandLineArgs : Ref LSPConf LSPConfiguration => List String -> Core () +processCommandLineArgs [] = pure () +processCommandLineArgs [ipkgFile] = do + update LSPConf {ipkgFile := Just ipkgFile} + logI Server "Set .ipkg file to \{ipkgFile}" +processCommandLineArgs _ = throw (InternalError "Unexpected number of arguments") + +startServer : List String -> IO () +startServer extraCommandLineArgs = coreRun (do l <- newRef LSPConf defaultConfig defs <- initDefs c <- newRef Ctxt defs s <- newRef Syn initSyntax addPrimitives + processCommandLineArgs extraCommandLineArgs bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX" the (Core ()) $ case bprefix of Just p => setPrefix p @@ -207,9 +215,8 @@ printVersion = do main : IO () main = do - (_::args) <- getArgs + (_ :: args) <- getArgs | _ => putStrLn "Invalid command line" case args of ["--version"] => printVersion - [] => startServer - _ => putStrLn "Invalid Arguments" + args => startServer args diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index eb98816..334526a 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -17,6 +17,7 @@ import Data.OneOf import Data.SortedMap import Data.SortedSet import Data.String +import Idris.CommandLine import Idris.Doc.String import Idris.Error import Idris.IDEMode.Holes @@ -202,7 +203,7 @@ loadURI : Ref LSPConf LSPConfiguration => Ref ROpts REPLOpts => InitializeParams -> URI -> Maybe Int -> Core (Either String ()) loadURI conf uri version = do - logI Server "Loading file \{show uri}" + logI Channel "Loading file \{show uri}" defs <- get Ctxt let extraDirs = defs.options.dirs.extra_dirs update LSPConf ({ openFile := Just (uri, fromMaybe 0 version) }) @@ -213,42 +214,73 @@ loadURI conf uri version = do | Nothing => do let msg = "Cannot find the parent folder for \{show uri}" logE Server msg pure $ Left msg - True <- coreLift $ changeDir startFolder - | False => do let msg = "Cannot change current directory to \{show startFolder}, folder of \{show startFile}" - logE Server msg - pure $ Left msg - Right fname <- catch (maybe (Left "Cannot find the ipkg file") Right <$> findIpkg (Just fpath)) - (pure . Left . show) - | Left err => do let msg = "Cannot load ipkg file for \{show uri}: \{show err}" - logE Server msg + -- Save CWD + cwd <- getWorkingDir + Right packageFilePath <- catch + (maybe + (Left (InternalError "Cannot find the .ipkg file")) + Right + <$> + [| gets LSPConf ipkgFile <+> coreLift (findIpkgFile <&> (<&> (\(dir, name, _) => dir name))) |] + ) + (pure . Left) + | Left err => do let msg = "Cannot load .ipkg file: \{show err}" + logE Channel msg pure $ Left msg - Right res <- coreLift $ File.ReadWrite.readFile fname - | Left err => do let msg = "Cannot read file at \{show uri}" - logE Server msg + logI Server ".ipkg file set to: \{packageFilePath}" + Right packageFileSource <- coreLift $ File.ReadWrite.readFile packageFilePath + | Left err => do let msg = "Cannot read .ipkg at \{packageFilePath} with CWD \{!getWorkingDir}" + logE Channel msg pure $ Left msg - update LSPConf ({ virtualDocuments $= insert uri (fromMaybe 0 version, res ++ "\n") }) - -- A hack to solve some interesting edge-cases around missing newlines ^^^^^^^ - setSource res + logI Server ".ipkg file read!" + let Just (packageFileDir, packageFileName) = splitParent packageFilePath + | _ => throw $ InternalError "Tried to split empty string" + let True = isSuffixOf ".ipkg" packageFileName + | _ => do let msg = "Packages must have an '.ipkg' extension: \{packageFilePath}" + logE Channel msg + pure $ Left msg + -- The CWD should be set to that of the .ipkg file + setWorkingDir packageFileDir + -- Using local packageFileName as we are now in the directory containing that file + -- Idris assumes that CWD and the directory of the .ipkg file coincide + pkg <- parsePkgFile True packageFileName + logI Channel ".ipkg file parsed!" + whenJust (builddir pkg) setBuildDir + setOutputDir (outputdir pkg) + logI Channel "Type checking..." errs <- catch - (buildDeps fname) + (do clock0 <- coreLift (clockTime Monotonic) + errs <- check pkg [] + clock1 <- coreLift (clockTime Monotonic) + let dif = timeDifference clock1 clock0 + logI Server "Type-checking finished in \{show (toNano dif)}ns with \{show (length errs)} errors" + pure errs + ) + -- 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 while building a project. (\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 + + errs <- case null errs of + True => do -- On success, reload the main ttc in a clean context + clearCtxt; addPrimitives + modIdent <- ctxtPathToNS fpath + put MD (initMetadata (PhysicalIdrSrc modIdent)) + mainttc <- getTTCFileName fpath "ttc" + log "import" 10 $ "Reloading " ++ show mainttc ++ " from " ++ fpath + errs0 <- catch ([] <$ readAsMain mainttc) $ (\err => pure [err]) + + + -- Load the associated metadata for interactive editing + mainttm <- getTTCFileName fpath "ttm" + log "import" 10 $ "Reloading " ++ show mainttm + errs1 <- catch ([] <$ readFromTTM mainttm) (\err => pure [err]) + pure (errs0 ++ errs1) + False => pure errs + let caps = (publishDiagnostics <=< textDocument) . capabilities $ conf update LSPConf ({ quickfixes := [], cachedActions := empty, cachedHovers := empty }) @@ -261,6 +293,9 @@ loadURI conf uri version = do put Ctxt ({ options->dirs->extra_dirs := extraDirs } defs) cNames <- completionNames update LSPConf ({completionCache $= insert uri cNames}) + logI Channel "File loaded!" + -- Reset CWD + setWorkingDir cwd pure $ Right () loadIfNeeded : Ref LSPConf LSPConfiguration @@ -290,7 +325,6 @@ withURI conf uri version d k = do case !(loadIfNeeded conf uri version) of Right () => k Left err => do - logE Server "Error while loading \{show uri}: \{show err}" pure $ Left (MkResponseError (Custom 3) err JNull) ||| Guard for requests that requires a successful initialization before being allowed. @@ -519,6 +553,14 @@ handleRequest WorkspaceExecuteCommand str <- render doc setColor c pure $ Right (JString str) +handleRequest WorkspaceExecuteCommand + (MkExecuteCommandParams partialResultToken "setIpkg" (Just [json])) = whenActiveRequest $ \conf => do + logI Channel "Received setIpkg command request" + let Just ipkg = fromJSON {a = String} json + | Nothing => pure $ Left (invalidParams "Expected String") + update LSPConf {ipkgFile := Just ipkg} + logI Channel "Set .ipkg file to \{ipkg}" + pure $ Right (JObject []) handleRequest WorkspaceExecuteCommand (MkExecuteCommandParams _ "metavars" _) = whenActiveRequest $ \conf => do logI Channel "Received metavars command request" Right . toJSON <$> metavarsCmd From d70b5dd158e9dd70bf72cfcdd8aacf2b161000da Mon Sep 17 00:00:00 2001 From: russoul Date: Fri, 29 Nov 2024 18:53:11 +0400 Subject: [PATCH 02/10] Employ lsp's native configuration facility instead of a command to handle ipkg paths --- src/Server/Configuration.idr | 6 +++--- src/Server/Main.idr | 29 +++++++++++------------------ src/Server/ProcessMessage.idr | 13 ++++--------- 3 files changed, 18 insertions(+), 30 deletions(-) diff --git a/src/Server/Configuration.idr b/src/Server/Configuration.idr index f6d1e60..dc4a226 100644 --- a/src/Server/Configuration.idr +++ b/src/Server/Configuration.idr @@ -71,8 +71,8 @@ record LSPConfiguration where virtualDocuments : SortedMap DocumentURI (Int, String) -- Version content ||| Insert only function name for completions briefCompletions : Bool - ||| Maybe specified .ipkg file - ipkgFile : Maybe String + ||| Maybe specified path to the .ipkg file + ipkgPath : Maybe String ||| Server default configuration. Uses standard input and standard output for input/output. export @@ -97,5 +97,5 @@ defaultConfig = , completionCache = empty , virtualDocuments = empty , briefCompletions = False - , ipkgFile = Nothing + , ipkgPath = Nothing } diff --git a/src/Server/Main.idr b/src/Server/Main.idr index 3caece8..c4979f2 100644 --- a/src/Server/Main.idr +++ b/src/Server/Main.idr @@ -71,12 +71,12 @@ parseHeaderPart h = do Nothing => pure $ Right Nothing handleMessage : Ref LSPConf LSPConfiguration - => Ref Ctxt Defs - => Ref UST UState - => Ref Syn SyntaxInfo - => Ref MD Metadata - => Ref ROpts REPLOpts - => Core () + => Ref Ctxt Defs + => Ref UST UState + => Ref Syn SyntaxInfo + => Ref MD Metadata + => Ref ROpts REPLOpts + => Core () handleMessage = do inputHandle <- gets LSPConf inputHandle Right (Just l) <- parseHeaderPart inputHandle @@ -150,21 +150,13 @@ runServer : Ref LSPConf LSPConfiguration => Core () runServer = handleMessage >> runServer -processCommandLineArgs : Ref LSPConf LSPConfiguration => List String -> Core () -processCommandLineArgs [] = pure () -processCommandLineArgs [ipkgFile] = do - update LSPConf {ipkgFile := Just ipkgFile} - logI Server "Set .ipkg file to \{ipkgFile}" -processCommandLineArgs _ = throw (InternalError "Unexpected number of arguments") - -startServer : List String -> IO () -startServer extraCommandLineArgs = +startServer : IO () +startServer = coreRun (do l <- newRef LSPConf defaultConfig defs <- initDefs c <- newRef Ctxt defs s <- newRef Syn initSyntax addPrimitives - processCommandLineArgs extraCommandLineArgs bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX" the (Core ()) $ case bprefix of Just p => setPrefix p @@ -215,8 +207,9 @@ printVersion = do main : IO () main = do - (_ :: args) <- getArgs + (_::args) <- getArgs | _ => putStrLn "Invalid command line" case args of ["--version"] => printVersion - args => startServer args + [] => startServer + _ => putStrLn "Invalid Arguments" diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index 334526a..7cc3cdd 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -187,6 +187,9 @@ processSettings (JObject xs) = do case lookup "briefCompletions" xs of Just (JBoolean b) => update LSPConf ({ briefCompletions := b}) _ => pure () + case lookup "ipkgPath" xs of + Just (JString path) => update LSPConf ({ ipkgPath := Just path}) + _ => pure () processSettings _ = logE Configuration "Incorrect type for options" isDirty : Ref LSPConf LSPConfiguration => DocumentURI -> Core Bool @@ -221,7 +224,7 @@ loadURI conf uri version = do (Left (InternalError "Cannot find the .ipkg file")) Right <$> - [| gets LSPConf ipkgFile <+> coreLift (findIpkgFile <&> (<&> (\(dir, name, _) => dir name))) |] + [| gets LSPConf ipkgPath <+> coreLift (findIpkgFile <&> (<&> (\(dir, name, _) => dir name))) |] ) (pure . Left) | Left err => do let msg = "Cannot load .ipkg file: \{show err}" @@ -553,14 +556,6 @@ handleRequest WorkspaceExecuteCommand str <- render doc setColor c pure $ Right (JString str) -handleRequest WorkspaceExecuteCommand - (MkExecuteCommandParams partialResultToken "setIpkg" (Just [json])) = whenActiveRequest $ \conf => do - logI Channel "Received setIpkg command request" - let Just ipkg = fromJSON {a = String} json - | Nothing => pure $ Left (invalidParams "Expected String") - update LSPConf {ipkgFile := Just ipkg} - logI Channel "Set .ipkg file to \{ipkg}" - pure $ Right (JObject []) handleRequest WorkspaceExecuteCommand (MkExecuteCommandParams _ "metavars" _) = whenActiveRequest $ \conf => do logI Channel "Received metavars command request" Right . toJSON <$> metavarsCmd From eeba508ab24395da96a1a7a4fdf6c08e8ee3e065 Mon Sep 17 00:00:00 2001 From: russoul Date: Fri, 29 Nov 2024 19:10:06 +0400 Subject: [PATCH 03/10] Unset ipkgPath is the config is empty --- src/Server/ProcessMessage.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index 7cc3cdd..f8c58f2 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -189,7 +189,7 @@ processSettings (JObject xs) = do _ => pure () case lookup "ipkgPath" xs of Just (JString path) => update LSPConf ({ ipkgPath := Just path}) - _ => pure () + _ => update LSPConf ({ ipkgPath := Nothing}) processSettings _ = logE Configuration "Incorrect type for options" isDirty : Ref LSPConf LSPConfiguration => DocumentURI -> Core Bool From b562b2c3fa2b17aaeb6c1bd689deec74c1c9ea94 Mon Sep 17 00:00:00 2001 From: russoul Date: Fri, 29 Nov 2024 19:45:27 +0400 Subject: [PATCH 04/10] Add some Channel logging when ipkg path is set --- src/Server/ProcessMessage.idr | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index f8c58f2..58ba243 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -188,8 +188,12 @@ processSettings (JObject xs) = do Just (JBoolean b) => update LSPConf ({ briefCompletions := b}) _ => pure () case lookup "ipkgPath" xs of - Just (JString path) => update LSPConf ({ ipkgPath := Just path}) - _ => update LSPConf ({ ipkgPath := Nothing}) + Just (JString path) => do + logI Channel "Set .ipkg path to \{path}" + update LSPConf ({ ipkgPath := Just path}) + _ => do + logI Channel "Unset .ipkg path" + update LSPConf ({ ipkgPath := Nothing}) processSettings _ = logE Configuration "Incorrect type for options" isDirty : Ref LSPConf LSPConfiguration => DocumentURI -> Core Bool From 7ba99ce256181ed6060243df2c9d0a21557632fd Mon Sep 17 00:00:00 2001 From: russoul Date: Sat, 30 Nov 2024 23:07:28 +0400 Subject: [PATCH 05/10] Bump Idris2 version --- Idris2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Idris2 b/Idris2 index fc3d2a0..33c97f9 160000 --- a/Idris2 +++ b/Idris2 @@ -1 +1 @@ -Subproject commit fc3d2a04dcd7571b8f736ee24b0fd25eefa408e9 +Subproject commit 33c97f92aff1f946fd6e5a30854c2cc175f4bb73 From 3f65f162955ebf0d23e37e42ac480ad44da433e4 Mon Sep 17 00:00:00 2001 From: russoul Date: Sat, 30 Nov 2024 23:14:48 +0400 Subject: [PATCH 06/10] Change logging topic of some messages: Server ~> Channel --- src/Server/ProcessMessage.idr | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index 58ba243..c1082e0 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -234,12 +234,12 @@ loadURI conf uri version = do | Left err => do let msg = "Cannot load .ipkg file: \{show err}" logE Channel msg pure $ Left msg - logI Server ".ipkg file set to: \{packageFilePath}" + logI Channel ".ipkg file configured to: \{packageFilePath}" Right packageFileSource <- coreLift $ File.ReadWrite.readFile packageFilePath | Left err => do let msg = "Cannot read .ipkg at \{packageFilePath} with CWD \{!getWorkingDir}" logE Channel msg pure $ Left msg - logI Server ".ipkg file read!" + logI Channel ".ipkg file read!" let Just (packageFileDir, packageFileName) = splitParent packageFilePath | _ => throw $ InternalError "Tried to split empty string" let True = isSuffixOf ".ipkg" packageFileName @@ -260,7 +260,7 @@ loadURI conf uri version = do errs <- check pkg [] clock1 <- coreLift (clockTime Monotonic) let dif = timeDifference clock1 clock0 - logI Server "Type-checking finished in \{show (toNano dif)}ns with \{show (length errs)} errors" + logI Channel "Type-checking finished in \{show (toNano dif)}ns with \{show (length errs)} errors" pure errs ) -- FIXME: the compiler always dumps the errors on stdout, requires From e1076efd44ba983af14a33424f1ed5087ff0a200 Mon Sep 17 00:00:00 2001 From: russoul Date: Sat, 30 Nov 2024 23:50:01 +0400 Subject: [PATCH 07/10] Don't pass error messages generated in loadURI down the line as they already get printed out eagerly --- src/Server/ProcessMessage.idr | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index c1082e0..edeadf9 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -208,7 +208,7 @@ loadURI : Ref LSPConf LSPConfiguration => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts - => InitializeParams -> URI -> Maybe Int -> Core (Either String ()) + => InitializeParams -> URI -> Maybe Int -> Core (Either () ()) loadURI conf uri version = do logI Channel "Loading file \{show uri}" defs <- get Ctxt @@ -220,7 +220,7 @@ loadURI conf uri version = do let Just (startFolder, startFile) = splitParent fpath | Nothing => do let msg = "Cannot find the parent folder for \{show uri}" logE Server msg - pure $ Left msg + pure $ Left () -- Save CWD cwd <- getWorkingDir Right packageFilePath <- catch @@ -233,19 +233,19 @@ loadURI conf uri version = do (pure . Left) | Left err => do let msg = "Cannot load .ipkg file: \{show err}" logE Channel msg - pure $ Left msg + pure $ Left () logI Channel ".ipkg file configured to: \{packageFilePath}" Right packageFileSource <- coreLift $ File.ReadWrite.readFile packageFilePath | Left err => do let msg = "Cannot read .ipkg at \{packageFilePath} with CWD \{!getWorkingDir}" logE Channel msg - pure $ Left msg + pure $ Left () logI Channel ".ipkg file read!" let Just (packageFileDir, packageFileName) = splitParent packageFilePath | _ => throw $ InternalError "Tried to split empty string" let True = isSuffixOf ".ipkg" packageFileName | _ => do let msg = "Packages must have an '.ipkg' extension: \{packageFilePath}" logE Channel msg - pure $ Left msg + pure $ Left () -- The CWD should be set to that of the .ipkg file setWorkingDir packageFileDir -- Using local packageFileName as we are now in the directory containing that file @@ -311,7 +311,7 @@ loadIfNeeded : Ref LSPConf LSPConfiguration => Ref Syn SyntaxInfo => Ref MD Metadata => Ref ROpts REPLOpts - => InitializeParams -> URI -> Maybe Int -> Core (Either String ()) + => InitializeParams -> URI -> Maybe Int -> Core (Either () ()) loadIfNeeded conf uri version = do Just (oldUri, oldVersion) <- gets LSPConf openFile | Nothing => loadURI conf uri version @@ -332,7 +332,7 @@ withURI conf uri version d k = do case !(loadIfNeeded conf uri version) of Right () => k Left err => do - pure $ Left (MkResponseError (Custom 3) err JNull) + pure $ Left (MkResponseError (Custom 3) "Loading \{show uri} failed (see the logs for more info)" JNull) ||| Guard for requests that requires a successful initialization before being allowed. whenInitializedRequest : Ref LSPConf LSPConfiguration => (InitializeParams -> Core (Either ResponseError a)) -> Core (Either ResponseError a) From 6da6baadab372c54a1b5d088e7d2fd6e61d8695c Mon Sep 17 00:00:00 2001 From: russoul Date: Sun, 1 Dec 2024 23:24:00 +0400 Subject: [PATCH 08/10] Diagnostics rework --- pack.toml | 5 +++ src/Server/Diagnostics.idr | 32 ++++++------------ src/Server/ProcessMessage.idr | 37 ++++++++++---------- src/Server/QuickFix.idr | 13 ++++---- src/Server/Response.idr | 63 ++++++++++++++++++++++++++++------- 5 files changed, 91 insertions(+), 59 deletions(-) create mode 100644 pack.toml diff --git a/pack.toml b/pack.toml new file mode 100644 index 0000000..caa7bb2 --- /dev/null +++ b/pack.toml @@ -0,0 +1,5 @@ +[custom.all.idris2-lsp] +type = "local" +path = "." +ipkg = "idris2-lsp.ipkg" +packagePath = true diff --git a/src/Server/Diagnostics.idr b/src/Server/Diagnostics.idr index ee61d41..a404c73 100644 --- a/src/Server/Diagnostics.idr +++ b/src/Server/Diagnostics.idr @@ -113,20 +113,15 @@ warningToDiagnostic : Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => (caps : Maybe PublishDiagnosticsClientCapabilities) - -> (uri : URI) -> (warning : Warning) -> Core Diagnostic -warningToDiagnostic caps uri warning = do +warningToDiagnostic caps warning = do defs <- get Ctxt warningAnn <- pwarning (killWarningLoc warning) let loc = Just (getWarningLoc warning) let wdir = defs.options.dirs.working_dir - p <- maybe (pure uri.path) (pure . (wdir ) <=< nsToSource replFC) - ((\case PhysicalIdrSrc ident => Just ident; _ => Nothing) . fst <=< isNonEmptyFC =<< loc) - if System.Path.parse (uriPathToSystemPath uri.path) == System.Path.parse p - then do let related = Nothing -- TODO related diagnostics? - pure $ buildDiagnostic Warning loc warningAnn related - else pure $ buildDiagnostic Warning (toStart <$> loc) ("In" <++> pretty0 p <+> colon <++> warningAnn) Nothing + let related = Nothing -- TODO related diagnostics? + pure (buildDiagnostic Warning loc warningAnn related) ||| Computes a LSP `Diagnostic` from a compiler error. @@ -136,20 +131,15 @@ warningToDiagnostic caps uri warning = do ||| @err The compiler error. export errorToDiagnostic : Ref Ctxt Defs - => Ref Syn SyntaxInfo - => Ref ROpts REPLOpts - => (caps : Maybe PublishDiagnosticsClientCapabilities) - -> (uri : URI) - -> (error : Error) - -> Core Diagnostic -errorToDiagnostic caps uri err = do + => Ref Syn SyntaxInfo + => Ref ROpts REPLOpts + => (caps : Maybe PublishDiagnosticsClientCapabilities) + -> (error : Error) + -> Core Diagnostic +errorToDiagnostic caps err = do defs <- get Ctxt error <- perror (killErrorLoc err) let loc = getErrorLoc err let wdir = defs.options.dirs.working_dir - p <- maybe (pure uri.path) (pure . (wdir ) <=< nsToSource replFC) - ((\case PhysicalIdrSrc ident => Just ident; _ => Nothing) . fst <=< isNonEmptyFC =<< loc) - if System.Path.parse (uriPathToSystemPath uri.path) == System.Path.parse p - then do let related = (flip toMaybe (getRelatedErrors uri err) <=< relatedInformation) =<< caps - pure $ buildDiagnostic Error loc error related - else pure $ buildDiagnostic Error (toStart <$> loc) ("In" <++> pretty0 p <+> colon <++> error) Nothing + let related = Nothing -- TODO + pure (buildDiagnostic Error loc error related) diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index edeadf9..b803109 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -217,10 +217,6 @@ loadURI conf uri version = do update ROpts { evalResultName := Nothing } resetContext (Virtual Interactive) let fpath = uriPathToSystemPath uri.path - let Just (startFolder, startFile) = splitParent fpath - | Nothing => do let msg = "Cannot find the parent folder for \{show uri}" - logE Server msg - pure $ Left () -- Save CWD cwd <- getWorkingDir Right packageFilePath <- catch @@ -263,10 +259,8 @@ loadURI conf uri version = do logI Channel "Type-checking finished in \{show (toNano dif)}ns with \{show (length errs)} errors" pure errs ) - -- FIXME: the compiler always dumps the errors on stdout, requires + -- FIXME: the compiler sometimes dumps the errors on stdout, requires -- a compiler change. - -- NOTE on catch: It seems the compiler sometimes throws errors instead - -- of accumulating them while building a project. (\err => do logE Server "Caught error which shouldn't be leaked while loading file: \{show err}" pure [err]) @@ -275,17 +269,9 @@ loadURI conf uri version = do True => do -- On success, reload the main ttc in a clean context clearCtxt; addPrimitives modIdent <- ctxtPathToNS fpath - put MD (initMetadata (PhysicalIdrSrc modIdent)) mainttc <- getTTCFileName fpath "ttc" log "import" 10 $ "Reloading " ++ show mainttc ++ " from " ++ fpath - errs0 <- catch ([] <$ readAsMain mainttc) $ (\err => pure [err]) - - - -- Load the associated metadata for interactive editing - mainttm <- getTTCFileName fpath "ttm" - log "import" 10 $ "Reloading " ++ show mainttm - errs1 <- catch ([] <$ readFromTTM mainttm) (\err => pure [err]) - pure (errs0 ++ errs1) + catch ([] <$ readAsMain mainttc) $ (\err => pure [err]) False => pure errs @@ -295,7 +281,11 @@ loadURI conf uri version = do defs <- get Ctxt session <- getSession let warnings = if session.warningsAsErrors then [] else reverse (warnings defs) - sendDiagnostics caps uri version warnings errs + -- Clear out all previously issued diagnostics + for_ !(SortedSet.toList <$> gets LSPConf errorFiles) sendEmptyDiagnostic + filesWithErrors <- sendDiagnostics caps warnings errs + logI Channel "Files containing errors: \{show filesWithErrors}" + update LSPConf { errorFiles := SortedSet.fromList filesWithErrors } defs <- get Ctxt put Ctxt ({ options->dirs->extra_dirs := extraDirs } defs) cNames <- completionNames @@ -539,8 +529,18 @@ handleRequest TextDocumentSemanticTokensFull params = whenActiveRequest $ \conf Nothing <- gets LSPConf (lookup params.textDocument.uri . semanticTokensSentFiles) | Just tokens => pure $ pure $ (make $ tokens) withURI conf params.textDocument.uri Nothing (pure $ Left (MkResponseError RequestCancelled "Document Errors" JNull)) $ do + -- Load the associated metadata for interactive editing + let fpath = uriPathToSystemPath params.textDocument.uri.path + modIdent <- ctxtPathToNS fpath + -- put MD (initMetadata (PhysicalIdrSrc modIdent)) + -- TODO: Reset everything related to *that* file only! + mainttm <- getTTCFileName fpath "ttm" + log "import" 10 $ "Reloading " ++ show mainttm + [] <- catch ([] <$ readFromTTM mainttm) (\err => pure [err]) + | _ => pure $ Left (MkResponseError RequestCancelled "Couldn't load TTM for the file" JNull) + Right src <- coreLift $ File.ReadWrite.readFile fpath + | Left err => pure $ Left (MkResponseError RequestCancelled "Couldn't read the file" JNull) md <- get MD - src <- getSource let srcLines = lines src let getLineLength = \lineNum => maybe 0 (cast . length) $ elemAt srcLines (integerToNat (cast lineNum)) tokens <- getSemanticTokens md getLineLength @@ -619,7 +619,6 @@ handleNotification TextDocumentDidSave params = whenActiveNotification $ \conf = logI Channel "Received didSave notification for \{show params.textDocument.uri}" update LSPConf ( { dirtyFiles $= delete params.textDocument.uri - , errorFiles $= delete params.textDocument.uri , semanticTokensSentFiles $= delete params.textDocument.uri }) ignore $ loadURI conf params.textDocument.uri Nothing diff --git a/src/Server/QuickFix.idr b/src/Server/QuickFix.idr index 97855fb..977a681 100644 --- a/src/Server/QuickFix.idr +++ b/src/Server/QuickFix.idr @@ -70,7 +70,6 @@ findQuickfix : Ref LSPConf LSPConfiguration => Ref Ctxt Defs => Ref Syn SyntaxInfo => Ref ROpts REPLOpts - => Ref MD Metadata => (caps : Maybe PublishDiagnosticsClientCapabilities) -> (uri : URI) -> Error @@ -82,7 +81,7 @@ findQuickfix caps uri (InLHS _ _ err) = findQuickfix caps uri err findQuickfix caps uri (InRHS _ _ err) = findQuickfix caps uri err findQuickfix caps uri err@(PatternVariableUnifies fc fct env n tm) = whenJust (isNonEmptyFC fct) $ \fc => do - diagnostic <- errorToDiagnostic caps uri err + diagnostic <- errorToDiagnostic caps err let textEdit = MkTextEdit (cast fc) (nameRoot n) let codeAction = buildQuickfix uri "Unify pattern names" diagnostic textEdit update LSPConf ({ quickfixes $= (codeAction ::) }) @@ -91,7 +90,7 @@ findQuickfix caps uri err@(ValidCase fc _ (Left tm)) = Just (f, args) <- (Utils.uncons' <=< init' <=< map words) <$> (getSourceLine (startLine fc + 1)) | Nothing => logE QuickFix "Error while fetching source line" >> pure () let line = unwords $ f :: args ++ ["=", "?\{f}_rhs_not_impossible"] - diagnostic <- errorToDiagnostic caps uri err + diagnostic <- errorToDiagnostic caps err let textEdit = MkTextEdit (cast fc) line let codeAction = buildQuickfix uri "Remove impossible keyword" diagnostic textEdit update LSPConf ({ quickfixes $= (codeAction ::) }) @@ -102,7 +101,7 @@ findQuickfix caps uri err@(NotCovering fc n (MissingCases cs)) = let endline = endLine fc src <- String.lines <$> getSource let blank = findBlankLine (drop (integerToNat (cast endline)) src) endline - diagnostic <- errorToDiagnostic caps uri err + diagnostic <- errorToDiagnostic caps err let range = MkRange (MkPosition blank 0) (MkPosition blank 0) let textEdit = MkTextEdit range cases let missingCodeAction = buildQuickfix uri "Add missing cases" diagnostic textEdit @@ -112,7 +111,7 @@ findQuickfix caps uri err@(NotCovering fc n (MissingCases cs)) = update LSPConf ({ quickfixes $= ([missingCodeAction, partialCodeAction] ++) }) findQuickfix caps uri err@(NotCovering fc n _) = whenJust (isNonEmptyFC fc) $ \fc => do - diagnostic <- errorToDiagnostic caps uri err + diagnostic <- errorToDiagnostic caps err let startline = startLine fc let range = MkRange (MkPosition startline 0) (MkPosition startline 0) let textEdit = MkTextEdit range "partial\n" @@ -120,7 +119,7 @@ findQuickfix caps uri err@(NotCovering fc n _) = update LSPConf ({ quickfixes $= (codeAction ::) }) findQuickfix caps uri err@(NotTotal fc n _) = whenJust (isNonEmptyFC fc) $ \fc => do - diagnostic <- errorToDiagnostic caps uri err + diagnostic <- errorToDiagnostic caps err let startline = startLine fc let range = MkRange (MkPosition startline 0) (MkPosition startline 0) let textEdit = MkTextEdit range "covering\n" @@ -128,7 +127,7 @@ findQuickfix caps uri err@(NotTotal fc n _) = update LSPConf ({ quickfixes $= (codeAction ::) }) findQuickfix caps uri (MaybeMisspelling err ns) = whenJust (isNonEmptyFC =<< getErrorLoc err) $ \fc => do - diagnostic <- errorToDiagnostic caps uri err + diagnostic <- errorToDiagnostic caps err let range = cast fc let codeActions = map (\n => buildQuickfix uri "Replace with \{show n}" diagnostic (MkTextEdit range n)) . forget $ ns update LSPConf ({ quickfixes $= (codeActions ++) }) diff --git a/src/Server/Response.idr b/src/Server/Response.idr index 8d8fc28..0fab3b6 100644 --- a/src/Server/Response.idr +++ b/src/Server/Response.idr @@ -5,10 +5,12 @@ module Server.Response import Core.Context import Core.Core +import Core.Directory import Core.Env import Core.FC import Data.OneOf import Data.String +import Data.List import Idris.Pretty import Idris.REPL.Opts import Idris.Resugar @@ -22,6 +24,7 @@ import Server.Diagnostics import Server.Log import Server.Utils import System.File +import System.Path ||| Header for messages on-the-wire. ||| By specification only Content-Length is mandatory. @@ -115,28 +118,64 @@ sendUnknownResponseMessage err = do writeResponse (toJSON {a = ResponseMessage Initialize} (Failure (make MkNull) err)) logI Channel "Sent response to unknown method" -||| Sends a LSP `Diagnostic` message for a given, potentially versioned, source -||| that produces some errors. +groupByFile : Ref Ctxt Defs => List Error -> Core (List (Maybe String, List1 Error)) +groupByFile list = do + withFileName <- traverse (\err => pure (!(getFilePath err), err)) list + pure $ map pull (groupBy sameFileName withFileName) + where + pull : List1 (a, b) -> (a, List1 b) + pull ((x, y) ::: []) = (x, singleton y) + pull ((_, y) ::: t :: ts) = mapSnd (y `cons`) (pull (t ::: ts)) + + sameFileName : (Maybe String, Error) -> (Maybe String, Error) -> Bool + sameFileName = on (==) fst + + getFilePath : Error -> Core (Maybe String) + getFilePath err = do + defs <- get Ctxt + let wdir = defs.options.dirs.working_dir + let loc = getErrorLoc err + traverseOpt (pure . (wdir ) <=< nsToSource replFC) ((\case PhysicalIdrSrc ident => Just ident; _ => Nothing) . fst <=< isNonEmptyFC =<< loc) + +||| Sends a LSP `Diagnostic` message for the whole project ||| ||| @caps The client capabilities related to diagnostics -||| @uri The source URI. ||| @version Optional source version. ||| @errs Errors produced while trying to check the source. +||| @return list of files that contain at least one error export sendDiagnostics : Ref LSPConf LSPConfiguration => Ref Syn SyntaxInfo => Ref Ctxt Defs => Ref ROpts REPLOpts => (caps : Maybe PublishDiagnosticsClientCapabilities) - -> (uri : DocumentURI) - -> (version : Maybe Int) -> (warnings : List Warning) -> (errs : List Error) - -> Core () -sendDiagnostics caps uri version warnings errs = do - warningDiagnostics <- traverse (warningToDiagnostic caps uri) warnings - errorDiagnostics <- traverse (errorToDiagnostic caps uri) errs - let diagnostics = warningDiagnostics ++ errorDiagnostics - let params = MkPublishDiagnosticsParams uri version diagnostics - logI Diagnostic "Sending diagnostic message for \{show uri}" + -> Core (List DocumentURI) +sendDiagnostics caps warnings errs = do + catMaybes <$> for !(groupByFile errs) mbForFile + where + forFile : DocumentURI -> List Error -> Core () + forFile uri errs = do + warningDiagnostics <- traverse (warningToDiagnostic caps) warnings + errorDiagnostics <- traverse (errorToDiagnostic caps) errs + let diagnostics = warningDiagnostics ++ errorDiagnostics + let params = MkPublishDiagnosticsParams uri Nothing diagnostics + logI Diagnostic "Sending diagnostic message for \{show uri}" + sendNotificationMessage TextDocumentPublishDiagnostics params + + mbForFile : (Maybe String, List1 Error) -> Core (Maybe DocumentURI) + mbForFile (Nothing, _) = pure Nothing -- TODO: Currently silently suppressed, not good + mbForFile (Just path, errs) = Just (pathToURI path) <$ forFile (pathToURI path) (forget errs) + +export +sendEmptyDiagnostic : Ref LSPConf LSPConfiguration + => Ref Syn SyntaxInfo + => Ref Ctxt Defs + => Ref ROpts REPLOpts + => DocumentURI + -> Core () +sendEmptyDiagnostic uri = do + let params = MkPublishDiagnosticsParams uri Nothing [] + logI Diagnostic "Sending empty diagnostic message for \{show uri}" sendNotificationMessage TextDocumentPublishDiagnostics params From 7694b2c9f18ae50f1cae16c1b660b2b7f49d849c Mon Sep 17 00:00:00 2001 From: russoul Date: Sun, 8 Dec 2024 18:56:43 +0400 Subject: [PATCH 09/10] Fix code actions --- src/Server/ProcessMessage.idr | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index b803109..86bf98a 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -463,6 +463,15 @@ handleRequest TextDocumentCodeAction params = whenActiveRequest $ \conf => do (do quickfixActions <- if maybe True (CodeActionKind.QuickFix `elem`) params.context.only then map Just <$> gets LSPConf quickfixes else pure [] + let fpath = uriPathToSystemPath params.textDocument.uri.path + setMainFile (Just fpath) + Right src <- coreLift $ File.ReadWrite.readFile fpath + | Left err => pure $ Left (MkResponseError RequestCancelled "Couldn't read the file source file" JNull) + setSource src + modIdent <- ctxtPathToNS fpath + mainttm <- getTTCFileName fpath "ttm" + [] <- catch ([] <$ readFromTTM mainttm) (\err => pure [err]) + | _ => pure $ Left (MkResponseError RequestCancelled "Couldn't load TTM for the file" JNull) exprSearchActions <- map Just <$> exprSearch params splitAction <- caseSplit params lemmaAction <- makeLemma params From 0ef47b5cce03d40239f0957a46fefd02ab90837c Mon Sep 17 00:00:00 2001 From: russoul Date: Mon, 16 Dec 2024 01:04:36 +0400 Subject: [PATCH 10/10] Remove precomputation of name completions (unused) which is *very* slow --- src/Language/LSP/Completion/Handler.idr | 1 + src/Language/LSP/Definition.idr | 7 --- src/Language/LSP/DocumentHighlight.idr | 9 +--- src/Language/LSP/DocumentSymbol.idr | 10 ++-- src/Server/Configuration.idr | 3 -- src/Server/ProcessMessage.idr | 69 ++++++++++--------------- 6 files changed, 34 insertions(+), 65 deletions(-) diff --git a/src/Language/LSP/Completion/Handler.idr b/src/Language/LSP/Completion/Handler.idr index 725a5e1..3626b2a 100644 --- a/src/Language/LSP/Completion/Handler.idr +++ b/src/Language/LSP/Completion/Handler.idr @@ -82,6 +82,7 @@ arguments (PrimVal fc c) = [] arguments (Erased fc why) = [] arguments (TType fc n) = [] +-- PERF: This is currently *very* slow. It can take up 5-10 seconds for when running this on this (idris2-lsp) project export covering completionNames : Ref Ctxt Defs diff --git a/src/Language/LSP/Definition.idr b/src/Language/LSP/Definition.idr index cf5a79c..1cace86 100644 --- a/src/Language/LSP/Definition.idr +++ b/src/Language/LSP/Definition.idr @@ -65,13 +65,6 @@ gotoDefinition : Ref Ctxt Defs => DefinitionParams -> Core (Maybe Location) gotoDefinition params = do logI GotoDefinition "Checking for \{show params.textDocument.uri} at \{show params.position}" - -- Check actual doc - Just (actualUri, _) <- gets LSPConf openFile - | Nothing => logE GotoDefinition "No open file" >> pure Nothing - let True = actualUri == params.textDocument.uri - | False => do - logD GotoDefinition "Expected request for the currently opened file \{show actualUri}, instead received \{show params.textDocument.uri}" - pure Nothing let line = params.position.line let col = params.position.character diff --git a/src/Language/LSP/DocumentHighlight.idr b/src/Language/LSP/DocumentHighlight.idr index f672e49..4cc93d1 100644 --- a/src/Language/LSP/DocumentHighlight.idr +++ b/src/Language/LSP/DocumentHighlight.idr @@ -25,13 +25,8 @@ documentHighlights : Ref Ctxt Defs => Ref LSPConf LSPConfiguration => DocumentHighlightParams -> Core (List DocumentHighlight) documentHighlights params = do - logI DocumentHighlight "Searching for \{show params.textDocument.uri}" - Just (uri, _) <- gets LSPConf openFile - | Nothing => logE DocumentHighlight "No open file" >> pure [] - let True = uri == params.textDocument.uri - | False => do - logD DocumentHighlight "Expected request for the currently opened file \{show uri}, instead received \{show params.textDocument.uri}" - pure [] + let uri = show params.textDocument.uri + logI DocumentHighlight "Searching for \{uri}" let line = params.position.line let col = params.position.character diff --git a/src/Language/LSP/DocumentSymbol.idr b/src/Language/LSP/DocumentSymbol.idr index 614a14e..64cb7df 100644 --- a/src/Language/LSP/DocumentSymbol.idr +++ b/src/Language/LSP/DocumentSymbol.idr @@ -60,13 +60,9 @@ documentSymbol : Ref Ctxt Defs => Ref LSPConf LSPConfiguration => DocumentSymbolParams -> Core (List SymbolInformation) documentSymbol params = do - logI DocumentSymbol "Making for \{show params.textDocument.uri}" - Just (uri, _) <- gets LSPConf openFile - | Nothing => logE DocumentSymbol "No open file" >> pure [] - let True = uri == params.textDocument.uri - | False => do - logD DocumentSymbol "Expected request for the currently opened file \{show uri}, instead received \{show params.textDocument.uri}" - pure [] + let uri = params.textDocument.uri + logI DocumentSymbol "Making for \{show uri}" + defs <- get Ctxt -- Get the current and visible namespaces from the context let currentNamespaces = defs.currentNS :: defs.nestedNS diff --git a/src/Server/Configuration.idr b/src/Server/Configuration.idr index dc4a226..1c1fba5 100644 --- a/src/Server/Configuration.idr +++ b/src/Server/Configuration.idr @@ -47,8 +47,6 @@ record LSPConfiguration where ||| True if the client has completed the shutdown protocol. ||| @see https://microsoft.github.io/language-server-protocol/specifications/specification-3-16/#shutdown isShutdown : Bool - ||| The currently loaded file, if any, and its version. - openFile : Maybe (DocumentURI, Int) ||| Files with modification not saved. Command will fail on these files. dirtyFiles : SortedSet DocumentURI ||| Files with errors @@ -85,7 +83,6 @@ defaultConfig = , logSeverity = Debug , initialized = Nothing , isShutdown = False - , openFile = Nothing , dirtyFiles = empty , errorFiles = empty , semanticTokensSentFiles = empty diff --git a/src/Server/ProcessMessage.idr b/src/Server/ProcessMessage.idr index 86bf98a..6e037f7 100644 --- a/src/Server/ProcessMessage.idr +++ b/src/Server/ProcessMessage.idr @@ -72,6 +72,9 @@ import System.Clock import System.Directory import System.File +toMillis : Integer -> Integer +toMillis = cast {to = Integer} . (/ 1000000.0) . cast {to = Double} + ||| Mostly copied from Idris.REPL.displayResult. partial replResultToDoc : Ref Ctxt Defs @@ -213,7 +216,6 @@ loadURI conf uri version = do logI Channel "Loading file \{show uri}" defs <- get Ctxt let extraDirs = defs.options.dirs.extra_dirs - update LSPConf ({ openFile := Just (uri, fromMaybe 0 version) }) update ROpts { evalResultName := Nothing } resetContext (Virtual Interactive) let fpath = uriPathToSystemPath uri.path @@ -256,7 +258,7 @@ loadURI conf uri version = do errs <- check pkg [] clock1 <- coreLift (clockTime Monotonic) let dif = timeDifference clock1 clock0 - logI Channel "Type-checking finished in \{show (toNano dif)}ns with \{show (length errs)} errors" + logI Channel "Type-checking finished in \{show (toMillis (toNano dif))}ms with \{show (length errs)} errors" pure errs ) -- FIXME: the compiler sometimes dumps the errors on stdout, requires @@ -288,27 +290,14 @@ loadURI conf uri version = do update LSPConf { errorFiles := SortedSet.fromList filesWithErrors } defs <- get Ctxt put Ctxt ({ options->dirs->extra_dirs := extraDirs } defs) - cNames <- completionNames - update LSPConf ({completionCache $= insert uri cNames}) + -- FIX: This is crazy slow (and unused?) + -- cNames <- completionNames + -- update LSPConf ({completionCache $= insert uri cNames}) logI Channel "File loaded!" -- Reset CWD setWorkingDir cwd pure $ Right () -loadIfNeeded : Ref LSPConf LSPConfiguration - => Ref Ctxt Defs - => Ref UST UState - => Ref Syn SyntaxInfo - => Ref MD Metadata - => Ref ROpts REPLOpts - => InitializeParams -> URI -> Maybe Int -> Core (Either () ()) -loadIfNeeded conf uri version = do - Just (oldUri, oldVersion) <- gets LSPConf openFile - | Nothing => loadURI conf uri version - if (oldUri == uri && (isNothing version || (Just oldVersion) == version)) - then pure $ Right () - else loadURI conf uri version - withURI : Ref LSPConf LSPConfiguration => Ref Ctxt Defs => Ref UST UState @@ -319,10 +308,21 @@ withURI : Ref LSPConf LSPConfiguration -> URI -> Maybe Int -> Core (Either ResponseError a) -> Core (Either ResponseError a) -> Core (Either ResponseError a) withURI conf uri version d k = do when !(isError uri) $ ignore $ logW Server "Trying to load \{show uri} which has errors" >> d - case !(loadIfNeeded conf uri version) of - Right () => k - Left err => do - pure $ Left (MkResponseError (Custom 3) "Loading \{show uri} failed (see the logs for more info)" JNull) + logI Channel "Loading metadata for file: \{show uri}" + clock0 <- coreLift (clockTime Monotonic) + let fpath = uriPathToSystemPath uri.path + setMainFile (Just fpath) + Right src <- coreLift $ File.ReadWrite.readFile fpath + | Left err => pure $ Left (MkResponseError RequestCancelled "Couldn't read the file source file" JNull) + setSource src + modIdent <- ctxtPathToNS fpath + mainttm <- getTTCFileName fpath "ttm" + [] <- catch ([] <$ readFromTTM mainttm) (\err => pure [err]) + | _ => pure $ Left (MkResponseError RequestCancelled "Couldn't load TTM for the file" JNull) + clock1 <- coreLift (clockTime Monotonic) + let dif = timeDifference clock1 clock0 + logI Channel "Loading metadata finished in \{show (toMillis (toNano dif))}ms" + k ||| Guard for requests that requires a successful initialization before being allowed. whenInitializedRequest : Ref LSPConf LSPConfiguration => (InitializeParams -> Core (Either ResponseError a)) -> Core (Either ResponseError a) @@ -463,15 +463,6 @@ handleRequest TextDocumentCodeAction params = whenActiveRequest $ \conf => do (do quickfixActions <- if maybe True (CodeActionKind.QuickFix `elem`) params.context.only then map Just <$> gets LSPConf quickfixes else pure [] - let fpath = uriPathToSystemPath params.textDocument.uri.path - setMainFile (Just fpath) - Right src <- coreLift $ File.ReadWrite.readFile fpath - | Left err => pure $ Left (MkResponseError RequestCancelled "Couldn't read the file source file" JNull) - setSource src - modIdent <- ctxtPathToNS fpath - mainttm <- getTTCFileName fpath "ttm" - [] <- catch ([] <$ readFromTTM mainttm) (\err => pure [err]) - | _ => pure $ Left (MkResponseError RequestCancelled "Couldn't load TTM for the file" JNull) exprSearchActions <- map Just <$> exprSearch params splitAction <- caseSplit params lemmaAction <- makeLemma params @@ -538,15 +529,9 @@ handleRequest TextDocumentSemanticTokensFull params = whenActiveRequest $ \conf Nothing <- gets LSPConf (lookup params.textDocument.uri . semanticTokensSentFiles) | Just tokens => pure $ pure $ (make $ tokens) withURI conf params.textDocument.uri Nothing (pure $ Left (MkResponseError RequestCancelled "Document Errors" JNull)) $ do - -- Load the associated metadata for interactive editing + logI Channel "Loading semantic tokens for file: \{show (params.textDocument.uri)}" + clock0 <- coreLift (clockTime Monotonic) let fpath = uriPathToSystemPath params.textDocument.uri.path - modIdent <- ctxtPathToNS fpath - -- put MD (initMetadata (PhysicalIdrSrc modIdent)) - -- TODO: Reset everything related to *that* file only! - mainttm <- getTTCFileName fpath "ttm" - log "import" 10 $ "Reloading " ++ show mainttm - [] <- catch ([] <$ readFromTTM mainttm) (\err => pure [err]) - | _ => pure $ Left (MkResponseError RequestCancelled "Couldn't load TTM for the file" JNull) Right src <- coreLift $ File.ReadWrite.readFile fpath | Left err => pure $ Left (MkResponseError RequestCancelled "Couldn't read the file" JNull) md <- get MD @@ -554,6 +539,9 @@ handleRequest TextDocumentSemanticTokensFull params = whenActiveRequest $ \conf let getLineLength = \lineNum => maybe 0 (cast . length) $ elemAt srcLines (integerToNat (cast lineNum)) tokens <- getSemanticTokens md getLineLength update LSPConf ({ semanticTokensSentFiles $= insert params.textDocument.uri tokens }) + clock1 <- coreLift (clockTime Monotonic) + let dif = timeDifference clock1 clock0 + logI Channel "Loading semantic tokens finished in \{show (toMillis (toNano dif))}ms" pure $ pure $ (make $ tokens) handleRequest WorkspaceExecuteCommand (MkExecuteCommandParams partialResultToken "repl" (Just [json])) = whenActiveRequest $ \conf => do @@ -649,8 +637,7 @@ handleNotification TextDocumentDidChange params = whenActiveNotification $ \conf handleNotification TextDocumentDidClose params = whenActiveNotification $ \conf => do logI Channel "Received didClose notification for \{show params.textDocument.uri}" - update LSPConf ({ openFile := Nothing - , quickfixes := [] + update LSPConf ({ quickfixes := [] , cachedActions := empty , cachedHovers := empty , dirtyFiles $= delete params.textDocument.uri