From 613a5a16b222c8e8cac05a5bff912f3c97eaa4d5 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Thu, 7 Sep 2023 17:08:23 +0300
Subject: [PATCH 01/16] Configure mkdocs-plugin-rzk

---
 docs/mkdocs.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
index d42c82161..18986be48 100644
--- a/docs/mkdocs.yml
+++ b/docs/mkdocs.yml
@@ -113,5 +113,7 @@ extra:
 
 plugins:
   - mike
-  - rzk
+  - rzk:
+      render_svg: true
+      anchor_definitions: true
   - search

From f2e79e0facfabe6d8f66f689fe5fbe29aec1e0c7 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Thu, 7 Sep 2023 17:10:37 +0300
Subject: [PATCH 02/16] Add alex and happy to dependencies

---
 rzk/package.yaml |  4 ++++
 rzk/rzk.cabal    | 12 ++++++++++++
 rzk/rzk.nix      | 13 ++++++++-----
 3 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/rzk/package.yaml b/rzk/package.yaml
index 164ac8643..1d2b8bd85 100644
--- a/rzk/package.yaml
+++ b/rzk/package.yaml
@@ -18,6 +18,10 @@ category: Dependent Types # same as Agda
 # common to point users to the README.md file.
 description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 
+build-tools:
+  - alex
+  - happy
+
 dependencies:
   - array
   - aeson
diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
index 5d95c9776..074464ef4 100644
--- a/rzk/rzk.cabal
+++ b/rzk/rzk.cabal
@@ -46,6 +46,9 @@ library
   hs-source-dirs:
       src
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+  build-tools:
+      alex
+    , happy
   build-depends:
       aeson
     , array
@@ -65,6 +68,9 @@ executable rzk
   hs-source-dirs:
       app
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-tools:
+      alex
+    , happy
   build-depends:
       aeson
     , array
@@ -84,6 +90,9 @@ test-suite doctests
   hs-source-dirs:
       test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+  build-tools:
+      alex
+    , happy
   build-depends:
       Glob
     , QuickCheck
@@ -107,6 +116,9 @@ test-suite rzk-test
   hs-source-dirs:
       test
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-tools:
+      alex
+    , happy
   build-depends:
       aeson
     , array
diff --git a/rzk/rzk.nix b/rzk/rzk.nix
index a0c9df368..0a095d0b3 100644
--- a/rzk/rzk.nix
+++ b/rzk/rzk.nix
@@ -1,5 +1,6 @@
-{ mkDerivation, aeson, array, base, bifunctors, bytestring, hpack
-, lib, mtl, optparse-generic, template-haskell, text
+{ mkDerivation, aeson, alex, array, base, bifunctors, bytestring
+, doctest, Glob, happy, hpack, lib, mtl, optparse-generic
+, QuickCheck, template-haskell, text
 }:
 mkDerivation {
   pname = "rzk";
@@ -11,15 +12,17 @@ mkDerivation {
     aeson array base bifunctors bytestring mtl optparse-generic
     template-haskell text
   ];
-  libraryToolDepends = [ hpack ];
+  libraryToolDepends = [ alex happy hpack ];
   executableHaskellDepends = [
     aeson array base bifunctors bytestring mtl optparse-generic
     template-haskell text
   ];
+  executableToolDepends = [ alex happy ];
   testHaskellDepends = [
-    aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text
+    aeson array base bifunctors bytestring doctest Glob mtl
+    optparse-generic QuickCheck template-haskell text
   ];
+  testToolDepends = [ alex happy ];
   prePatch = "hpack";
   homepage = "https://github.com/rzk-lang/rzk#readme";
   description = "An experimental proof assistant for synthetic ∞-categories";

From 828f7e4c9a649028f9b1ed4a3c89a2052cadfb88 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <fizruk@users.noreply.github.com>
Date: Fri, 15 Sep 2023 15:49:08 +0300
Subject: [PATCH 03/16] Update site_name in mkdocs.yml

Thanks to @jonweinb for noticing!
---
 docs/mkdocs.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
index 18986be48..c45d21394 100644
--- a/docs/mkdocs.yml
+++ b/docs/mkdocs.yml
@@ -1,4 +1,4 @@
-site_name: "rzk: an experimental proof assistant for syntheric ∞-categories"
+site_name: "rzk: an experimental proof assistant for synthetic ∞-categories"
 repo_url: https://github.com/rzk-lang/rzk
 repo_name: rzk-lang/rzk
 edit_uri: edit/develop/docs/docs/

From 6bd45fdc3d9a71c2f52b033a516ed25bb053d7ed Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Mon, 18 Sep 2023 20:50:35 +0200
Subject: [PATCH 04/16] Install and use the "with-utf8" package

To support other locales on systems that do not default to UTF-8
---
 rzk/package.yaml    | 1 +
 rzk/rzk.cabal       | 6 +++++-
 rzk/src/Rzk/Main.hs | 4 ++--
 stack.yaml          | 3 ++-
 stack.yaml.lock     | 9 ++++++++-
 5 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/rzk/package.yaml b/rzk/package.yaml
index 1d2b8bd85..d5465f5c7 100644
--- a/rzk/package.yaml
+++ b/rzk/package.yaml
@@ -32,6 +32,7 @@ dependencies:
   - template-haskell
   - text
   - optparse-generic
+  - with-utf8
 
 ghc-options:
   - -Wall
diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
index 074464ef4..3fda2e19b 100644
--- a/rzk/rzk.cabal
+++ b/rzk/rzk.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.35.1.
+-- This file has been generated from package.yaml by hpack version 0.35.2.
 --
 -- see: https://github.com/sol/hpack
 
@@ -59,6 +59,7 @@ library
     , optparse-generic
     , template-haskell
     , text
+    , with-utf8
   default-language: Haskell2010
 
 executable rzk
@@ -82,6 +83,7 @@ executable rzk
     , rzk
     , template-haskell
     , text
+    , with-utf8
   default-language: Haskell2010
 
 test-suite doctests
@@ -106,6 +108,7 @@ test-suite doctests
     , optparse-generic
     , template-haskell
     , text
+    , with-utf8
   default-language: Haskell2010
 
 test-suite rzk-test
@@ -130,4 +133,5 @@ test-suite rzk-test
     , rzk
     , template-haskell
     , text
+    , with-utf8
   default-language: Haskell2010
diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
index ee6513686..621331587 100644
--- a/rzk/src/Rzk/Main.hs
+++ b/rzk/src/Rzk/Main.hs
@@ -10,6 +10,7 @@ import qualified Data.ByteString.Lazy.Char8   as ByteString
 import           Data.Version                 (showVersion)
 import           Options.Generic
 import           System.Exit                  (exitFailure)
+import           Main.Utf8                    (withUtf8)
 
 import qualified Language.Rzk.Syntax          as Rzk
 import           Language.Rzk.VSCode.Tokenize (tokenizeModule)
@@ -23,7 +24,7 @@ data Command
   deriving (Generic, Show, ParseRecord)
 
 main :: IO ()
-main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case
+main = withUtf8 $ getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case
   Typecheck paths -> do
     modules <- parseRzkFilesOrStdin paths
     case defaultTypeCheck (typecheckModulesWithLocation modules) of
@@ -80,4 +81,3 @@ typecheckString moduleString = do
         ]
       ]
     Right _ -> pure "Everything is ok!"
