diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -6,6 +6,15 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.4 — 2024-04-01 + +Fixes: +- Fix caching in Rzk Language Server, especially in presence of errors (see [#167](https://github.com/rzk-lang/rzk/pull/167)) +- Fix CI for the Rzk Playground (see [#174](https://github.com/rzk-lang/rzk/pull/174)) + +This release also contains minor refactoring (see [#165](https://github.com/rzk-lang/rzk/pull/165)) +and a typo fix (see [#171](https://github.com/rzk-lang/rzk/pull/171)). + ## v0.7.3 — 2023-12-16 Fixes: @@ -82,7 +91,7 @@ ## v0.6.5 — 2023-10-01 -This version contains mostly intrastructure improvements: +This version contains mostly infrastructure improvements: - Typecheck using `rzk.yaml` if it exists (see [#119](https://github.com/rzk-lang/rzk/pull/119)) - Update Rzk Playground and Nix Flake (see [#84](https://github.com/rzk-lang/rzk/pull/84)) @@ -91,7 +100,7 @@ - GHCJS 9.6 is now used - Support `snippet={code}` or `code={code}` param (see [#118](https://github.com/rzk-lang/rzk/pull/118)) - Support for `snippet_url={URL}` is temporarily dropped -- Update to GHC 9.6, latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see [#116](https://github.com/rzk-lang/rzk/pull/116)) +- Update to GHC 9.6, the latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see [#116](https://github.com/rzk-lang/rzk/pull/116)) - Add logging for Rzk Language Server (see [#114](https://github.com/rzk-lang/rzk/pull/114)) Fixes: @@ -100,7 +109,7 @@ ## v0.6.4 — 2023-09-27 -This version improves the stucture of the project, in particular w.r.t dependencies: +This version improves the structure of the project, in particular w.r.t dependencies: - Add custom snapshot and explicit lower bounds (see [#108](https://github.com/rzk-lang/rzk/pull/108)) @@ -111,7 +120,7 @@ - Fix command line `rzk typecheck` (see [#106](https://github.com/rzk-lang/rzk/pull/106)) - Previous version ignored failures in the command line - (the bug was introced when allowing better autocompletion in LSP). + (the bug was introduced when allowing better autocompletion in LSP). ## v0.6.2 — 2023-09-26 @@ -145,14 +154,14 @@ ## v0.5.6 — 2023-09-19 -This version fixes the behaviour of glob (see [`77b7cc0`](https://github.com/rzk-lang/rzk/commit/77b7cc0494fe0bfd1c9f1aa83db20f42cfda5794)). +This version fixes the behavior of glob (see [`77b7cc0`](https://github.com/rzk-lang/rzk/commit/77b7cc0494fe0bfd1c9f1aa83db20f42cfda5794)). ## v0.5.5 — 2023-09-19 This version contains Unicode and tope logic-related fixes: 1. Fix (add missing checks) for subshapes (see [#85](https://github.com/rzk-lang/rzk/pull/85)); -2. Allow to handle wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83)); +2. Allow handling wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83)); 3. Fix Unicode on machines with non-standard locales (see [#82](https://github.com/rzk-lang/rzk/pull/82)); 4. Specify `happy` and `alex` as build tools to fix cabal build from Hackage (see [#80](https://github.com/rzk-lang/rzk/pull/80)). 5. Add configuration for MkDocs plugin for Rzk (see [#79](https://github.com/rzk-lang/rzk/pull/79)). @@ -172,7 +181,7 @@ 2. Hint about possible shape coercions (see [#67](https://github.com/rzk-lang/rzk/pull/67)); 3. Enable doctests (see [#68](https://github.com/rzk-lang/rzk/pull/68)); 4. Improve documentation (add recommended installation instructions via VS Code) -5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983)); +5. Migrate from `fizruk` to `rzk-lang` organization on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983)); 6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66)); ## v0.5.2 — 2023-07-05 @@ -228,7 +237,7 @@ ## v0.3.0 — 2023-04-28 -This version introduces an experimental feature for generating visualisations for simplicial terms in SVG. +This version introduces an experimental feature for generating visualizations for simplicial terms in SVG. To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`): ```rzk @@ -252,7 +261,7 @@ ### Language Syntax is almost entirely backwards compatible with version 0.1.0. -Typechecking has been fixed and improved. +Type checking has been fixed and improved. #### Breaking Changes @@ -293,7 +302,7 @@ := (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ] ``` -6. Restrictions can now support multiple subshapes, effectively internalising `recOR`: +6. Restrictions can now support multiple subshapes, effectively internalizing `recOR`: ```rzk #def hom (A : U) (x y : A) : U @@ -308,7 +317,7 @@ 9. `recOR` now supports alternative syntax with an arbitrary number of subshapes: `recOR( tope1 |-> term1, tope2 |-> term2, ..., topeN |-> termN )` -10. Now it is possible to have type ascriptions: `t as T`. This can help with ensuring types of subexpressions in parts of formalisations, or to upcast types. +10. Now it is possible to have type ascriptions: `t as T`. This can help with ensuring types of subexpressions in parts of formalizations, or to upcast types. 11. New (better) commands are now supported: @@ -350,8 +359,8 @@ ### Internal representation A new internal representation (a version of second-order abstract syntax) -allows to stop worrying about name captures in substitutions, +allows stopping worrying about name captures in substitutions, so the implementation is much more trustworthy. -The new representation will also allow to bring in higher-order unification in the future, for better type inference, matching, etc. +The new representation will also allow bringing in higher-order unification in the future, for better type inference, matching, etc. New representation also allowed annotating each (sub)term with its type to avoid recomputations and some other minor speedups. There are still some performance issues, which need to be debugged, but overall it is much faster than version 0.1.0 already. diff --git a/rzk.cabal b/rzk.cabal --- a/rzk.cabal +++ b/rzk.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: rzk -version: 0.7.3 +version: 0.7.4 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types diff --git a/src/Language/Rzk/VSCode/Env.hs b/src/Language/Rzk/VSCode/Env.hs --- a/src/Language/Rzk/VSCode/Env.hs +++ b/src/Language/Rzk/VSCode/Env.hs @@ -3,12 +3,18 @@ import Control.Concurrent.STM import Control.Monad.Reader import Language.LSP.Server +import Language.Rzk.Free.Syntax (VarIdent) import Language.Rzk.VSCode.Config (ServerConfig) -import Rzk.TypeCheck (Decl') +import Rzk.TypeCheck (Decl', TypeErrorInScopedContext) -type RzkTypecheckCache = [(FilePath, [Decl'])] +data RzkCachedModule = RzkCachedModule + { cachedModuleDecls :: [Decl'] + , cachedModuleErrors :: [TypeErrorInScopedContext VarIdent] + } -data RzkEnv = RzkEnv +type RzkTypecheckCache = [(FilePath, RzkCachedModule)] + +newtype RzkEnv = RzkEnv { rzkEnvTypecheckCache :: TVar RzkTypecheckCache } @@ -17,7 +23,6 @@ typecheckCache <- newTVarIO [] return RzkEnv { rzkEnvTypecheckCache = typecheckCache } - type LSP = LspT ServerConfig (ReaderT RzkEnv IO) diff --git a/src/Language/Rzk/VSCode/Handlers.hs b/src/Language/Rzk/VSCode/Handlers.hs --- a/src/Language/Rzk/VSCode/Handlers.hs +++ b/src/Language/Rzk/VSCode/Handlers.hs @@ -1,21 +1,28 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE RecordWildCards #-} module Language.Rzk.VSCode.Handlers ( typecheckFromConfigFile, provideCompletions, formatDocument, + provideSemanticTokens, + handleFilesChanged, ) where import Control.Exception (SomeException, evaluate, try) import Control.Lens import Control.Monad (forM_, when) +import Control.Monad.Except (ExceptT (ExceptT), + MonadError (throwError), + modifyError, runExceptT) import Control.Monad.IO.Class (MonadIO (..)) import Data.Default.Class -import Data.List (sort, (\\)) +import Data.List (isSuffixOf, sort, (\\)) import Data.Maybe (fromMaybe, isNothing) import qualified Data.Text as T import qualified Data.Yaml as Yaml @@ -25,7 +32,7 @@ HasLabel (label), HasParams (params), HasTextDocument (textDocument), - HasUri (uri)) + HasUri (uri), changes, uri) import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types import Language.LSP.Server @@ -36,10 +43,12 @@ import Language.Rzk.Free.Syntax (RzkPosition (RzkPosition), VarIdent (getVarIdent)) import Language.Rzk.Syntax (Module, VarIdent' (VarIdent), - parseModuleFile, printTree) + parseModuleFile, + parseModuleSafe, printTree) import Language.Rzk.VSCode.Config (ServerConfig (ServerConfig, formatEnabled)) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Logging +import Language.Rzk.VSCode.Tokenize (tokenizeModule) import Rzk.Format (FormattingEdit (..), formatTextEdits) import Rzk.Project.Config (ProjectConfig (include)) @@ -94,7 +103,8 @@ rawPaths <- liftIO $ globDir (map compile (include config)) rootPath let paths = concatMap sort rawPaths - cachedModules <- getCachedTypecheckedModules + typecheckedCachedModules <- getCachedTypecheckedModules + let cachedModules = map (\(path, RzkCachedModule{..}) -> (path, cachedModuleDecls)) typecheckedCachedModules let cachedPaths = map fst cachedModules modifiedFiles = paths \\ cachedPaths @@ -118,13 +128,14 @@ -- cache well-typed modules logInfo (show (length checkedModules) ++ " modules successfully typechecked") logInfo (show (length errors) ++ " errors found") - cacheTypecheckedModules checkedModules + let checkedModules' = map (\(path, decls) -> (path, RzkCachedModule decls (filter ((== path) . filepathOfTypeError) errors))) checkedModules + cacheTypecheckedModules checkedModules' return (errors, checkedModules) -- Reset all published diags -- TODO: remove this after properly grouping by path below, after which there can be an empty list of errors -- TODO: handle clearing diagnostics for files that got removed from the project (rzk.yaml) - forM_ paths $ \path -> do + forM_ modifiedFiles $ \path -> do publishDiagnostics 0 (filePathToNormalizedUri path) Nothing (partitionBySource []) -- Report parse errors to the client @@ -194,8 +205,9 @@ logDebug ("Found " ++ show (length cachedModules) ++ " modules in the cache") let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri -- Take all the modules up to and including the currently open one - let modules = takeWhileInc ((/= currentFile) . fst) cachedModules + let modules = map ignoreErrors $ takeWhileInc ((/= currentFile) . fst) cachedModules where + ignoreErrors (path, RzkCachedModule{..}) = (path, cachedModuleDecls) takeWhileInc _ [] = [] takeWhileInc p (x:xs) | p x = x : takeWhileInc p xs @@ -249,3 +261,80 @@ else do logDebug "Formatting is disabled in config" res $ Right $ InR Null + +provideSemanticTokens :: Handler LSP 'Method_TextDocumentSemanticTokensFull +provideSemanticTokens req responder = do + let doc = req ^. params . textDocument . uri . to toNormalizedUri + mdoc <- getVirtualFile doc + possibleTokens <- case virtualFileText <$> mdoc of + Nothing -> return (Left "Failed to get file content") + Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $ + parseModuleSafe (filter (/= '\r') $ T.unpack sourceCode) + case possibleTokens of + Left err -> do + -- Exception occurred when parsing the module + logWarning ("Failed to tokenize file: " ++ err) + Right tokens -> do + let encoded = encodeTokens defaultSemanticTokensLegend $ relativizeTokens tokens + case encoded of + Left _err -> do + -- Failed to encode the tokens + return () + Right list -> + responder (Right (InL (SemanticTokens Nothing list))) + + +data IsChanged + = HasChanged + | NotChanged + +-- | Detects if the given path has changes in its declaration compared to what's in the cache +isChanged :: RzkTypecheckCache -> FilePath -> LSP IsChanged +isChanged cache path = toIsChanged $ do + let cacheWithoutErrors = map (fmap cachedModuleDecls) cache + errors <- maybeToEitherLSP $ cachedModuleErrors <$> lookup path cache + cachedDecls <- maybeToEitherLSP $ cachedModuleDecls <$> lookup path cache + module' <- toExceptTLifted $ parseModuleFile path + e <- toExceptTLifted $ try @SomeException $ evaluate $ + defaultTypeCheck (typecheckModulesWithLocationIncremental (takeWhile ((/= path) . fst) cacheWithoutErrors) [(path, module')]) + (checkedModules, errors') <- toExceptT $ return e + decls' <- maybeToEitherLSP $ lookup path checkedModules + return $ if null errors' && null errors && decls' == cachedDecls + then NotChanged + else HasChanged + where + toExceptT = modifyError (const ()) . ExceptT + toExceptTLifted = toExceptT . liftIO + maybeToEitherLSP = \case + Nothing -> throwError () + Just x -> return x + toIsChanged m = runExceptT m >>= \case + Left _ -> return HasChanged -- in case of error consider the file has changed + Right x -> return x + +hasNotChanged :: RzkTypecheckCache -> FilePath -> LSP Bool +hasNotChanged cache path = isChanged cache path >>= \case + HasChanged -> return False + NotChanged -> return True + +-- | Monadic 'dropWhile' +dropWhileM :: (Monad m) => (a -> m Bool) -> [a] -> m [a] +dropWhileM _ [] = return [] +dropWhileM p (x:xs) = do + q <- p x + if q + then dropWhileM p xs + else return (x:xs) + +handleFilesChanged :: Handler LSP 'Method_WorkspaceDidChangeWatchedFiles +handleFilesChanged msg = do + let modifiedPaths = msg ^.. params . changes . traverse . uri . to uriToFilePath . _Just + if any ("rzk.yaml" `isSuffixOf`) modifiedPaths + then do + logDebug "rzk.yaml modified. Clearing module cache" + resetCacheForAllFiles + else do + cache <- getCachedTypecheckedModules + actualModified <- dropWhileM (hasNotChanged cache) modifiedPaths + resetCacheForFiles actualModified + typecheckFromConfigFile diff --git a/src/Language/Rzk/VSCode/Lsp.hs b/src/Language/Rzk/VSCode/Lsp.hs --- a/src/Language/Rzk/VSCode/Lsp.hs +++ b/src/Language/Rzk/VSCode/Lsp.hs @@ -1,84 +1,26 @@ {-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TypeApplications #-} module Language.Rzk.VSCode.Lsp where -import Control.Lens (_Just, to, (^.), (^..)) import Control.Monad.IO.Class import Control.Monad.Reader import Data.Default.Class (Default (def)) -import Data.List (isSuffixOf) import qualified Data.Text as T -import Language.LSP.Protocol.Lens (HasParams (params), - HasTextDocument (textDocument), - HasUri (uri), changes, uri) import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types import Language.LSP.Server -import Language.LSP.VFS (virtualFileText) -import Control.Exception (SomeException, evaluate, try) -import Control.Monad.Except (ExceptT (ExceptT), - MonadError (throwError), - modifyError, runExceptT) import Data.Aeson (Result (Error, Success), fromJSON) -import Language.Rzk.Syntax (parseModuleFile, - parseModuleSafe) import Language.Rzk.VSCode.Config (ServerConfig (..)) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Handlers -import Language.Rzk.VSCode.Logging -import Language.Rzk.VSCode.Tokenize (tokenizeModule) -import Rzk.TypeCheck (defaultTypeCheck, - typecheckModulesWithLocationIncremental) -- | The maximum number of diagnostic messages to send to the client maxDiagnosticCount :: Int maxDiagnosticCount = 100 -data IsChanged - = HasChanged - | NotChanged - --- | Detects if the given path has changes in its declaration compared to what's in the cache -isChanged :: RzkTypecheckCache -> FilePath -> LSP IsChanged -isChanged cache path = toIsChanged $ do - cachedDecls <- maybeToEitherLSP $ lookup path cache - module' <- toExceptTLifted $ parseModuleFile path - e <- toExceptTLifted $ try @SomeException $ evaluate $ - defaultTypeCheck (typecheckModulesWithLocationIncremental (takeWhile ((/= path) . fst) cache) [(path, module')]) - (checkedModules, _errors) <- toExceptT $ return e - decls' <- maybeToEitherLSP $ lookup path checkedModules - return $ if decls' == cachedDecls - then NotChanged - else HasChanged - where - toExceptT = modifyError (const ()) . ExceptT - toExceptTLifted = toExceptT . liftIO - maybeToEitherLSP = \case - Nothing -> throwError () - Just x -> return x - toIsChanged m = runExceptT m >>= \case - Left _ -> return HasChanged -- in case of error consider the file has changed - Right x -> return x - -hasNotChanged :: RzkTypecheckCache -> FilePath -> LSP Bool -hasNotChanged cache path = isChanged cache path >>= \case - HasChanged -> return False - NotChanged -> return True - --- | Monadic 'dropWhile' -dropWhileM :: (Monad m) => (a -> m Bool) -> [a] -> m [a] -dropWhileM _ [] = return [] -dropWhileM p (x:xs) = do - q <- p x - if q - then dropWhileM p xs - else return (x:xs) - handlers :: Handlers LSP handlers = mconcat @@ -86,20 +28,9 @@ -- TODO: add logging -- Empty handlers to silence the errors , notificationHandler SMethod_TextDocumentDidOpen $ \_msg -> pure () - -- , requestHandler SMethod_TextDocumentFormatting $ \_req _res -> pure () , notificationHandler SMethod_TextDocumentDidChange $ \_msg -> pure () , notificationHandler SMethod_TextDocumentDidClose $ \_msg -> pure () - , notificationHandler SMethod_WorkspaceDidChangeWatchedFiles $ \msg -> do - let modifiedPaths = msg ^.. params . changes . traverse . uri . to uriToFilePath . _Just - if any ("rzk.yaml" `isSuffixOf`) modifiedPaths - then do - logDebug "rzk.yaml modified. Clearing module cache" - resetCacheForAllFiles - else do - cache <- getCachedTypecheckedModules - actualModified <- dropWhileM (hasNotChanged cache) modifiedPaths - resetCacheForFiles actualModified - typecheckFromConfigFile + , notificationHandler SMethod_WorkspaceDidChangeWatchedFiles handleFilesChanged , notificationHandler SMethod_TextDocumentDidSave $ \_msg -> do -- TODO: check if the file is included in the config's `include` list. -- If not (and not in `exclude`) either, issue a warning. @@ -115,25 +46,7 @@ -- range' = Range pos pos -- responder (Right $ InL rsp) , requestHandler SMethod_TextDocumentCompletion provideCompletions - , requestHandler SMethod_TextDocumentSemanticTokensFull $ \req responder -> do - let doc = req ^. params . textDocument . uri . to toNormalizedUri - mdoc <- getVirtualFile doc - possibleTokens <- case virtualFileText <$> mdoc of - Nothing -> return (Left "Failed to get file content") - Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $ - parseModuleSafe (filter (/= '\r') $ T.unpack sourceCode) - case possibleTokens of - Left err -> do - -- Exception occurred when parsing the module - logWarning ("Failed to tokenize file: " ++ err) - Right tokens -> do - let encoded = encodeTokens defaultSemanticTokensLegend $ relativizeTokens tokens - case encoded of - Left _err -> do - -- Failed to encode the tokens - return () - Right list -> - responder (Right (InL SemanticTokens { _resultId = Nothing, _data_ = list })) + , requestHandler SMethod_TextDocumentSemanticTokensFull provideSemanticTokens , requestHandler SMethod_TextDocumentFormatting formatDocument ] diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs --- a/src/Rzk/TypeCheck.hs +++ b/src/Rzk/TypeCheck.hs @@ -5,8 +5,6 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE TypeSynonymInstances #-} module Rzk.TypeCheck where import Control.Applicative ((<|>))