From ee0d0638283232c99003a83fdf41eb109ae78983 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sun, 9 Jul 2023 23:03:30 +0300 Subject: [PATCH] Update all references from fizruk to rzk-lang --- .github/workflows/mkdocs.yml | 2 +- CITATION.cff | 4 +-- README.md | 22 ++++++------ docs/docs/getting-started/changelog.md | 36 +++++++++---------- docs/docs/getting-started/install.md | 8 ++--- docs/docs/reference/builtins/unit.rzk.md | 2 +- docs/docs/reference/introduction.rzk.md | 2 +- docs/docs/tools/continuous.md | 2 +- docs/docs/tools/highlight.md | 6 ++-- docs/docs/tools/ide.md | 2 +- docs/mkdocs.yml | 4 +-- rzk/ChangeLog.md | 46 ++++++++++++------------ rzk/README.md | 2 +- rzk/package.yaml | 4 +-- rzk/rzk.cabal | 8 ++--- rzk/rzk.nix | 2 +- rzk/src/Rzk/TypeCheck.hs | 2 +- try-rzk/index.html | 2 +- 18 files changed, 78 insertions(+), 78 deletions(-) diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml index 2bdfd9fd..2af10e61 100644 --- a/.github/workflows/mkdocs.yml +++ b/.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 diff --git a/CITATION.cff b/CITATION.cff index e55a5711..94eb5862 100644 --- a/CITATION.cff +++ b/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" diff --git a/README.md b/README.md index 0b08f148..1b495871 100644 --- a/README.md +++ b/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 diff --git a/docs/docs/getting-started/changelog.md b/docs/docs/getting-started/changelog.md index 5bfe3a33..c5e8babe 100644 --- a/docs/docs/getting-started/changelog.md +++ b/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 `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. -- 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 diff --git a/docs/docs/getting-started/install.md b/docs/docs/getting-started/install.md index c62b9baa..fd11e01f 100644 --- a/docs/docs/getting-started/install.md +++ b/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 diff --git a/docs/docs/reference/builtins/unit.rzk.md b/docs/docs/reference/builtins/unit.rzk.md index 746bb190..bb2335b7 100644 --- a/docs/docs/reference/builtins/unit.rzk.md +++ b/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._ diff --git a/docs/docs/reference/introduction.rzk.md b/docs/docs/reference/introduction.rzk.md index b99c9bd1..a399a27c 100644 --- a/docs/docs/reference/introduction.rzk.md +++ b/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. -[^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. diff --git a/docs/docs/tools/continuous.md b/docs/docs/tools/continuous.md index 2f87cc06..7bb5b35b 100644 --- a/docs/docs/tools/continuous.md +++ b/docs/docs/tools/continuous.md @@ -2,4 +2,4 @@ ## GitHub Action -See . See also for an example usage of the action. +See . See also for an example usage of the action. diff --git a/docs/docs/tools/highlight.md b/docs/docs/tools/highlight.md index e5e4205a..efd0505d 100644 --- a/docs/docs/tools/highlight.md +++ b/docs/docs/tools/highlight.md @@ -3,6 +3,6 @@ Currently basic syntax highlighting is supported for several environments: 1. `vscode-rzk` VS Code extension provides syntax highlighting for both `*.rzk` files and `rzk` code blocks in Markdown files. -2. HighlightJS syntax highlighting (used by MkDocs) is available at https://github.com/fizruk/rzk/blob/develop/docs/custom_theme/js/rzk.js -3. Pygments syntax highlighting is available a Python package at https://github.com/fizruk/rzk/tree/develop/rzk/RzkLexer. This syntax highlighter is suitable for using with LaTeX (e.g. with `minted` package). -4. There is also an obsolete syntax highlighting mode for CodeMirror 5. \ No newline at end of file +2. HighlightJS syntax highlighting (used by MkDocs) is available at https://github.com/rzk-lang/rzk/blob/develop/docs/custom_theme/js/rzk.js +3. Pygments syntax highlighting is available a Python package at https://github.com/rzk-lang/rzk/tree/develop/rzk/RzkLexer. This syntax highlighter is suitable for using with LaTeX (e.g. with `minted` package). +4. There is also an obsolete syntax highlighting mode for CodeMirror 5. diff --git a/docs/docs/tools/ide.md b/docs/docs/tools/ide.md index 12cf4df0..5ed2b48c 100644 --- a/docs/docs/tools/ide.md +++ b/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. diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index c55c8b70..d42c8216 100644 --- a/docs/mkdocs.yml +++ b/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: diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index 7630a855..739c0418 100644 --- a/rzk/ChangeLog.md +++ b/rzk/ChangeLog.md @@ -10,52 +10,52 @@ and this project adheres to the This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit: -- Support some Unicode syntax (see [#61](https://github.com/fizruk/rzk/pull/61)); -- Support curly braces syntax for code blocks (see [#64](https://github.com/fizruk/rzk/pull/64)); -- Update documentation a bit (see [07b520a6](https://github.com/fizruk/rzk/commit/07b520a67eb432105fad908202949c93a1639ca8) and [7cc7f383](https://github.com/fizruk/rzk/commit/7cc7f383b1785130277ed79d123c1dd357162d9d)); -- Factor out Pygments highlighting to https://github.com/fizruk/pygments-rzk; -- Use new cache action for Nix (see [#60](https://github.com/fizruk/rzk/pull/60)). +- Support some Unicode syntax (see [#61](https://github.com/rzk-lang/rzk/pull/61)); +- Support curly braces syntax for code blocks (see [#64](https://github.com/rzk-lang/rzk/pull/64)); +- Update documentation a bit (see [07b520a6](https://github.com/rzk-lang/rzk/commit/07b520a67eb432105fad908202949c93a1639ca8) and [7cc7f383](https://github.com/rzk-lang/rzk/commit/7cc7f383b1785130277ed79d123c1dd357162d9d)); +- 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 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 `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. -- 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 diff --git a/rzk/README.md b/rzk/README.md index 1a0c081f..8b786e25 100644 --- a/rzk/README.md +++ b/rzk/README.md @@ -2,4 +2,4 @@ An experimental proof assistant for synthetic ∞-categories. -See README at https://github.com/fizruk/rzk#readme. +See README at https://github.com/rzk-lang/rzk#readme. diff --git a/rzk/package.yaml b/rzk/package.yaml index 7c162c74..a5a7cdd7 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -1,6 +1,6 @@ name: rzk version: 0.5.2 -github: "fizruk/rzk" +github: "rzk-lang/rzk" license: BSD3 author: "Nikolai Kudasov" maintainer: "nickolay.kudasov@gmail.com" @@ -16,7 +16,7 @@ category: Dependent Types # same as Agda # To avoid duplicated efforts in documentation and dealing with the # complications of embedding Haddock markup inside cabal files, it is # common to point users to the README.md file. -description: Please see the README on GitHub at +description: Please see the README on GitHub at dependencies: - array diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index 012fea8e..1a654e38 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -7,10 +7,10 @@ cabal-version: 1.12 name: rzk version: 0.5.2 synopsis: An experimental proof assistant for synthetic ∞-categories -description: Please see the README on GitHub at +description: Please see the README on GitHub at category: Dependent Types -homepage: https://github.com/fizruk/rzk#readme -bug-reports: https://github.com/fizruk/rzk/issues +homepage: https://github.com/rzk-lang/rzk#readme +bug-reports: https://github.com/rzk-lang/rzk/issues author: Nikolai Kudasov maintainer: nickolay.kudasov@gmail.com copyright: 2023 Nikolai Kudasov @@ -23,7 +23,7 @@ extra-source-files: source-repository head type: git - location: https://github.com/fizruk/rzk + location: https://github.com/rzk-lang/rzk library exposed-modules: diff --git a/rzk/rzk.nix b/rzk/rzk.nix index 66a21bd3..0b6190ce 100644 --- a/rzk/rzk.nix +++ b/rzk/rzk.nix @@ -21,7 +21,7 @@ mkDerivation { template-haskell text ]; prePatch = "hpack"; - homepage = "https://github.com/fizruk/rzk#readme"; + homepage = "https://github.com/rzk-lang/rzk#readme"; description = "An experimental proof assistant for synthetic ∞-categories"; license = lib.licenses.bsd3; } diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index 8eee829b..363db095 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -399,7 +399,7 @@ issueTypeError err = do panicImpossible :: String -> a panicImpossible msg = error $ unlines [ "PANIC! Impossible happened (" <> msg <> ")!" - , "Please, report a bug at https://github.com/fizruk/rzk/issues" + , "Please, report a bug at https://github.com/rzk-lang/rzk/issues" -- TODO: add details and/or instructions how to produce an artifact for reproducing ] diff --git a/try-rzk/index.html b/try-rzk/index.html index a2a5b111..9f0b22ab 100644 --- a/try-rzk/index.html +++ b/try-rzk/index.html @@ -13,7 +13,7 @@ - +