Update all references from fizruk to rzk-lang

.github/workflows/mkdocs.yml

@@ -28,7 +28,7 @@ jobs:
       - name: 🔨 Install rzk proof assistant
         uses: jaxxstorm/action-install-gh-release@v1.10.0
         with:
-          repo: fizruk/rzk
+          repo: rzk-lang/rzk
           tag: latest # FIXME: should use the version from the same Git commit
           rename-to: rzk
           chmod: 0755

CITATION.cff

@@ -4,5 +4,5 @@ authors:
   given-names: Nikolai
   orcid: "https://orcid.org/0000-0001-6572-7292"
 title: "rzk: a prototype proof assistant for synthetic $\\infty$-categories"
-version: 0.5
-url: "https://github.com/fizruk/rzk"
+version: 0.5.2
+url: "https://github.com/rzk-lang/rzk"

README.md

@@ -1,16 +1,16 @@
 # rzk
 
-[![MkDocs](https://shields.io/badge/MkDocs-documentation-informational)](https://fizruk.github.io/rzk/)
-[![Haddock](https://shields.io/badge/Haddock-documentation-informational)](https://fizruk.github.io/rzk/haddock/index.html)
-[![GHCJS build](https://github.com/fizruk/rzk/actions/workflows/ghcjs.yml/badge.svg?branch=main)](https://github.com/fizruk/rzk/actions/workflows/ghcjs.yml)
+[![MkDocs](https://shields.io/badge/MkDocs-documentation-informational)](https://rzk-lang.github.io/rzk/)
+[![Haddock](https://shields.io/badge/Haddock-documentation-informational)](https://rzk-lang.github.io/rzk/haddock/index.html)
+[![GHCJS build](https://github.com/rzk-lang/rzk/actions/workflows/ghcjs.yml/badge.svg?branch=main)](https://github.com/rzk-lang/rzk/actions/workflows/ghcjs.yml)
 
 An experimental proof assistant for synthetic ∞-categories.
 
-[![Early prototype demo.](images/split-demo-render.png)](https://fizruk.github.io/rzk/)
+[![Early prototype demo.](images/split-demo-render.png)](https://rzk-lang.github.io/rzk/)
 
 ## About this project
 
-This project has started with the idea of bringing Riehl and Shulman's 2017 paper [1] to "life" by implementing a proof assistant based on their type theory with shapes. Currently an early prototype with an [online playground](https://fizruk.github.io/rzk/) is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: https://github.com/fizruk/sHoTT and https://github.com/emilyriehl/yoneda. `sHoTT` project (originally a fork of the yoneda project) aims to cover more formalisations in simplicial HoTT and ∞-categories, while `yoneda` project aims to compare different formalisations of the Yoneda lemma.
+This project has started with the idea of bringing Riehl and Shulman's 2017 paper [1] to "life" by implementing a proof assistant based on their type theory with shapes. Currently an early prototype with an [online playground](https://rzk-lang.github.io/rzk/) is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: https://github.com/fizruk/sHoTT and https://github.com/emilyriehl/yoneda. `sHoTT` project (originally a fork of the yoneda project) aims to cover more formalisations in simplicial HoTT and ∞-categories, while `yoneda` project aims to compare different formalisations of the Yoneda lemma.
 
 Internally, `rzk` uses a version of second-order abstract syntax allowing relatively straightforward handling of binders (such as lambda abstraction). In the future, `rzk` aims to support dependent type inference relying on E-unification for second-order abstract syntax [2].
 Using such representation is motivated by automatic handling of binders and easily automated boilerplate code. The idea is that this should keep the implementation of `rzk` relatively small and less error-prone than some of the existing approaches to implementation of dependent type checkers.
@@ -19,7 +19,7 @@ An important part of `rzk` is a tope layer solver, which is essentially a theore
 
 ## How to use `rzk`
 
-For relatively small single-file formalisations, you can use the online playground at https://fizruk.github.io/rzk/playground.html
+For relatively small single-file formalisations, you can use the online playground at https://rzk-lang.github.io/rzk/playground.html
 
 However, for larger and multi-file formalisations you should install a version of `rzk` locally:
 
@@ -28,9 +28,9 @@ However, for larger and multi-file formalisations you should install a version o
   cabal install rzk
   ```
 
-- You can install the latest "development" version of `rzk` from the [`develop` branch](https://github.com/fizruk/rzk/tree/develop) of this repository:
+- You can install the latest "development" version of `rzk` from the [`develop` branch](https://github.com/rzk-lang/rzk/tree/develop) of this repository:
   ```sh
-  git clone https://github.com/fizruk/rzk.git
+  git clone https://github.com/rzk-lang/rzk.git
   cd rzk
   git checkout develop
   stack build && stack install
@@ -99,7 +99,7 @@ The project is developed with both Stack and Nix (for GHCJS version).
 For quick local development and testing it is recommended to work with a GHC version, using [Stack tool](https://docs.haskellstack.org/en/stable/README/). Clone this project and simply run `stack build`:
 
 ```sh
-git clone git@github.com:fizruk/rzk.git
+git clone git@github.com:rzk-lang/rzk.git
 cd rzk
 stack build
 ```
@@ -125,12 +125,12 @@ cachix use miso-haskell
 
 Clone the repository, enter `try-rzk` directory and use `nix-build`:
 ```sh
-git clone git@github.com:fizruk/rzk.git
+git clone git@github.com:rzk-lang/rzk.git
 cd rzk/try-rzk
 nix-build
 ```
 
-Now open `playground.html` to see the result. Note that if local GHCJS build is unavailable, `playground.html` will use the [JS file from GitHub Pages](https://fizruk.github.io/rzk/v0.1.0/result/bin/try-rzk.jsexe/all.js) as a fallback.
+Now open `playground.html` to see the result. Note that if local GHCJS build is unavailable, `playground.html` will use the [JS file from GitHub Pages](https://rzk-lang.github.io/rzk/v0.1.0/result/bin/try-rzk.jsexe/all.js) as a fallback.
 
 ##### Flake
 

docs/docs/getting-started/changelog.md

@@ -10,42 +10,42 @@ and this project adheres to the
 
 This version fixes `Unit` type and makes some changes to documentation:
 
-- Fix computation for `Unit` (see [2f7d6295]( https://github.com/fizruk/rzk/commit/2f7d6295 ));
-- Update documentation (see [ea2d176b]( https://github.com/fizruk/rzk/commit/ea2d176b ));
-- Use mike to deploy versioned docs (see [99cf721a]( https://github.com/fizruk/rzk/commit/99cf721a ));
-- Replace MkDocs hook with the published plugin (see [#58]( https://github.com/fizruk/rzk/pull/58 ));
-- Switch to Material theme for MkDocs (see [#57]( https://github.com/fizruk/rzk/pull/57 ));
-- Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b]( https://github.com/fizruk/rzk/commit/8ba1c55b ));
+- Fix computation for `Unit` (see [2f7d6295]( https://github.com/rzk-lang/rzk/commit/2f7d6295 ));
+- Update documentation (see [ea2d176b]( https://github.com/rzk-lang/rzk/commit/ea2d176b ));
+- Use mike to deploy versioned docs (see [99cf721a]( https://github.com/rzk-lang/rzk/commit/99cf721a ));
+- Replace MkDocs hook with the published plugin (see [#58]( https://github.com/rzk-lang/rzk/pull/58 ));
+- 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
 
 This version contains the following changes:
 
-- `Unit` type (with `unit` value) (see [ede02611]( https://github.com/fizruk/rzk/commit/ede02611 ) and [bf9d6cd9]( https://github.com/fizruk/rzk/commit/bf9d6cd9 );
-- Add basic tokenizer support via `rzk tokenize` (see [#53]( https://github.com/fizruk/rzk/pull/53 ));
-- Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9]( https://github.com/fizruk/rzk/commit/bf9d6cd9 )).
+- `Unit` type (with `unit` value) (see [ede02611]( https://github.com/rzk-lang/rzk/commit/ede02611 ) and [bf9d6cd9]( https://github.com/rzk-lang/rzk/commit/bf9d6cd9 );
+- 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
 
 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 ));
+- Add `rzk version` command (see [f1709dc7]( https://github.com/rzk-lang/rzk/commit/f1709dc7 ));
+- Add action to release binaries (see [9286afae]( https://github.com/rzk-lang/rzk/commit/9286afae ));
+- Automate SVG rendering in MkDocs (see [#49]( https://github.com/rzk-lang/rzk/pull/49 ));
+- Read `stdin` when no filepaths are given (see [936c15a3]( https://github.com/rzk-lang/rzk/commit/936c15a3 ));
+- 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
 
 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.
 
-- Variables and sections (Coq-style) (see [#38]( https://github.com/fizruk/rzk/pull/38 ));
+- Variables and sections (Coq-style) (see [#38]( https://github.com/rzk-lang/rzk/pull/38 ));
 
 Minor improvements:
 
-- Add flake, set up nix and cabal builds, cache nix store on CI (see [#39]( https://github.com/fizruk/rzk/pull/39 ));
-- Apply stylish-haskell (see [7d42ef62]( https://github.com/fizruk/rzk/commit/7d42ef62 ));
+- 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
 

docs/docs/getting-started/install.md

@@ -3,13 +3,13 @@
 ## VS Code extension with binaries (recommended)
 
 !!! warning "Work-in-progress"
-    We plan to make installation from a VS Code extension as recommended to simplify user experience. See [https://github.com/fizruk/vscode-rzk/issues/21](https://github.com/fizruk/vscode-rzk/issues/21) for details and current status.
+    We plan to make installation from a VS Code extension as recommended to simplify user experience. See [https://github.com/rzk-lang/vscode-rzk/issues/21](https://github.com/rzk-lang/vscode-rzk/issues/21) for details and current status.
 
 ## Install binaries
 
 ### Download from GitHub
 
-You can download and use binaries (at least for some platforms) directly for one of the latest releases on GitHub at https://github.com/fizruk/rzk/releases. If your platform is not represented, please consider leaving an issue at https://github.com/fizruk/rzk/issues/new.
+You can download and use binaries (at least for some platforms) directly for one of the latest releases on GitHub at https://github.com/rzk-lang/rzk/releases. If your platform is not represented, please consider leaving an issue at https://github.com/rzk-lang/rzk/issues/new.
 
 ## Install from sources
 
@@ -26,7 +26,7 @@ stack install rzk
 To build and install with Stack from sources on GitHub:
 
 ```sh
-git clone https://github.com/fizruk/rzk.git
+git clone https://github.com/rzk-lang/rzk.git
 cd rzk
 git checkout develop
 stack build && stack install
@@ -43,7 +43,7 @@ cabal v2-install rzk
 To build and install with `cabal-install` from sources on GitHub:
 
 ```sh
-git clone https://github.com/fizruk/rzk.git
+git clone https://github.com/rzk-lang/rzk.git
 cd rzk
 git checkout develop
 cabal v2-build && cabal v2-install

docs/docs/reference/builtins/unit.rzk.md

@@ -59,6 +59,6 @@ As a non-trivial example, here is a proof that `Unit` is a Segal type:
 #end isSegal-Unit
 ```
 
-[Unit support]: https://github.com/fizruk/rzk/releases/tag/v0.5.1
+[Unit support]: https://github.com/rzk-lang/rzk/releases/tag/v0.5.1
 
 [^1]: The Univalent Foundations Program (2013). _Homotopy Type Theory: Univalent Foundations of Mathematics._ <https://homotopytypetheory.org/book>

docs/docs/reference/introduction.rzk.md

@@ -69,4 +69,4 @@ so current version embraces this lax treatment of universes.
 
 [^1]: Emily Riehl & Michael Shulman. _A type theory for synthetic ∞-categories._ Higher Structures 1(1), 147-224. 2017. <https://arxiv.org/abs/1705.07442>
 
-[^2]: In version [:octicons-tag-24: v0.1.0](https://github.com/fizruk/rzk/releases/tag/v0.1.0), `rzk` has supported simply typed lambda calculus, PCF, and MLTT. However, those languages have been removed.
+[^2]: In version [:octicons-tag-24: v0.1.0](https://github.com/rzk-lang/rzk/releases/tag/v0.1.0), `rzk` has supported simply typed lambda calculus, PCF, and MLTT. However, those languages have been removed.

docs/docs/tools/continuous.md

@@ -2,4 +2,4 @@
 
 ## GitHub Action
 
-See <https://github.com/fizruk/rzk-action>. See also <https://github.com/emilyriehl/yoneda> for an example usage of the action.
+See <https://github.com/rzk-lang/rzk-action>. See also <https://github.com/emilyriehl/yoneda> for an example usage of the action.

docs/docs/tools/highlight.md

@@ -3,6 +3,6 @@
 Currently basic syntax highlighting is supported for several environments:
 
 1. <a href="https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting" target="_blank">`vscode-rzk` VS Code extension</a> provides syntax highlighting for both `*.rzk` files and `rzk` code blocks in Markdown files.
-2. HighlightJS syntax highlighting (used by MkDocs) is available at <a href="https://github.com/fizruk/rzk/blob/develop/docs/custom_theme/js/rzk.js" target="_blank">https://github.com/fizruk/rzk/blob/develop/docs/custom_theme/js/rzk.js</a>
-3. Pygments syntax highlighting is available a Python package at <a href="https://github.com/fizruk/rzk/tree/develop/rzk/RzkLexer#readme" target="_blank">https://github.com/fizruk/rzk/tree/develop/rzk/RzkLexer</a>. This syntax highlighter is suitable for using with LaTeX (e.g. with `minted` package).
-4. There is also an obsolete <a href="https://github.com/fizruk/rzk/blob/develop/try-rzk/playground.html#L219-L269" target="_blank">syntax highlighting mode for CodeMirror 5</a>.
+2. HighlightJS syntax highlighting (used by MkDocs) is available at <a href="https://github.com/rzk-lang/rzk/blob/develop/docs/custom_theme/js/rzk.js" target="_blank">https://github.com/rzk-lang/rzk/blob/develop/docs/custom_theme/js/rzk.js</a>
+3. Pygments syntax highlighting is available a Python package at <a href="https://github.com/rzk-lang/rzk/tree/develop/rzk/RzkLexer#readme" target="_blank">https://github.com/rzk-lang/rzk/tree/develop/rzk/RzkLexer</a>. This syntax highlighter is suitable for using with LaTeX (e.g. with `minted` package).
+4. There is also an obsolete <a href="https://github.com/rzk-lang/rzk/blob/develop/try-rzk/playground.html#L219-L269" target="_blank">syntax highlighting mode for CodeMirror 5</a>.

docs/docs/tools/ide.md

@@ -2,6 +2,6 @@
 
 ## VS Code
 
-There exists a VS Code extension for `rzk` ([on VS Marketplace](https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting), [on GitHub](https://github.com/fizruk/vscode-rzk)).
+There exists a VS Code extension for `rzk` ([on VS Marketplace](https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting), [on GitHub](https://github.com/rzk-lang/vscode-rzk)).
 
 Please, refer to the documentation of the extension for more details.

docs/mkdocs.yml

@@ -1,6 +1,6 @@
 site_name: "rzk: an experimental proof assistant for syntheric ∞-categories"
-repo_url: https://github.com/fizruk/rzk
-repo_name: fizruk/rzk
+repo_url: https://github.com/rzk-lang/rzk
+repo_name: rzk-lang/rzk
 edit_uri: edit/develop/docs/docs/
 
 nav: