[WIP] Support multi-ipkg setup; Rework how we build the workspace project and when we compute metadata (TTM)

pack.toml

@@ -0,0 +1,5 @@
+[custom.all.idris2-lsp]
+type = "local"
+path = "."
+ipkg = "idris2-lsp.ipkg"
+packagePath = true

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

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
@@ -71,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
@@ -186,6 +190,13 @@ 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) => 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
@@ -200,83 +211,93 @@ 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 clock0 <- coreLift (clockTime Monotonic)
+                errs <- check pkg []
+                clock1 <- coreLift (clockTime Monotonic)
+                let dif = timeDifference clock1 clock0
+                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
+            --        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_ !(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
-  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 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
@@ -287,11 +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
-         logE Server "Error while loading \{show uri}: \{show err}"
-         pure $ Left (MkResponseError (Custom 3) err 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)
@@ -498,12 +529,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 (toMillis (toNano dif))}ms"
       pure $ pure $ (make $ tokens)
 handleRequest WorkspaceExecuteCommand
   (MkExecuteCommandParams partialResultToken "repl" (Just [json])) = whenActiveRequest $ \conf => do
@@ -578,7 +616,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 +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