-
diff --git a/stack.yaml b/stack.yaml
index 440b582fc..fd1d578d8 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -39,7 +39,8 @@ packages:
 # - git: https://github.com/commercialhaskell/stack.git
 #   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
 #
-# extra-deps: []
+extra-deps:
+- with-utf8-1.0.2.4
 
 # Override default flag values for local packages and extra-deps
 # flags: {}
diff --git a/stack.yaml.lock b/stack.yaml.lock
index 58dd3e438..b2d29558a 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -3,7 +3,14 @@
 # For more information, please see the documentation at:
 #   https://docs.haskellstack.org/en/stable/lock_files
 
-packages: []
+packages:
+- completed:
+    hackage: with-utf8-1.0.2.4@sha256:c47c077769883cc54a18ea0a6567c5b49fd2ab708f796ec92b8ad3c8b60a8b09,2974
+    pantry-tree:
+      sha256: af0f438235d84ce1ea04f1e8ad566d1aeeb287515adae3d2843c309f4d031651
+      size: 1051
+  original:
+    hackage: with-utf8-1.0.2.4
 snapshots:
 - completed:
     sha256: cbf721fafa21237e4999d83cfd27137f440ae0e3032ff18fa96e8148d9bf5ce1

From 559dff6b09348797c9f8094f23d89f3308facf78 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 18 Sep 2023 21:00:15 +0200
Subject: [PATCH 05/16] Update rzk.nix

---
 rzk/rzk.nix | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/rzk/rzk.nix b/rzk/rzk.nix
