Replace single-file tracking with whole-project type-checking

- Remove the `openFile` field and `loadIfNeeded` logic; add `ipkgPath`
  config option so the server knows which .ipkg to use
- `loadURI` now builds the full project via `check pkg` instead of
  `buildDeps`, then reloads the main module's TTM on success
- `withURI` loads metadata from TTM directly without re-type-checking
- `sendDiagnostics` now groups errors by source file and sends per-file
  diagnostics across the whole project; clears stale diagnostics first
- Drop the "must match currently open file" guard from Definition,
  DocumentHighlight, and DocumentSymbol handlers

Author: Russoul

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

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

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

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
@@ -71,6 +69,8 @@ record LSPConfiguration where
   virtualDocuments : SortedMap DocumentURI (Int, String) -- Version content
   ||| Insert only function name for completions
   briefCompletions : Bool
+  ||| Maybe specified path to the .ipkg file
+  ipkgPath : Maybe String
 
 ||| Server default configuration. Uses standard input and standard output for input/output.
 export
@@ -83,7 +83,6 @@ defaultConfig =
     , logSeverity             = Debug
     , initialized             = Nothing
     , isShutdown              = False
-    , openFile                = Nothing
     , dirtyFiles              = empty
     , errorFiles              = empty
     , semanticTokensSentFiles = empty
@@ -94,5 +93,6 @@ defaultConfig =
     , nextRequestId           = 0
     , completionCache         = empty
     , virtualDocuments        = empty
-    , briefCompletions       = False
+    , briefCompletions        = False
+    , ipkgPath                = Nothing
     }

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)

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
@@ -176,15 +177,28 @@ processSettings (JObject xs) = do
          when (pp.showMachineNames /= b) $ do
            setPPrint ({ showMachineNames := b } pp)
            update LSPConf ({ cachedHovers := empty })
+         logI Configuration "Show machine names set to \{show b}"
        Just _ => logE Configuration "Incorrect type for show machine names, expected boolean"
        Nothing => pure ()
   case lookup "logSeverity" xs of
        Just (JString ll) =>
-         whenJust (parseSeverity ll) $ \l => update LSPConf ({ logSeverity := l})
+         case parseSeverity ll of
+           Just l => update LSPConf ({ logSeverity := l}) >> logI Configuration "Log severity set to \{show l}"
+           Nothing => logE Configuration "Incorrect string for log severity"
        Just _ => logE Configuration "Incorrect type for log severity, expected string"
        Nothing => pure ()
   case lookup "briefCompletions" xs of
-      Just (JBoolean b) => update LSPConf ({ briefCompletions := b})
+      Just (JBoolean b) => do
+        update LSPConf ({ briefCompletions := b})
+        logI Configuration "Brief completions set to \{show b}"
+      _ => pure ()
+  case lookup "ipkgPath" xs of
+      Just (JString path) => do
+        update LSPConf ({ ipkgPath := Just path})
+        logI Channel "Ipkg path set to \{path}"
+      Just JNull => do
+        update LSPConf ({ ipkgPath := Nothing})
+        logI Channel "Ipkg path unset"
       _ => pure ()
 processSettings _ = logE Configuration "Incorrect type for options"
 
@@ -200,83 +214,91 @@ 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 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) })
   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 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
-                     pure $ Left msg
-  Right res <- coreLift $ File.ReadWrite.readFile fname
-    | Left err => do let msg = "Cannot read file at \{show uri}"
-                     logE Server 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
+  -- Save CWD
+  cwd <- getWorkingDir
+  Right packageFilePath <- catch
+    (maybe
+       (Left (InternalError "Cannot find the .ipkg file"))
+       Right
+      <$>
+     [| gets LSPConf ipkgPath <+> coreLift (findIpkgFile <&> (<&> (\(dir, name, _) => dir </> name))) |]
+    )
+    (pure . Left)
+    | Left err => do let msg = "Cannot load .ipkg file: \{show err}"
+                     logE Channel 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 ()
+  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 ()
+  -- 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
+                (duration, errs) <- clock $ check pkg []
+                logI Channel "Type-checking finished in \{show duration.milliseconds}ms with \{show (length errs)} errors"
+                pure errs
+            )
+            -- FIXME: the compiler sometimes dumps the errors on stdout, requires
+            --        a compiler change.
             (\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
+      mainttc <- getTTCFileName fpath "ttc"
+      log "import" 10 $ "Reloading " ++ show mainttc ++ " from " ++ fpath
+      catch ([] <$ readAsMain mainttc) $ (\err => pure [err])
+    False => pure errs
+
 
   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)
-  sendDiagnostics caps uri version warnings errs
+  -- Clear out all previously issued diagnostics
+  for_ !(Prelude.toList <$> gets LSPConf errorFiles) sendEmptyDiagnostic
+  filesWithErrors <- sendDiagnostics caps uri 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
+  (duration, cNames) <- clock completionNames
+  logI Channel "Populating completion cache took \{show duration.milliseconds}ms"
   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 String ())
-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
@@ -285,13 +307,25 @@ withURI : Ref LSPConf LSPConfiguration
        => Ref ROpts REPLOpts
        => InitializeParams
        -> 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
-         logE Server "Error while loading \{show uri}: \{show err}"
-         pure $ Left (MkResponseError (Custom 3) err JNull)
+withURI conf uri version d k =
+  case !(isError uri) of
+    True => logI Server "Trying to load \{show uri} which has errors" >> d
+    False => do
+      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 dif.milliseconds}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)
@@ -498,12 +532,19 @@ 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
+      logI Channel "Loading semantic tokens for file: \{show (params.textDocument.uri)}"
+      clock0 <- coreLift (clockTime Monotonic)
+      let fpath = uriPathToSystemPath params.textDocument.uri.path
+      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
       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 dif.milliseconds}ms"
       pure $ pure $ (make $ tokens)
 handleRequest WorkspaceExecuteCommand
   (MkExecuteCommandParams partialResultToken "repl" (Just [json])) = whenActiveRequest $ \conf => do
@@ -578,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
@@ -600,8 +640,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
@@ -614,3 +653,4 @@ handleNotification TextDocumentDidClose params = whenActiveNotification $ \conf
 
 handleNotification method params = whenActiveNotification $ \conf =>
   logW Channel "Received unhandled notification for method \{stringify $ toJSON method}"
+