rzk 0.4.0 → 0.4.1

raw patch · 4 files changed

+52/−23 lines, 4 filesdep +optparse-generic

Dependencies added: optparse-generic

Files

• ChangeLog.md +11/−0
• rzk.cabal +5/−4
• src/Rzk/Main.hs +35/−18
• src/Rzk/TypeCheck.hs +1/−1

@@ -6,6 +6,17 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.4.1 — 2022-06-16++This is version contains minor changes, primarily in tools around rzk:++- Add `rzk version` command (see [f1709dc7]( https://github.com/fizruk/rzk/commit/f1709dc7 ));+- Add action to release binaries (see [9286afae]( https://github.com/fizruk/rzk/commit/9286afae ));+- Automate SVG rendering in MkDocs (see [#49]( https://github.com/fizruk/rzk/pull/49 ));+- Read `stdin` when no filepaths are given (see [936c15a3]( https://github.com/fizruk/rzk/commit/936c15a3 ));+- Add Pygments highlighting (see [01c2a017]( https://github.com/fizruk/rzk/commit/01c2a017 ), [cbd656cc]( https://github.com/fizruk/rzk/commit/cbd656cc ), [5220ddf9]( https://github.com/fizruk/rzk/commit/5220ddf9 ), [142ec003]( https://github.com/fizruk/rzk/commit/142ec003 ), [5c7425f2]( https://github.com/fizruk/rzk/commit/5c7425f2 ));+- Update HighlightJS config for rzk v0.4.0 (see [171ee63f]( https://github.com/fizruk/rzk/commit/171ee63f ));+ ## v0.4.0 — 2022-05-18  This version introduces sections and variables. The feature is similar to <a href="https://coq.inria.fr/refman/language/core/assumptions.html#coq:cmd.Variable" target="_blank">`Variable` command in Coq</a>. An important difference, however, is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental.

@@ -1,13 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.35.1. -- -- see: https://github.com/sol/hpack------ hash: 7855530fcdfd2a28c4ea3654677ed2d18f83d419f5d1c173f4bb44a915464c06  name:           rzk-version:        0.4.0+version:        0.4.1 synopsis:       An experimental proof assistant for synthetic ∞-categories description:    Please see the README on GitHub at <https://github.com/fizruk/rzk#readme> category:       Dependent Types@@ -51,6 +49,7 @@     , base >=4.7 && <5     , bifunctors     , mtl+    , optparse-generic     , template-haskell   default-language: Haskell2010 @@ -66,6 +65,7 @@     , base >=4.7 && <5     , bifunctors     , mtl+    , optparse-generic     , rzk     , template-haskell   default-language: Haskell2010@@ -83,6 +83,7 @@     , base >=4.7 && <5     , bifunctors     , mtl+    , optparse-generic     , rzk     , template-haskell   default-language: Haskell2010

@@ -1,18 +1,37 @@+{-# LANGUAGE DeriveAnyClass    #-}+{-# LANGUAGE DeriveGeneric     #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE OverloadedStrings #-} module Rzk.Main where  import           Control.Monad       (forM)-import           System.Environment  (getArgs)+import           Data.Version        (showVersion)+import           Options.Generic import           System.Exit         (exitFailure)  import qualified Language.Rzk.Syntax as Rzk+import           Paths_rzk           (version) import           Rzk.TypeCheck +data Command+  = Typecheck [FilePath]+  | Version+  deriving (Generic, Show, ParseRecord)+ main :: IO ()-main = do-  args <- getArgs-  case args of-    "typecheck" : paths -> do-      modules <- forM paths $ \path -> do+main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case+  Typecheck paths -> do+    modules <- case paths of+      -- if no paths are given — read from stdin+      [] -> do+        result <- Rzk.parseModule <$> getContents+        case result of+          Left err -> do+            putStrLn ("An error occurred when parsing stdin")+            error err+          Right rzkModule -> return [("<stdin>", rzkModule)]+      -- otherwise — parse all given files in given order+      _ -> forM paths $ \path -> do         putStrLn ("Loading file " <> path)         result <- Rzk.parseModule <$> readFile path         case result of@@ -20,19 +39,17 @@             putStrLn ("An error occurred when parsing file " <> path)             error err           Right rzkModule -> return (path, rzkModule)-      case defaultTypeCheck (typecheckModulesWithLocation modules) of-        Left err -> do-          putStrLn "An error occurred when typechecking!"-          putStrLn $ unlines-            [ "Type Error:"-            , ppTypeErrorInScopedContext' err-            ]-          exitFailure-        Right () -> putStrLn "Everything is ok!"-    _ -> ppUsage+    case defaultTypeCheck (typecheckModulesWithLocation modules) of+      Left err -> do+        putStrLn "An error occurred when typechecking!"+        putStrLn $ unlines+          [ "Type Error:"+          , ppTypeErrorInScopedContext' err+          ]+        exitFailure+      Right () -> putStrLn "Everything is ok!" -ppUsage :: IO ()-ppUsage = putStrLn "rzk typecheck FILE"+  Version -> putStrLn (showVersion version)  typecheckString :: String -> Either String String typecheckString moduleString = do

@@ -2936,7 +2936,7 @@   -> (String -> Maybe RenderObjectData)   -> String renderCube camera rotY renderDataOf' = unlines $ filter (not . null)-  [ "<svg class=\"zoom\" style=\"float: right\" viewBox=\"-175 -200 350 375\" width=\"150\" height=\"150\">"+  [ "<svg class=\"rzk-render\" viewBox=\"-175 -200 350 375\" width=\"150\" height=\"150\">"   , intercalate "\n"       [ "  <path d=\"M " <> show x1 <> " " <> show y1                 <> " L " <> show x2 <> " " <> show y2