Merge branch 'release-v0.6.3'

* release-v0.6.3: Bump version and update changelogs Fix rzk typecheck (CLI version)
rzk-lang · Sep 27, 2023 · 6969508 · 6969508
2 parents 9120caa + 0c66cff
commit 6969508
Show file tree

Hide file tree

Showing 7 changed files with 80 additions and 59 deletions.
diff --git a/docs/docs/getting-started/changelog.md b/docs/docs/getting-started/changelog.md
@@ -6,6 +6,15 @@ 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.3 — 2023-09-27
+
+This version contains a fix for the command line interface of `rzk`:
+
+- 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).
+
 ## v0.6.2 — 2023-09-26
 
 This version contains some improvements in efficiency and also to the language server:

diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md
@@ -6,6 +6,15 @@ 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.3 — 2023-09-27
+
+This version contains a fix for the command line interface of `rzk`:
+
+- 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).
+
 ## v0.6.2 — 2023-09-26
 
 This version contains some improvements in efficiency and also to the language server:

diff --git a/rzk/package.yaml b/rzk/package.yaml
@@ -1,5 +1,5 @@
 name: rzk
-version: 0.6.2
+version: 0.6.3
 github: 'rzk-lang/rzk'
 license: BSD3
 author: 'Nikolai Kudasov'

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.6.2
+version:        0.6.3
 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

diff --git a/rzk/rzk.nix b/rzk/rzk.nix
@@ -5,7 +5,7 @@
 }:
 mkDerivation {
   pname = "rzk";
-  version = "0.6.2";
+  version = "0.6.3";
   src = ./.;
   isLibrary = true;
   isExecutable = true;

diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
@@ -38,7 +38,7 @@ main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categor
           , ppTypeErrorInScopedContext' BottomUp err
           ]
         exitFailure
-      Right _declsByPath -> putStrLn "Everything is ok!"
+      Right _decls -> putStrLn "Everything is ok!"
 
   Lsp ->
 #ifndef __GHCJS__

diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs
@@ -77,12 +77,11 @@ typecheckModulesWithLocation = \case
   [] -> return []
   m@(path, _) : ms -> do
     (decls, errs) <- typecheckModuleWithLocation m
