[WIP] Support multi-ipkg setup; Rework how we build the workspace project and when we compute metadata (TTM) #231
Conversation
…already get printed out eagerly
|
Currently there is one regression that needs to be attended to: when loading a file, the whole project (defined by ipkg) gets built (or loaded from cache). That is slower and less ergonomic, as error messages appearing in independent files will block syntax highlighting and interactive commands for the target file. |
| (Left (InternalError "Cannot find the .ipkg file")) | ||
| Right | ||
| <$> | ||
| [| gets LSPConf ipkgPath <+> coreLift (findIpkgFile <&> (<&> (\(dir, name, _) => dir </> name))) |] |
There was a problem hiding this comment.
This line gets a bit terse IMO right around the time your anonymous function begins with <&>. I suppose this isn't a requested change unless you also are on the fence about it. I can follow, but I'm spending more effort reading the syntax than I usually like to.
src/Server/ProcessMessage.idr
Outdated
| @@ -212,43 +220,74 @@ loadURI conf uri version = do | |||
| let Just (startFolder, startFile) = splitParent fpath | |||
There was a problem hiding this comment.
startFolder and startFile are not used anymore. did you forget to remove their calculation from here or did you intend to use them below?
There was a problem hiding this comment.
Oh, just forgot to remove them. If only we had a linter...
| -- 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 }) |
There was a problem hiding this comment.
your code never sets errorFiles does it?
There was a problem hiding this comment.
Hm, right. Probably removed unintentionally.
| | 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") }) |
There was a problem hiding this comment.
The new code doesn't add the current file to the virtual documents.
Russoul
changed the title
TODO: Update the description
The main change is around
loadURI. First we figure out which ipkg file to use (either one provided in LSP configuration by the client or we try to find one via idris2 api). The first option takes priority. Next we call an api function that builds the main module (including all dependencies) specified in the ipkg file. Rest is unchanged.Another small change is addition of a new LSP configuration option, called "ipkgPath", which can be sent to the server from the client on initialisation and/or changed any time later. It represents optional relative path to the ipkg file. The root path is that where LSP server has been started.
Functionally, the PR makes it possible to switch/specify the ipkg file mid-air. Next time
loadURIgets triggered the project will get rebuilt against the last specified ipkg file. Moreover, due to TTC cache, the switch may be close to instantaneous in case no single file needs a fresh build or a rebuild.