diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -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 `Variable` command in Coq. 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.
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -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
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
diff --git a/src/Rzk/Main.hs b/src/Rzk/Main.hs
--- a/src/Rzk/Main.hs
+++ b/src/Rzk/Main.hs
@@ -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 [("", 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
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -2936,7 +2936,7 @@
-> (String -> Maybe RenderObjectData)
-> String
renderCube camera rotY renderDataOf' = unlines $ filter (not . null)
- [ "