-    if null errs
-      then
-        localDeclsPrepared decls $
-          ((path, decls) :) <$> typecheckModulesWithLocation ms
-      else
-        return [(path, decls)]
+    case errs of
+      err : _ -> do
+        throwError err
+      [] -> localDeclsPrepared decls $
+        ((path, decls) :) <$> typecheckModulesWithLocation ms
 
 typecheckModules :: [Rzk.Module] -> TypeCheck VarIdent [Decl']
 typecheckModules = \case
@@ -302,19 +301,19 @@ type TypeError' = TypeError VarIdent
 ppTypeError' :: TypeError' -> String
 ppTypeError' = \case
   TypeErrorOther msg -> msg
-  TypeErrorUnify term expected actual -> unlines
+  TypeErrorUnify term expected actual -> block TopDown
     [ "cannot unify expected type"
     , "  " <> show (untyped expected)
     , "with actual type"
     , "  " <> show (untyped actual)
     , "for term"
     , "  " <> show (untyped term) ]
-  TypeErrorUnifyTerms expected actual -> unlines
+  TypeErrorUnifyTerms expected actual -> block TopDown
     [ "cannot unify term"
     , "  " <> show (untyped expected)
     , "with term"
     , "  " <> show (untyped actual) ]
-  TypeErrorNotPair term ty -> unlines
+  TypeErrorNotPair term ty -> block TopDown
     [ "expected a cube product or dependent pair"
     , "but got type"
     , "  " <> show (untyped ty)
@@ -325,26 +324,26 @@ ppTypeError' = \case
         _          -> ""
     ]
 
-  TypeErrorUnexpectedLambda term ty -> unlines
+  TypeErrorUnexpectedLambda term ty -> block TopDown
     [ "unexpected lambda abstraction"
     , "  " <> show term
     , "when typechecking against a non-function type"
     , "  " <> show ty
     ]
-  TypeErrorUnexpectedPair term ty -> unlines
+  TypeErrorUnexpectedPair term ty -> block TopDown
     [ "unexpected pair"
     , "  " <> show term
     , "when typechecking against a type that is not a product or a dependent sum"
     , "  " <> show ty
     ]
-  TypeErrorUnexpectedRefl term ty -> unlines
+  TypeErrorUnexpectedRefl term ty -> block TopDown
     [ "unexpected refl"
     , "  " <> show term
     , "when typechecking against a type that is not an identity type"
     , "  " <> show ty
     ]
 
-  TypeErrorNotFunction term ty -> unlines
+  TypeErrorNotFunction term ty -> block TopDown
     [ "expected a function or extension type"
     , "but got type"
     , "  " <> show (untyped ty)
@@ -354,38 +353,38 @@ ppTypeError' = \case
         AppT _ty f _x -> "\nPerhaps the term\n  " <> show (untyped f) <> "\nis applied to too many arguments?"
         _ -> ""
     ]
-  TypeErrorCannotInferBareLambda term -> unlines
+  TypeErrorCannotInferBareLambda term -> block TopDown
     [ "cannot infer the type of the argument"
     , "in lambda abstraction"
     , "  " <> show term
     ]
-  TypeErrorCannotInferBareRefl term -> unlines
+  TypeErrorCannotInferBareRefl term -> block TopDown
     [ "cannot infer the type of term"
     , "  " <> show term
     ]
-  TypeErrorUndefined var -> unlines
+  TypeErrorUndefined var -> block TopDown
     [ "undefined variable: " <> show (Pure var :: Term') ]
-  TypeErrorTopeNotSatisfied topes tope -> unlines
+  TypeErrorTopeNotSatisfied topes tope -> block TopDown
     [ "local context is not included in (does not entail) the tope"
     , "  " <> show (untyped tope)
     , "in local context (normalised)"
     , intercalate "\n" (map ("  " <>) (map show topes))
     , intercalate "\n" (map ("  " <>) (map show (generateTopesForPoints (allTopePoints tope))))] -- FIXME: remove
-  TypeErrorTopesNotEquivalent expected actual -> unlines
+  TypeErrorTopesNotEquivalent expected actual -> block TopDown
     [ "expected tope"
     , "  " <> show (untyped expected)
     , "but got"
     , "  " <> show (untyped actual) ]
 
-  TypeErrorInvalidArgumentType argType argKind -> unlines
+  TypeErrorInvalidArgumentType argType argKind -> block TopDown
     [ "invalid function parameter type"
     , "  " <> show argType
     , "function parameter can be a cube, a shape, or a type"
     , "but given parameter type has type"
     , "  " <> show (untyped argKind)
     ]
 
-  TypeErrorDuplicateTopLevel previous lastName -> unlines
+  TypeErrorDuplicateTopLevel previous lastName -> block TopDown
     [ "duplicate top-level definition"
     , "  " <> ppVarIdentWithLocation lastName
     , "previous top-level definitions found at"
@@ -394,19 +393,19 @@ ppTypeError' = \case
       | name <- previous ]
     ]
 
-  TypeErrorUnusedVariable name type_ -> unlines
+  TypeErrorUnusedVariable name type_ -> block TopDown
     [ "unused variable"
     , "  " <> Rzk.printTree (getVarIdent name) <> " : " <> show (untyped type_)
     ]
 
-  TypeErrorUnusedUsedVariables vars name -> unlines
+  TypeErrorUnusedUsedVariables vars name -> block TopDown
     [ "unused variables"
     , "  " <> intercalate " " (map (Rzk.printTree . getVarIdent) vars)
     , "declared as used in definition of"
     , "  " <> Rzk.printTree (getVarIdent name)
     ]
 
-  TypeErrorImplicitAssumption (a, aType) name -> unlines
+  TypeErrorImplicitAssumption (a, aType) name -> block TopDown
     [ "implicit assumption"
     , "  " <> Rzk.printTree (getVarIdent a) <> " : " <> show (untyped aType)
     , "used in definition of"
@@ -416,6 +415,7 @@ ppTypeError' = \case
 ppTypeErrorInContext :: OutputDirection -> TypeErrorInContext VarIdent -> String
 ppTypeErrorInContext dir TypeErrorInContext{..} = block dir
   [ ppTypeError' typeErrorError
+  , ""
   , ppContext' dir typeErrorContext
   ]
 
@@ -813,6 +813,7 @@ abstractAssumption (var, VarInfo{..}) Decl{..} = Decl
     newDeclType = typeFunT varOrig varType Nothing (abstract var declType)
 
 data OutputDirection = TopDown | BottomUp
+  deriving (Eq)
 
 block :: OutputDirection -> [String] -> String
 block TopDown  = intercalate "\n"
@@ -824,39 +825,41 @@ namedBlock dir name lines_ = block dir $
   where
     indent = intercalate "\n" . (map ("  " ++)) . lines
 
-
 ppContext' :: OutputDirection -> Context VarIdent -> String
-ppContext' dir ctx@Context{..} = block dir
-  [ case location of
-      Just (LocationInfo (Just path) (Just lineNo)) ->
-        path <> " (line " <> show lineNo <> "):"
-      Just (LocationInfo (Just path) _) ->
-        path <> ":"
-      _  -> ""
-  , case currentCommand of
-      Just (Rzk.CommandDefine _loc name _vars _params _ty _term) ->
-        "  Error occurred when checking\n    #define " <> Rzk.printTree name
-      Just (Rzk.CommandPostulate _loc name _vars _params _ty ) ->
-        "  Error occurred when checking\n    #postulate " <> Rzk.printTree name
-      Just (Rzk.CommandCheck _loc term ty) ->
-        "  Error occurred when checking\n    " <> Rzk.printTree term <> " : " <> Rzk.printTree ty
-      Just (Rzk.CommandCompute _loc term) ->
-        "  Error occurred when computing\n    " <> Rzk.printTree term
-      Just (Rzk.CommandComputeNF _loc term) ->
-        "  Error occurred when computing NF for\n    " <> Rzk.printTree term
-      Just (Rzk.CommandComputeWHNF _loc term) ->
-        "  Error occurred when computing WHNF for\n    " <> Rzk.printTree term
-      Just (Rzk.CommandSetOption _loc optionName _optionValue) ->
-        "  Error occurred when trying to set option\n    #set-option " <> show optionName
-      Just command@Rzk.CommandUnsetOption{} ->
-        "  Error occurred when trying to unset option\n    " <> Rzk.printTree command
-      Just command@Rzk.CommandAssume{} ->
-        "  Error occurred when checking assumption\n    " <> Rzk.printTree command
-      Just (Rzk.CommandSection _loc name) ->
-        "  Error occurred when checking\n    #section " <> Rzk.printTree name
-      Just (Rzk.CommandSectionEnd _loc name) ->
-        "  Error occurred when checking\n    #end " <> Rzk.printTree name
-      Nothing -> "  Error occurred outside of any command!"
+ppContext' dir ctx@Context{..} = block dir $ dropWhile null
+  [ block TopDown
+    [ case location of
+        _ | dir == TopDown -> "" -- FIXME
+        Just (LocationInfo (Just path) (Just lineNo)) ->
+          path <> " (line " <> show lineNo <> "):"
+        Just (LocationInfo (Just path) _) ->
+          path <> ":"
+        _  -> ""
+    , case currentCommand of
+        Just (Rzk.CommandDefine _loc name _vars _params _ty _term) ->
+          "  Error occurred when checking\n    #define " <> Rzk.printTree name
+        Just (Rzk.CommandPostulate _loc name _vars _params _ty ) ->
+          "  Error occurred when checking\n    #postulate " <> Rzk.printTree name
+        Just (Rzk.CommandCheck _loc term ty) ->
+          "  Error occurred when checking\n    " <> Rzk.printTree term <> " : " <> Rzk.printTree ty
+        Just (Rzk.CommandCompute _loc term) ->
+          "  Error occurred when computing\n    " <> Rzk.printTree term
+        Just (Rzk.CommandComputeNF _loc term) ->
+          "  Error occurred when computing NF for\n    " <> Rzk.printTree term
+        Just (Rzk.CommandComputeWHNF _loc term) ->
+          "  Error occurred when computing WHNF for\n    " <> Rzk.printTree term
+        Just (Rzk.CommandSetOption _loc optionName _optionValue) ->
+          "  Error occurred when trying to set option\n    #set-option " <> show optionName
+        Just command@Rzk.CommandUnsetOption{} ->
+          "  Error occurred when trying to unset option\n    " <> Rzk.printTree command
+        Just command@Rzk.CommandAssume{} ->
+          "  Error occurred when checking assumption\n    " <> Rzk.printTree command
+        Just (Rzk.CommandSection _loc name) ->
+          "  Error occurred when checking\n    #section " <> Rzk.printTree name
+        Just (Rzk.CommandSectionEnd _loc name) ->
+          "  Error occurred when checking\n    #end " <> Rzk.printTree name
+        Nothing -> "  Error occurred outside of any command!"
+    ]
   , ""
   , case filter (/= topeTopT) localTopes of
       [] -> "Local tope context is unrestricted (⊤)."