Merge branch 'release-v0.3.0'

* release-v0.3.0: (26 commits) Update changelog link Update changelog Bump version and update changelog Update demo image in README Fix #33 (missing check), limit full label length to 30 Scale SVG x1.5 by default Update changelog Add docs for rendering Fix empty tope context, change colors for rendering Fix some labels Update changelog Improve rendering Add labels for edges and faces Add render option, limit label length Use black for known params, simplify some labels Fix rendering for topes, add rendering for types Refactor rendering, support curried functions Render subshapes in 1D, 2D, and 3D Fix external links and Ulrik's name in the docs Introduce RenderObjectData ...
rzk-lang · Apr 28, 2023 · e31c70a · e31c70a
2 parents b5628de + 4a71bf2
commit e31c70a
Show file tree

Hide file tree

Showing 13 changed files with 1,126 additions and 252 deletions.
diff --git a/README.md b/README.md
@@ -6,7 +6,7 @@
 
 An experimental proof assistant for synthetic ∞-categories.
 
-[![Early prototype demo.](images/split-demo.png)](https://fizruk.github.io/rzk/)
+[![Early prototype demo.](images/split-demo-render.png)](https://fizruk.github.io/rzk/)
 
 ## About this project
 

diff --git a/docs/docs/related/sHoTT.md b/docs/docs/related/sHoTT.md
@@ -1,11 +1,11 @@
 # sHoTT
 
-[sHoTT](https://github.com/fizruk/sHoTT) is a formalisation project for simplicial HoTT and ∞-categories.
+<a href="https://github.com/fizruk/sHoTT" target="_blank">sHoTT</a> is a formalisation project for simplicial HoTT and ∞-categories.
 
-The project is a fork of https://github.com/emilyriehl/yoneda,
+The project is a fork of <a href="https://github.com/emilyriehl/yoneda" target="_blank">https://github.com/emilyriehl/yoneda</a>,
 with a goal to grow and eventually include various
 formalisations for HoTT (e.g. HoTT book),
-synthetic fibered ∞-categories from the work of Ulrich Buchholtz and Jonathan Weinberger, variations of cubical type theories, etc.
+synthetic fibered ∞-categories from the work of Ulrik Buchholtz and Jonathan Weinberger, variations of cubical type theories, etc.
 
 See more details in the documentation of the project at
-[https://github.com/fizruk/sHoTT](https://github.com/fizruk/sHoTT).
+<a href="https://github.com/fizruk/sHoTT" target="_blank">https://github.com/fizruk/sHoTT</a>.
diff --git a/docs/docs/related/simple-topes.md b/docs/docs/related/simple-topes.md
@@ -1,6 +1,6 @@
 # simple-topes
 
-[simple-topes](https://github.com/fizruk/simple-topes) is a playground theorem prover project for type theory with shapes that allows user-defined cubes and topes. Once stable, the project will be merged into `rzk`, extending it to a proof assistant for type theory with (user-defined) cubes, topes, and shapes.
+<a href="https://github.com/fizruk/simple-topes" target="_blank">simple-topes</a> is a playground theorem prover project for type theory with shapes that allows user-defined cubes and topes. Once stable, the project will be merged into `rzk`, extending it to a proof assistant for type theory with (user-defined) cubes, topes, and shapes.
 
 See more details in the documentation of the project at
-[https://github.com/fizruk/simple-topes](https://github.com/fizruk/simple-topes).
+<a href="https://github.com/fizruk/simple-topes" target="_blank">https://github.com/fizruk/simple-topes</a>.
diff --git a/docs/docs/rzk-1/introduction.md b/docs/docs/rzk-1/introduction.md
@@ -3,7 +3,7 @@
 !!! warning "Work-in-progress"
     The documentation is not yet up-to-date with all
     the changes introduced in `rzk-0.2.0`. <br>
-    See [`rzk` changelog](https://github.com/fizruk/rzk/blob/release-v0.2.0/rzk/ChangeLog.md#v020---2022-04-20) for more details.
+    See [`rzk` changelog](https://github.com/fizruk/rzk/blob/release-v0.3.0/rzk/ChangeLog.md#v020---2022-04-20) for more details.
 
 `rzk` is an experimental proof assistant for synthetic ∞-categories.
 `rzk-1` is an early version of the language supported by `rzk`.

diff --git a/docs/docs/rzk-1/render.md b/docs/docs/rzk-1/render.md
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
@@ -4,6 +4,7 @@ nav:
     - About: index.md
   - rzk-1 Language:
     - Introduction: rzk-1/introduction.md
+    - Rendering Diagrams: rzk-1/render.md
     - Weak tope disjunction elimination: rzk-1/recId.md
   - Tools:
     - IDE support: tools/ide.md

diff --git a/images/split-demo-render.png b/images/split-demo-render.png
diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md
@@ -6,6 +6,25 @@ 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.3.0 — 2022-04-28
+
+This version introduces an experimental feature for generating visualisations for simplicial terms in SVG.
+To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):
+
+```rzk
+#set-option "render" = "svg"  -- enable rendering in SVG
+```
+
+Minor changes:
+
+- Exit with non-zero code upon a type error (see b135c4fb)
+- Fix external links and some typos in the documentation
+
+Fixes:
+
+- Fixed an issue with tope solver when context was empty (see 6196af9e);
+- Fixed #33 (missing coherence check for restricted types).
+
 ## v0.2.0 - 2022-04-20
 
 This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0.

diff --git a/rzk/debug.txt b/rzk/debug.txt
diff --git a/rzk/package.yaml b/rzk/package.yaml
@@ -1,5 +1,5 @@
 name:                rzk
-version:             0.2.0
+version:             0.3.0
 github:              "fizruk/rzk"
 license:             BSD3
 author:              "Nikolai Kudasov"

diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
@@ -4,10 +4,10 @@ cabal-version: 1.12
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: e731bc697ba22a070995646c30c641e0805466b3cabb2fdf377ce74e07985a32
+-- hash: 7855530fcdfd2a28c4ea3654677ed2d18f83d419f5d1c173f4bb44a915464c06
 
 name:           rzk
-version:        0.2.0
+version:        0.3.0
 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

diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
@@ -1,5 +1,6 @@
 module Rzk.Main where
 
+import System.Exit (exitFailure)
 import System.Environment (getArgs)
 import Control.Monad (forM)
 
@@ -22,11 +23,11 @@ main = do
       case defaultTypeCheck (typecheckModulesWithLocation modules) of
         Left err -> do
           putStrLn "An error occurred when typechecking!"
-          putStrLn "Rendering type error... (this may take a few seconds)"
           putStrLn $ unlines
             [ "Type Error:"
             , ppTypeErrorInScopedContext' err
             ]
+          exitFailure
         Right () -> putStrLn "Everything is ok!"
     _ -> ppUsage