Merge branch 'release-v0.6.0'

* release-v0.6.0: (38 commits) Bump version and update changelogs Do not build Language.Rzk.VSCode.* modules with GHCJS Add rzk.yaml to specify files to check Do not depend on lsp and lsp-types with GHCJS Update rzk.nix Cache well-typed modules even in presence of type errors in other modules Slightly improve rzk.yaml error/warning Support incremental typechecking with in-memory cache of well-typed modules Invalidate cache for all files after the first modified file Use file watcher to invalidate cache for typechecked files Sketch cache implementation Add line location to errors Add rzk.nix back (generated manually via cabal2nix --compiler ghcjs) Revert back to calling cabal2nix from the workflow Remove rzk.nix Try using callCabal2nix in try-rzk/default.nix instead Use cabal2nix --compiler ghcjs to generate rzk.nix for GHCJS Add a handler for typechecking all files in config Define a Yaml schema for our config file Add the filepath package for processing paths ...
rzk-lang · Sep 23, 2023 · af5f66a · af5f66a
2 parents 67f7d5a + cea45e3
commit af5f66a
Show file tree

Hide file tree

Showing 24 changed files with 4,009 additions and 3,727 deletions.
diff --git a/docs/docs/getting-started/changelog.md b/docs/docs/getting-started/changelog.md
@@ -6,6 +6,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.6.0 — 2023-09-23
+
+This version introduces a proper LSP server with basic support for incremental typechecking
+and some minor improvements:
+
+1. LSP server with incremental typechecking (see [#95](https://github.com/rzk-lang/rzk/pull/95));
+2. Improve error messages for unclosed `#section` and extra `#end` (see [#91](https://github.com/rzk-lang/rzk/pull/91)).
+
 ## v0.5.7 — 2023-09-21
 
 This version contains two fixes (see [#88](https://github.com/rzk-lang/rzk/pull/88)) for issues discovered in [rzk-lang/sHoTT#30](https://github.com/rzk-lang/sHoTT/pull/30#issuecomment-1729212862):

diff --git a/rzk.yaml b/rzk.yaml
@@ -0,0 +1,2 @@
+include:
+  - docs/docs/examples/recId.rzk.md
diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md
@@ -6,6 +6,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.6.0 — 2023-09-23
+
+This version introduces a proper LSP server with basic support for incremental typechecking
+and some minor improvements:
+
+1. LSP server with incremental typechecking (see [#95](https://github.com/rzk-lang/rzk/pull/95));
+2. Improve error messages for unclosed `#section` and extra `#end` (see [#91](https://github.com/rzk-lang/rzk/pull/91)).
+
 ## v0.5.7 — 2023-09-21
 
 This version contains two fixes (see [#88](https://github.com/rzk-lang/rzk/pull/88)) for issues discovered in [rzk-lang/sHoTT#30](https://github.com/rzk-lang/sHoTT/pull/30#issuecomment-1729212862):

diff --git a/rzk/package.yaml b/rzk/package.yaml
@@ -1,10 +1,10 @@
 name: rzk
-version: 0.5.7
-github: "rzk-lang/rzk"
+version: 0.6.0
+github: 'rzk-lang/rzk'
 license: BSD3
-author: "Nikolai Kudasov"
-maintainer: "[email protected]"
-copyright: "2023 Nikolai Kudasov"
+author: 'Nikolai Kudasov'
+maintainer: '[email protected]'
+copyright: '2023 Nikolai Kudasov'
 
 extra-source-files:
   - README.md
@@ -33,6 +33,10 @@ dependencies:
   - text
   - optparse-generic
   - Glob
+  - lens
+  - filepath
+  - stm
+  - yaml
 
 ghc-options:
   - -Wall
@@ -53,6 +57,16 @@ library:
         - Language.Rzk.Syntax.Test
         - Language.Rzk.Syntax.ErrM
         - Language.Rzk.Syntax.Skel
+    - condition: '!impl(ghcjs)'
+      exposed-modules:
+        - Language.Rzk.VSCode.Env
+        - Language.Rzk.VSCode.Handlers
+        - Language.Rzk.VSCode.Lsp
+        - Language.Rzk.VSCode.State
+        - Language.Rzk.VSCode.Tokenize
+      dependencies:
+        - lsp
+        - lsp-types
 
 executables:
   rzk:
@@ -65,7 +79,7 @@ executables:
     dependencies:
       - rzk
     when:
-      - condition: "!impl(ghcjs)"
+      - condition: '!impl(ghcjs)'
         dependencies:
           - with-utf8
 

diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
@@ -5,7 +5,7 @@ cabal-version: 1.12
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.5.7
+version:        0.6.0
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
@@ -36,8 +36,6 @@ library
       Language.Rzk.Syntax.Lex
       Language.Rzk.Syntax.Par
       Language.Rzk.Syntax.Print
-      Language.Rzk.VSCode.Tokenize
-      Language.Rzk.VSCode.Tokens
       Rzk
       Rzk.Main
       Rzk.TypeCheck
@@ -56,11 +54,25 @@ library
     , base >=4.7 && <5
     , bifunctors
     , bytestring
+    , filepath
+    , lens
     , mtl
     , optparse-generic
+    , stm
     , template-haskell
     , text
+    , yaml
   default-language: Haskell2010
+  if !impl(ghcjs)
+    exposed-modules:
+        Language.Rzk.VSCode.Env
+        Language.Rzk.VSCode.Handlers
+        Language.Rzk.VSCode.Lsp
+        Language.Rzk.VSCode.State
+        Language.Rzk.VSCode.Tokenize
+    build-depends:
+        lsp
+      , lsp-types
 
 executable rzk
   main-is: Main.hs
@@ -79,11 +91,15 @@ executable rzk
     , base >=4.7 && <5
     , bifunctors
     , bytestring
+    , filepath
+    , lens
     , mtl
     , optparse-generic
     , rzk
+    , stm
     , template-haskell
     , text
+    , yaml
   default-language: Haskell2010
   if !impl(ghcjs)
     build-depends:
@@ -107,10 +123,14 @@ test-suite doctests
     , bifunctors
     , bytestring
     , doctest
+    , filepath
+    , lens
     , mtl
     , optparse-generic
+    , stm
     , template-haskell
     , text
+    , yaml
   default-language: Haskell2010
 
 test-suite rzk-test
@@ -131,9 +151,13 @@ test-suite rzk-test
     , base >=4.7 && <5
     , bifunctors
     , bytestring
+    , filepath
+    , lens
     , mtl
     , optparse-generic
     , rzk
+    , stm
     , template-haskell
     , text
+    , yaml
   default-language: Haskell2010
diff --git a/rzk/rzk.nix b/rzk/rzk.nix
@@ -1,26 +1,26 @@
 { mkDerivation, aeson, alex, array, base, bifunctors, bytestring
-, doctest, Glob, happy, hpack, lib, mtl, optparse-generic
-, QuickCheck, template-haskell, text
+, doctest, filepath, Glob, happy, hpack, lens, lib, mtl
+, optparse-generic, QuickCheck, stm, template-haskell, text, yaml
 }:
 mkDerivation {
   pname = "rzk";
-  version = "0.5.7";
+  version = "0.6.0";
   src = ./.;
   isLibrary = true;
   isExecutable = true;
   libraryHaskellDepends = [
-    aeson array base bifunctors bytestring Glob mtl optparse-generic
-    template-haskell text
+    aeson array base bifunctors bytestring filepath Glob lens mtl
+    optparse-generic stm template-haskell text yaml
   ];
   libraryToolDepends = [ alex happy hpack ];
   executableHaskellDepends = [
-    aeson array base bifunctors bytestring Glob mtl optparse-generic
-    template-haskell text
+    aeson array base bifunctors bytestring filepath Glob lens mtl
+    optparse-generic stm template-haskell text yaml
   ];
   executableToolDepends = [ alex happy ];
   testHaskellDepends = [
-    aeson array base bifunctors bytestring doctest Glob mtl
-    optparse-generic QuickCheck template-haskell text
+    aeson array base bifunctors bytestring doctest filepath Glob lens
+    mtl optparse-generic QuickCheck stm template-haskell text yaml
   ];
   testToolDepends = [ alex happy ];
   prePatch = "hpack";

diff --git a/rzk/src/Language/Rzk/Syntax.cf b/rzk/src/Language/Rzk/Syntax.cf
@@ -37,7 +37,8 @@ define commandVariable name term = CommandAssume [name] term ;
 commandVariables.         Command ::= "#variables" [VarIdent] ":" Term ;
 define commandVariables names term = CommandAssume names term ;
 
-CommandSection.           Command ::= "#section" SectionName ";" [Command] "#end" SectionName ;
+CommandSection.           Command ::= "#section" SectionName ;
+CommandSectionEnd.        Command ::= "#end" SectionName ;
 
 CommandDefine.            Command ::= "#define" VarIdent DeclUsedVars [Param] ":" Term ":=" Term ;
 commandDefineNoParams.    Command ::= "#define" VarIdent DeclUsedVars ":" Term ":=" Term ;

diff --git a/rzk/src/Language/Rzk/Syntax/Abs.hs b/rzk/src/Language/Rzk/Syntax/Abs.hs
@@ -53,7 +53,8 @@ data Command' a
     | CommandComputeNF a (Term' a)
     | CommandPostulate a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a)
     | CommandAssume a [VarIdent' a] (Term' a)
-    | CommandSection a (SectionName' a) [Command' a] (SectionName' a)
+    | CommandSection a (SectionName' a)
+    | CommandSectionEnd a (SectionName' a)
     | CommandDefine a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a) (Term' a)
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
 
@@ -234,7 +235,8 @@ instance HasPosition Command where
     CommandComputeNF p _ -> p
     CommandPostulate p _ _ _ _ -> p
     CommandAssume p _ _ -> p
-    CommandSection p _ _ _ -> p
+    CommandSection p _ -> p
+    CommandSectionEnd p _ -> p
     CommandDefine p _ _ _ _ _ -> p
 
 instance HasPosition DeclUsedVars where

diff --git a/rzk/src/Language/Rzk/Syntax/Doc.txt b/rzk/src/Language/Rzk/Syntax/Doc.txt
@@ -82,7 +82,8 @@ All other symbols are terminals.
   |  |  **|**  | ``#assume`` //[VarIdent]// ``:`` //Term//
   |  |  **|**  | ``#variable`` //VarIdent// ``:`` //Term//
   |  |  **|**  | ``#variables`` //[VarIdent]// ``:`` //Term//
-  |  |  **|**  | ``#section`` //SectionName// ``;`` //[Command]// ``#end`` //SectionName//
+  |  |  **|**  | ``#section`` //SectionName//
+  |  |  **|**  | ``#end`` //SectionName//
   |  |  **|**  | ``#define`` //VarIdent// //DeclUsedVars// //[Param]// ``:`` //Term// ``:=`` //Term//
   |  |  **|**  | ``#define`` //VarIdent// //DeclUsedVars// ``:`` //Term// ``:=`` //Term//
   |  |  **|**  | ``#def`` //VarIdent// //DeclUsedVars// //[Param]// ``:`` //Term// ``:=`` //Term//

diff --git a/rzk/src/Language/Rzk/Syntax/Par.hs b/rzk/src/Language/Rzk/Syntax/Par.hs