index 0a095d0b3..2c19d1d72 100644
--- a/rzk/rzk.nix
+++ b/rzk/rzk.nix
@@ -1,6 +1,6 @@
 { mkDerivation, aeson, alex, array, base, bifunctors, bytestring
 , doctest, Glob, happy, hpack, lib, mtl, optparse-generic
-, QuickCheck, template-haskell, text
+, QuickCheck, template-haskell, text, with-utf8
 }:
 mkDerivation {
   pname = "rzk";
@@ -10,17 +10,17 @@ mkDerivation {
   isExecutable = true;
   libraryHaskellDepends = [
     aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text
+    template-haskell text with-utf8
   ];
   libraryToolDepends = [ alex happy hpack ];
   executableHaskellDepends = [
     aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text
+    template-haskell text with-utf8
   ];
   executableToolDepends = [ alex happy ];
   testHaskellDepends = [
     aeson array base bifunctors bytestring doctest Glob mtl
-    optparse-generic QuickCheck template-haskell text
+    optparse-generic QuickCheck template-haskell text with-utf8
   ];
   testToolDepends = [ alex happy ];
   prePatch = "hpack";

From 657742f97ac3813f4664d5de8bbcbd00e9177e8d Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 18 Sep 2023 21:32:40 +0200
Subject: [PATCH 06/16] Conditionally depend on with-utf8, only for executable

---
 rzk/app/Main.hs     |  3 ++-
 rzk/package.yaml    |  5 ++++-
 rzk/rzk.cabal       |  7 +++----
 rzk/rzk.ghcjs.nix   | 30 ++++++++++++++++++++++++++++++
 rzk/rzk.nix         |  4 ++--
 rzk/src/Rzk/Main.hs |  3 +--
 try-rzk/default.nix |  2 +-
 7 files changed, 43 insertions(+), 11 deletions(-)
 create mode 100644 rzk/rzk.ghcjs.nix

diff --git a/rzk/app/Main.hs b/rzk/app/Main.hs
index b9d762ac8..e8ded814d 100644
--- a/rzk/app/Main.hs
+++ b/rzk/app/Main.hs
@@ -1,6 +1,7 @@
 module Main (main) where
 
+import           Main.Utf8 (withUtf8)
 import qualified Rzk.Main
 
 main :: IO ()
-main = Rzk.Main.main
+main = withUtf8 Rzk.Main.main
diff --git a/rzk/package.yaml b/rzk/package.yaml
index d5465f5c7..dd8cb3e0c 100644
--- a/rzk/package.yaml
+++ b/rzk/package.yaml
@@ -32,7 +32,6 @@ dependencies:
   - template-haskell
   - text
   - optparse-generic
-  - with-utf8
 
 ghc-options:
   - -Wall
@@ -64,6 +63,10 @@ executables:
       - -with-rtsopts=-N
     dependencies:
       - rzk
+    when:
+      - condition: "!impl(ghcjs)"
+        dependencies:
+          - with-utf8
 
 tests:
   rzk-test:
diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
index 3fda2e19b..1b0a6bfda 100644
--- a/rzk/rzk.cabal
+++ b/rzk/rzk.cabal
@@ -59,7 +59,6 @@ library
     , optparse-generic
     , template-haskell
     , text
-    , with-utf8
   default-language: Haskell2010
 
 executable rzk
@@ -83,8 +82,10 @@ executable rzk
     , rzk
     , template-haskell
     , text
-    , with-utf8
   default-language: Haskell2010
+  if !impl(ghcjs)
+    build-depends:
+        with-utf8
 
 test-suite doctests
   type: exitcode-stdio-1.0
@@ -108,7 +109,6 @@ test-suite doctests
     , optparse-generic
     , template-haskell
     , text
-    , with-utf8
   default-language: Haskell2010
 
 test-suite rzk-test
@@ -133,5 +133,4 @@ test-suite rzk-test
     , rzk
     , template-haskell
     , text
-    , with-utf8
   default-language: Haskell2010
diff --git a/rzk/rzk.ghcjs.nix b/rzk/rzk.ghcjs.nix
new file mode 100644
index 000000000..0a095d0b3
--- /dev/null
+++ b/rzk/rzk.ghcjs.nix
@@ -0,0 +1,30 @@
+{ mkDerivation, aeson, alex, array, base, bifunctors, bytestring
+, doctest, Glob, happy, hpack, lib, mtl, optparse-generic
+, QuickCheck, template-haskell, text
+}:
+mkDerivation {
+  pname = "rzk";
+  version = "0.5.4";
+  src = ./.;
+  isLibrary = true;
+  isExecutable = true;
+  libraryHaskellDepends = [
+    aeson array base bifunctors bytestring mtl optparse-generic
+    template-haskell text
+  ];
+  libraryToolDepends = [ alex happy hpack ];
+  executableHaskellDepends = [
+    aeson array base bifunctors bytestring mtl optparse-generic
+    template-haskell text
+  ];
+  executableToolDepends = [ alex happy ];
+  testHaskellDepends = [
+    aeson array base bifunctors bytestring doctest Glob mtl
+    optparse-generic QuickCheck template-haskell text
+  ];
+  testToolDepends = [ alex happy ];
+  prePatch = "hpack";
+  homepage = "https://github.com/rzk-lang/rzk#readme";
+  description = "An experimental proof assistant for synthetic ∞-categories";
+  license = lib.licenses.bsd3;
+}
diff --git a/rzk/rzk.nix b/rzk/rzk.nix
index 2c19d1d72..6526f4933 100644
--- a/rzk/rzk.nix
+++ b/rzk/rzk.nix
@@ -10,7 +10,7 @@ mkDerivation {
   isExecutable = true;
   libraryHaskellDepends = [
     aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text with-utf8
+    template-haskell text
   ];
   libraryToolDepends = [ alex happy hpack ];
   executableHaskellDepends = [
@@ -20,7 +20,7 @@ mkDerivation {
   executableToolDepends = [ alex happy ];
   testHaskellDepends = [
     aeson array base bifunctors bytestring doctest Glob mtl
-    optparse-generic QuickCheck template-haskell text with-utf8
+    optparse-generic QuickCheck template-haskell text
   ];
   testToolDepends = [ alex happy ];
   prePatch = "hpack";
diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
index 621331587..aeecc55e6 100644
--- a/rzk/src/Rzk/Main.hs
+++ b/rzk/src/Rzk/Main.hs
@@ -10,7 +10,6 @@ import qualified Data.ByteString.Lazy.Char8   as ByteString
 import           Data.Version                 (showVersion)
 import           Options.Generic
 import           System.Exit                  (exitFailure)
-import           Main.Utf8                    (withUtf8)
 
 import qualified Language.Rzk.Syntax          as Rzk
 import           Language.Rzk.VSCode.Tokenize (tokenizeModule)
@@ -24,7 +23,7 @@ data Command
   deriving (Generic, Show, ParseRecord)
 
 main :: IO ()
-main = withUtf8 $ getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case
+main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case
   Typecheck paths -> do
     modules <- parseRzkFilesOrStdin paths
     case defaultTypeCheck (typecheckModulesWithLocation modules) of
diff --git a/try-rzk/default.nix b/try-rzk/default.nix
index 55570b513..942bd91d6 100644
--- a/try-rzk/default.nix
+++ b/try-rzk/default.nix
@@ -2,5 +2,5 @@ with (import (builtins.fetchTarball {
   url = "https://github.com/dmjio/miso/archive/refs/tags/1.8.3.tar.gz";
   /* sha256 = "1yb9yvc0ln4yn1jk2k5kwwa1s32310abawz40yd8cqqkm1z7w6wg"; */
 }) {});
-let rzk-local = pkgs.haskell.packages.ghcjs.callPackage ../rzk/rzk.nix { };
+let rzk-local = pkgs.haskell.packages.ghcjs.callPackage ../rzk/rzk.ghcjs.nix { };
 in pkgs.haskell.packages.ghcjs.callCabal2nix "try-rzk" ./. { rzk = rzk-local; }

From 73a00e44589088dcf860599d65925392a80b0634 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 18 Sep 2023 21:42:01 +0200
Subject: [PATCH 07/16] Do not use hpack for the GHCJS build

---
 rzk/rzk.ghcjs.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rzk/rzk.ghcjs.nix b/rzk/rzk.ghcjs.nix
index 0a095d0b3..9ba47a4a4 100644
--- a/rzk/rzk.ghcjs.nix
+++ b/rzk/rzk.ghcjs.nix
@@ -23,7 +23,7 @@ mkDerivation {
     optparse-generic QuickCheck template-haskell text
   ];
   testToolDepends = [ alex happy ];
-  prePatch = "hpack";
+  /* prePatch = "hpack"; */
   homepage = "https://github.com/rzk-lang/rzk#readme";
   description = "An experimental proof assistant for synthetic ∞-categories";
   license = lib.licenses.bsd3;

From e9df2691ef79a0827b4d1a9c77ef2070546b4b96 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 18 Sep 2023 21:46:20 +0200
Subject: [PATCH 08/16] Remove hpack and with-utf8 from nix files completely

---
 rzk/rzk.ghcjs.nix   | 30 ------------------------------
 rzk/rzk.nix         |  6 +++---
 try-rzk/default.nix |  2 +-
 3 files changed, 4 insertions(+), 34 deletions(-)
 delete mode 100644 rzk/rzk.ghcjs.nix

diff --git a/rzk/rzk.ghcjs.nix b/rzk/rzk.ghcjs.nix
deleted file mode 100644
index 9ba47a4a4..000000000
--- a/rzk/rzk.ghcjs.nix
+++ /dev/null
@@ -1,30 +0,0 @@
-{ mkDerivation, aeson, alex, array, base, bifunctors, bytestring
-, doctest, Glob, happy, hpack, lib, mtl, optparse-generic
-, QuickCheck, template-haskell, text
-}:
-mkDerivation {
-  pname = "rzk";
-  version = "0.5.4";
-  src = ./.;
-  isLibrary = true;
-  isExecutable = true;
-  libraryHaskellDepends = [
-    aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text
-  ];
-  libraryToolDepends = [ alex happy hpack ];
-  executableHaskellDepends = [
-    aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text
-  ];
-  executableToolDepends = [ alex happy ];
-  testHaskellDepends = [
-    aeson array base bifunctors bytestring doctest Glob mtl
-    optparse-generic QuickCheck template-haskell text
-  ];
-  testToolDepends = [ alex happy ];
-  /* prePatch = "hpack"; */
-  homepage = "https://github.com/rzk-lang/rzk#readme";
-  description = "An experimental proof assistant for synthetic ∞-categories";
-  license = lib.licenses.bsd3;
-}
diff --git a/rzk/rzk.nix b/rzk/rzk.nix
index 6526f4933..9ba47a4a4 100644
--- a/rzk/rzk.nix
+++ b/rzk/rzk.nix
@@ -1,6 +1,6 @@
 { mkDerivation, aeson, alex, array, base, bifunctors, bytestring
 , doctest, Glob, happy, hpack, lib, mtl, optparse-generic
-, QuickCheck, template-haskell, text, with-utf8
+, QuickCheck, template-haskell, text
 }:
 mkDerivation {
   pname = "rzk";
@@ -15,7 +15,7 @@ mkDerivation {
   libraryToolDepends = [ alex happy hpack ];
   executableHaskellDepends = [
     aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text with-utf8
+    template-haskell text
   ];
   executableToolDepends = [ alex happy ];
   testHaskellDepends = [
@@ -23,7 +23,7 @@ mkDerivation {
     optparse-generic QuickCheck template-haskell text
   ];
   testToolDepends = [ alex happy ];
-  prePatch = "hpack";
+  /* prePatch = "hpack"; */
   homepage = "https://github.com/rzk-lang/rzk#readme";
   description = "An experimental proof assistant for synthetic ∞-categories";
   license = lib.licenses.bsd3;
diff --git a/try-rzk/default.nix b/try-rzk/default.nix
index 942bd91d6..55570b513 100644
--- a/try-rzk/default.nix
+++ b/try-rzk/default.nix
@@ -2,5 +2,5 @@ with (import (builtins.fetchTarball {
   url = "https://github.com/dmjio/miso/archive/refs/tags/1.8.3.tar.gz";
   /* sha256 = "1yb9yvc0ln4yn1jk2k5kwwa1s32310abawz40yd8cqqkm1z7w6wg"; */
 }) {});
-let rzk-local = pkgs.haskell.packages.ghcjs.callPackage ../rzk/rzk.ghcjs.nix { };
+let rzk-local = pkgs.haskell.packages.ghcjs.callPackage ../rzk/rzk.nix { };
 in pkgs.haskell.packages.ghcjs.callCabal2nix "try-rzk" ./. { rzk = rzk-local; }

From 99b489a3e85441589ba6a366bc7b529a67d47bbc Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 18 Sep 2023 21:53:27 +0200
Subject: [PATCH 09/16] Do not remove rzk.cabal when building with GHCJS

---
 .github/workflows/ghcjs.yml | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
index 38df74136..c4bd2d0f7 100644
--- a/.github/workflows/ghcjs.yml
+++ b/.github/workflows/ghcjs.yml
@@ -2,21 +2,21 @@ name: Build with GHCJS and Deploy to GitHub Pages
 
 on:
   push:
-    branches: [ main, develop ]
-    tags: [ v* ]
+    branches: [main, develop]
+    tags: [v*]
     paths:
       - .github/workflows/ghcjs.yml
       - rzk/**
       - try-rzk/**
       - stack.yaml
   pull_request:
-    branches: [ main, develop ]
+    branches: [main, develop]
     paths:
       - rzk/**
       - try-rzk/**
       - stack.yaml
 
-  workflow_dispatch:  # allow triggering this workflow manually
+  workflow_dispatch: # allow triggering this workflow manually
 
 permissions:
   contents: write
@@ -35,7 +35,7 @@ jobs:
             substituters = https://cache.nixos.org/ https://cache.iog.io https://nix-community.cachix.org https://miso-haskell.cachix.org
             trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= nix-community.cachix.org-1:mB9FSh9qf2dCimDSUo8Zy7bkq5CX+/rkCWyvRCYg3Fs= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= miso-haskell.cachix.org-1:6N2DooyFlZOHUfJtAx1Q09H0P5XXYzoxxQYiwn6W1e8=
             keep-outputs = true
-      
+
       - name: Restore and cache Nix store
         uses: nix-community/cache-nix-action@v1
         with:
@@ -44,11 +44,10 @@ jobs:
             ${{ runner.os }}-nix-${{ hashfiles('./flake.nix', './flake.lock', '.github/workflows/ghcjs.yml') }}
             ${{ runner.os }}-nix-
 
-      - name: 🔨 Remove rzk.cabal, lexer and parser generator files
+      - name: 🔨 Remove lexer and parser generator files
         run: |
           rm -f rzk/src/Language/Rzk/Syntax/Lex.x
           rm -f rzk/src/Language/Rzk/Syntax/Par.y
-          rm -f rzk/rzk.cabal
 
       - name: 🔨 Build GHCJS version with Nix
         run: |
@@ -61,7 +60,7 @@ jobs:
           chmod -R +w dist/
           cp try-rzk/index.html dist/.
 
-      - name: "🚀 Publish JS \"binaries\" (${{ github.ref_name }})"
+      - name: '🚀 Publish JS "binaries" (${{ github.ref_name }})'
         if: ${{ github.ref_name != 'main' && github.event_name == 'push' }}
         uses: JamesIves/github-pages-deploy-action@v4
         with:
@@ -71,7 +70,7 @@ jobs:
           clean: false
           single-commit: true
 
-      - name: "🚀 Publish JS \"binaries\""
+      - name: '🚀 Publish JS "binaries"'
         if: ${{ github.ref_name == 'main' && github.event_name == 'push' }}
         uses: JamesIves/github-pages-deploy-action@v4
         with:

From 29995338205f5cf93920d0b3334e1e0ac9395847 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Mon, 18 Sep 2023 22:21:43 +0200
Subject: [PATCH 10/16] Remove executable from rzk.nix

---
 rzk/rzk.nix | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/rzk/rzk.nix b/rzk/rzk.nix
index 9ba47a4a4..27c3a7914 100644
--- a/rzk/rzk.nix
+++ b/rzk/rzk.nix
@@ -7,17 +7,12 @@ mkDerivation {
   version = "0.5.4";
   src = ./.;
   isLibrary = true;
-  isExecutable = true;
+  isExecutable = false;
   libraryHaskellDepends = [
     aeson array base bifunctors bytestring mtl optparse-generic
     template-haskell text
   ];
   libraryToolDepends = [ alex happy hpack ];
-  executableHaskellDepends = [
-    aeson array base bifunctors bytestring mtl optparse-generic
-    template-haskell text
-  ];
-  executableToolDepends = [ alex happy ];
   testHaskellDepends = [
     aeson array base bifunctors bytestring doctest Glob mtl
     optparse-generic QuickCheck template-haskell text

From 360dad67f6d707d58e76f5ecb773eadf00b2a4c8 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Tue, 19 Sep 2023 00:25:21 +0200
Subject: [PATCH 11/16] Use CPP in Main.hs

---
 rzk/app/Main.hs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/rzk/app/Main.hs b/rzk/app/Main.hs
index e8ded814d..5277b0eaa 100644
--- a/rzk/app/Main.hs
+++ b/rzk/app/Main.hs
@@ -1,7 +1,14 @@
+{-# LANGUAGE CPP #-}
 module Main (main) where
 
+#ifndef __GHCJS__
 import           Main.Utf8 (withUtf8)
+#endif
 import qualified Rzk.Main
 
 main :: IO ()
-main = withUtf8 Rzk.Main.main
+main =
+#ifndef __GHCJS__
+  withUtf8
+#endif
+    Rzk.Main.main

From fc597a051eecd30e1042f742581ecb35568fa1c3 Mon Sep 17 00:00:00 2001
From: Abdelrahman Abounegm <abounegm.abdelrahman@gmail.com>
Date: Tue, 19 Sep 2023 11:26:25 +0200
Subject: [PATCH 12/16] Install and use the glob library

To improve support for shells that do not expand globs automatically
such as PowerShell and CMD on Windows
---
 rzk/package.yaml    |  1 +
 rzk/rzk.cabal       |  9 ++++++---
 rzk/src/Rzk/Main.hs | 19 +++++++++++--------
 stack.yaml          |  1 +
 stack.yaml.lock     |  7 +++++++
 5 files changed, 26 insertions(+), 11 deletions(-)

diff --git a/rzk/package.yaml b/rzk/package.yaml
index dd8cb3e0c..770605884 100644
--- a/rzk/package.yaml
+++ b/rzk/package.yaml
@@ -32,6 +32,7 @@ dependencies:
   - template-haskell
   - text
   - optparse-generic
+  - Glob
 
 ghc-options:
   - -Wall
diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
index 1b0a6bfda..1ecc37d93 100644
--- a/rzk/rzk.cabal
+++ b/rzk/rzk.cabal
@@ -50,7 +50,8 @@ library
       alex
     , happy
   build-depends:
-      aeson
+      Glob
+    , aeson
     , array
     , base >=4.7 && <5
     , bifunctors
@@ -72,7 +73,8 @@ executable rzk
       alex
     , happy
   build-depends:
-      aeson
+      Glob
+    , aeson
     , array
     , base >=4.7 && <5
     , bifunctors
@@ -123,7 +125,8 @@ test-suite rzk-test
       alex
     , happy
   build-depends:
-      aeson
+      Glob
+    , aeson
     , array
     , base >=4.7 && <5
     , bifunctors
diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
index aeecc55e6..61b905b9f 100644
--- a/rzk/src/Rzk/Main.hs
+++ b/rzk/src/Rzk/Main.hs
@@ -10,6 +10,7 @@ import qualified Data.ByteString.Lazy.Char8   as ByteString
 import           Data.Version                 (showVersion)
 import           Options.Generic
 import           System.Exit                  (exitFailure)
+import           System.FilePath.Glob         (glob)
 
 import qualified Language.Rzk.Syntax          as Rzk
 import           Language.Rzk.VSCode.Tokenize (tokenizeModule)
@@ -58,14 +59,16 @@ parseRzkFilesOrStdin = \case
     rzkModule <- parseStdin
     return [("<stdin>", rzkModule)]
   -- otherwise — parse all given files in given order
-  paths -> forM paths $ \path -> do
-    putStrLn ("Loading file " <> path)
-    result <- Rzk.parseModule <$> readFile path
-    case result of
-      Left err -> do
-        putStrLn ("An error occurred when parsing file " <> path)
-        error err
-      Right rzkModule -> return (path, rzkModule)
+  paths -> do
+    expandedPaths <- foldMap glob paths
+    forM (reverse expandedPaths) $ \path -> do
+      putStrLn ("Loading file " <> path)
+      result <- Rzk.parseModule <$> readFile path
+      case result of
+        Left err -> do
+          putStrLn ("An error occurred when parsing file " <> path)
+          error err
+        Right rzkModule -> return (path, rzkModule)
 
 typecheckString :: String -> Either String String
 typecheckString moduleString = do
diff --git a/stack.yaml b/stack.yaml
index fd1d578d8..f5ca303ca 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -41,6 +41,7 @@ packages:
 #
 extra-deps:
 - with-utf8-1.0.2.4
+- Glob-0.10.2
 
 # Override default flag values for local packages and extra-deps
 # flags: {}
diff --git a/stack.yaml.lock b/stack.yaml.lock
index b2d29558a..b59c814c3 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -11,6 +11,13 @@ packages:
       size: 1051
   original:
     hackage: with-utf8-1.0.2.4
+- completed:
+    hackage: Glob-0.10.2@sha256:dd2ddbecae8f84e8f4cacb5b856901a19c25ceaa11f2525d3ee88d034acb0081,2938
+    pantry-tree:
+      sha256: 3c9d365a19c0e15d7cf5e93ee994bdc81958c8e4056f43ec0408f34f1a3bb970
+      size: 1432
+  original:
+    hackage: Glob-0.10.2
 snapshots:
 - completed:
     sha256: cbf721fafa21237e4999d83cfd27137f440ae0e3032ff18fa96e8148d9bf5ce1

From e0045ba59dc8661f1e0ab60f06937488f1276d0f Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Tue, 19 Sep 2023 14:11:21 +0200
Subject: [PATCH 13/16] Update rzk.nix

---
 rzk/rzk.nix | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/rzk/rzk.nix b/rzk/rzk.nix
index 27c3a7914..d347f6eba 100644
--- a/rzk/rzk.nix
+++ b/rzk/rzk.nix
@@ -7,18 +7,23 @@ mkDerivation {
   version = "0.5.4";
   src = ./.;
   isLibrary = true;
-  isExecutable = false;
+  isExecutable = true;
   libraryHaskellDepends = [
-    aeson array base bifunctors bytestring mtl optparse-generic
+    aeson array base bifunctors bytestring Glob mtl optparse-generic
     template-haskell text
   ];
   libraryToolDepends = [ alex happy hpack ];
+  executableHaskellDepends = [
+    aeson array base bifunctors bytestring Glob mtl optparse-generic
+    template-haskell text
+  ];
+  executableToolDepends = [ alex happy ];
   testHaskellDepends = [
     aeson array base bifunctors bytestring doctest Glob mtl
     optparse-generic QuickCheck template-haskell text
   ];
   testToolDepends = [ alex happy ];
-  /* prePatch = "hpack"; */
+  prePatch = "hpack";
   homepage = "https://github.com/rzk-lang/rzk#readme";
   description = "An experimental proof assistant for synthetic ∞-categories";
   license = lib.licenses.bsd3;

From a55f8c579de53b17a22e84dd42caffa33ebe89ff Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Tue, 19 Sep 2023 14:22:35 +0200
Subject: [PATCH 14/16] Throw an exception when glob returns an empty list

---
 rzk/src/Rzk/Main.hs | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
index 61b905b9f..cbc159b89 100644
--- a/rzk/src/Rzk/Main.hs
+++ b/rzk/src/Rzk/Main.hs
@@ -52,6 +52,14 @@ parseStdin = do
       error err
     Right rzkModule -> return rzkModule
 
+-- | Finds matches to the given pattern in the current working directory.
+-- **NOTE:** throws exception when 'glob' returns an empty list.
+globNonEmpty :: FilePath -> IO [FilePath]
+globNonEmpty path = do
+  glob path >>= \case
+    []    -> error ("File(s) not found at " <> path)
+    paths -> return paths
+
 parseRzkFilesOrStdin :: [FilePath] -> IO [(FilePath, Rzk.Module)]
 parseRzkFilesOrStdin = \case
   -- if no paths are given — read from stdin
@@ -60,7 +68,7 @@ parseRzkFilesOrStdin = \case
     return [("<stdin>", rzkModule)]
   -- otherwise — parse all given files in given order
   paths -> do
-    expandedPaths <- foldMap glob paths
+    expandedPaths <- foldMap globNonEmpty paths
     forM (reverse expandedPaths) $ \path -> do
       putStrLn ("Loading file " <> path)
       result <- Rzk.parseModule <$> readFile path

From f2fbf3cf79321ae845ce7782648129d8397d3aa1 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Tue, 19 Sep 2023 15:29:23 +0200
Subject: [PATCH 15/16] Fix handling of subshapes (more type errors!)

---
 rzk/src/Rzk/TypeCheck.hs | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs
index c22b06c3a..36d83f9d4 100644
--- a/rzk/src/Rzk/TypeCheck.hs
+++ b/rzk/src/Rzk/TypeCheck.hs
@@ -2361,13 +2361,15 @@ infer tt = performing (ActionInfer tt) $ case tt of
         b' <- enterScope orig a' $ inferAs universeT b
         return (typeFunT orig a' Nothing b')
       -- an argument can be a shape
-      TypeFunT _ty _orig cube _mtope UniverseTopeT{} -> do
+      TypeFunT _ty _orig cube mtope UniverseTopeT{} -> do
         mapM_ checkNameShadowing orig
         enterScope orig cube $ do
           let tope' = appT topeT (S <$> a') (Pure Z)  -- eta expand a'
           localTope tope' $ do
             b' <- inferAs universeT b
-            return (typeFunT orig cube (Just tope') b')
+            case mtope of
+              Nothing -> return (typeFunT orig cube (Just tope') b')
+              Just tope'' -> return (typeFunT orig cube (Just (topeAndT tope'' tope')) b')
       ty -> issueTypeError $ TypeErrorInvalidArgumentType a ty
 
   TypeFun orig cube (Just tope) ret -> do
@@ -2403,10 +2405,16 @@ infer tt = performing (ActionInfer tt) $ case tt of
       RecBottomT{} -> pure recBottomT -- FIXME: is this ok?
       TypeFunT _ty _orig a mtope b -> do
         x' <- typecheck x a
+        let result = appT (substituteT x' b) f' x'
         case b of
-          UniverseTopeT{} -> return ()
-          _               -> mapM_ (contextEntails . substituteT x') mtope   -- FIXME: need to check?
-        return (appT (substituteT x' b) f' x')
+          UniverseTopeT{} -> do
+            case mtope of
+              Nothing -> return result
+              Just tope -> do
+                return (topeAndT (substituteT x' tope) result)
+          _               -> do
+            mapM_ (contextEntails . substituteT x') mtope   -- FIXME: need to check?
+            return result
       ty -> issueTypeError $ TypeErrorNotFunction f' ty
 
   Lambda _orig Nothing _body -> do

From 13cdc6d7413748003287ad7be0843e94852ff70a Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Tue, 19 Sep 2023 16:10:07 +0200
Subject: [PATCH 16/16] Bump version and update changelogs

---
 docs/docs/getting-started/changelog.md | 33 +++++++++++++++++++-------
 rzk/ChangeLog.md                       | 28 +++++++++++++++-------
 rzk/package.yaml                       |  2 +-
 rzk/rzk.cabal                          |  2 +-
 rzk/rzk.nix                            |  2 +-
 5 files changed, 47 insertions(+), 20 deletions(-)

diff --git a/docs/docs/getting-started/changelog.md b/docs/docs/getting-started/changelog.md
index 7d2316971..a97958696 100644
--- a/docs/docs/getting-started/changelog.md
+++ b/docs/docs/getting-started/changelog.md
@@ -6,7 +6,24 @@ 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.5.3 — 2022-07-12
+## v0.5.5 — 2023-09-19
+
+This version contains Unicode and tope logic-related fixes:
+
+1. Fix (add missing checks) for subshapes (see [#85](https://github.com/rzk-lang/rzk/pull/85));
+2. Allow to handle wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83));
+3. Fix Unicode on machines with non-standard locales (see [#82](https://github.com/rzk-lang/rzk/pull/82));
+4. Specify `happy` and `alex` as build tools to fix cabal build from Hackage (see [#80](https://github.com/rzk-lang/rzk/pull/80)).
+5. Add configuration for MkDocs plugin for Rzk (see [#79](https://github.com/rzk-lang/rzk/pull/79)).
+
+## v0.5.4 — 2023-08-19
+
+This version contains minor improvements:
+
+1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76));
+2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)).
+
+## v0.5.3 — 2023-07-12
 
 This version contains a few minor improvements:
 
@@ -17,7 +34,7 @@ This version contains a few minor improvements:
 5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983));
 6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66));
 
-## v0.5.2 — 2022-07-05
+## v0.5.2 — 2023-07-05
 
 This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit:
 
@@ -27,7 +44,7 @@ This version introduces support for Unicode syntax, better recognition of Markdo
 - Factor out Pygments highlighting to https://github.com/rzk-lang/pygments-rzk;
 - Use new cache action for Nix (see [#60](https://github.com/rzk-lang/rzk/pull/60)).
 
-## v0.5.1 — 2022-06-29
+## v0.5.1 — 2023-06-29
 
 This version fixes `Unit` type and makes some changes to documentation:
 
@@ -38,7 +55,7 @@ This version fixes `Unit` type and makes some changes to documentation:
 - Switch to Material theme for MkDocs (see [#57](https://github.com/rzk-lang/rzk/pull/57));
 - Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b](https://github.com/rzk-lang/rzk/commit/8ba1c55b));
 
-## v0.5 — 2022-06-20
+## v0.5 — 2023-06-20
 
 This version contains the following changes:
 
@@ -46,7 +63,7 @@ This version contains the following changes:
 - Add basic tokenizer support via `rzk tokenize` (see [#53](https://github.com/rzk-lang/rzk/pull/53));
 - Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9)).
 
-## v0.4.1 — 2022-06-16
+## v0.4.1 — 2023-06-16
 
 This is version contains minor changes, primarily in tools around rzk:
 
@@ -57,7 +74,7 @@ This is version contains minor changes, primarily in tools around rzk:
 - Add Pygments highlighting (see [01c2a017](https://github.com/rzk-lang/rzk/commit/01c2a017), [cbd656cc](https://github.com/rzk-lang/rzk/commit/cbd656cc), [5220ddf9](https://github.com/rzk-lang/rzk/commit/5220ddf9), [142ec003](https://github.com/rzk-lang/rzk/commit/142ec003), [5c7425f2](https://github.com/rzk-lang/rzk/commit/5c7425f2));
 - Update HighlightJS config for rzk v0.4.0 (see [171ee63f](https://github.com/rzk-lang/rzk/commit/171ee63f));
 
-## v0.4.0 — 2022-05-18
+## v0.4.0 — 2023-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.
 
@@ -68,7 +85,7 @@ Minor improvements:
 - Add flake, set up nix and cabal builds, cache nix store on CI (see [#39](https://github.com/rzk-lang/rzk/pull/39));
 - Apply stylish-haskell (see [7d42ef62](https://github.com/rzk-lang/rzk/commit/7d42ef62));
 
-## v0.3.0 — 2022-04-28
+## v0.3.0 — 2023-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"`):
@@ -87,7 +104,7 @@ 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
+## v0.2.0 - 2023-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/ChangeLog.md b/rzk/ChangeLog.md
index a76472e73..a97958696 100644
--- a/rzk/ChangeLog.md
+++ b/rzk/ChangeLog.md
@@ -6,14 +6,24 @@ 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.5.4 — 2022-08-19
+## v0.5.5 — 2023-09-19
+
+This version contains Unicode and tope logic-related fixes:
+
+1. Fix (add missing checks) for subshapes (see [#85](https://github.com/rzk-lang/rzk/pull/85));
+2. Allow to handle wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83));
+3. Fix Unicode on machines with non-standard locales (see [#82](https://github.com/rzk-lang/rzk/pull/82));
+4. Specify `happy` and `alex` as build tools to fix cabal build from Hackage (see [#80](https://github.com/rzk-lang/rzk/pull/80)).
+5. Add configuration for MkDocs plugin for Rzk (see [#79](https://github.com/rzk-lang/rzk/pull/79)).
+
+## v0.5.4 — 2023-08-19
 
 This version contains minor improvements:
 
 1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76));
 2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)).
 
-## v0.5.3 — 2022-07-12
+## v0.5.3 — 2023-07-12
 
 This version contains a few minor improvements:
 
@@ -24,7 +34,7 @@ This version contains a few minor improvements:
 5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983));
 6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66));
 
-## v0.5.2 — 2022-07-05
+## v0.5.2 — 2023-07-05
 
 This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit:
 
@@ -34,7 +44,7 @@ This version introduces support for Unicode syntax, better recognition of Markdo
 - Factor out Pygments highlighting to https://github.com/rzk-lang/pygments-rzk;
 - Use new cache action for Nix (see [#60](https://github.com/rzk-lang/rzk/pull/60)).
 
-## v0.5.1 — 2022-06-29
+## v0.5.1 — 2023-06-29
 
 This version fixes `Unit` type and makes some changes to documentation:
 
@@ -45,7 +55,7 @@ This version fixes `Unit` type and makes some changes to documentation:
 - Switch to Material theme for MkDocs (see [#57](https://github.com/rzk-lang/rzk/pull/57));
 - Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b](https://github.com/rzk-lang/rzk/commit/8ba1c55b));
 
-## v0.5 — 2022-06-20
+## v0.5 — 2023-06-20
 
 This version contains the following changes:
 
@@ -53,7 +63,7 @@ This version contains the following changes:
 - Add basic tokenizer support via `rzk tokenize` (see [#53](https://github.com/rzk-lang/rzk/pull/53));
 - Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9)).
 
-## v0.4.1 — 2022-06-16
+## v0.4.1 — 2023-06-16
 
 This is version contains minor changes, primarily in tools around rzk:
 
@@ -64,7 +74,7 @@ This is version contains minor changes, primarily in tools around rzk:
 - Add Pygments highlighting (see [01c2a017](https://github.com/rzk-lang/rzk/commit/01c2a017), [cbd656cc](https://github.com/rzk-lang/rzk/commit/cbd656cc), [5220ddf9](https://github.com/rzk-lang/rzk/commit/5220ddf9), [142ec003](https://github.com/rzk-lang/rzk/commit/142ec003), [5c7425f2](https://github.com/rzk-lang/rzk/commit/5c7425f2));
 - Update HighlightJS config for rzk v0.4.0 (see [171ee63f](https://github.com/rzk-lang/rzk/commit/171ee63f));
 
-## v0.4.0 — 2022-05-18
+## v0.4.0 — 2023-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.
 
@@ -75,7 +85,7 @@ Minor improvements:
 - Add flake, set up nix and cabal builds, cache nix store on CI (see [#39](https://github.com/rzk-lang/rzk/pull/39));
 - Apply stylish-haskell (see [7d42ef62](https://github.com/rzk-lang/rzk/commit/7d42ef62));
 
-## v0.3.0 — 2022-04-28
+## v0.3.0 — 2023-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"`):
@@ -94,7 +104,7 @@ 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
+## v0.2.0 - 2023-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/package.yaml b/rzk/package.yaml
index 770605884..d87de35dd 100644
--- a/rzk/package.yaml
+++ b/rzk/package.yaml
@@ -1,5 +1,5 @@
 name: rzk
-version: 0.5.4
+version: 0.5.5
 github: "rzk-lang/rzk"
 license: BSD3
 author: "Nikolai Kudasov"
diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
index 1ecc37d93..4d1e11f48 100644
--- 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.4
+version:        0.5.5
 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
index d347f6eba..6bee4ac32 100644
--- a/rzk/rzk.nix
+++ b/rzk/rzk.nix
@@ -4,7 +4,7 @@
 }:
 mkDerivation {
   pname = "rzk";
-  version = "0.5.4";
+  version = "0.5.5";
   src = ./.;
   isLibrary = true;
   isExecutable = true;