Merge branch 'release-v0.6.7'

* release-v0.6.7: Bump version and update changelog Add cabal update to instructions Add links to Rzk Zulip fix: bnfc executable name refactor: naming refactor: rename message -> output, move const definitions fix: build scripts fix: switch to vite
rzk-lang · Oct 7, 2023 · f05581c · f05581c
2 parents 9acf9bd + aac000f
commit f05581c
Show file tree

Hide file tree

Showing 33 changed files with 970 additions and 538 deletions.
diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
@@ -75,7 +75,7 @@ jobs:
 
       - name: 🔨 Build Playground
         env:
-          BASEPATH: /${{ github.event.repository.name }}/${{ github.ref_name }}/playground
+          ASSET_URL: /${{ github.event.repository.name }}/${{ github.ref_name }}/playground
         run: |
           nix run .#release-rzk-playground
 

diff --git a/CITATION.cff b/CITATION.cff
@@ -1,8 +1,8 @@
 cff-version: 1.2.0
 authors:
-- family-names: Kudasov
-  given-names: Nikolai
-  orcid: "https://orcid.org/0000-0001-6572-7292"
+  - family-names: Kudasov
+    given-names: Nikolai
+    orcid: "https://orcid.org/0000-0001-6572-7292"
 title: "Rzk: a  proof assistant for synthetic $\\infty$-categories"
-version: 0.6.6
+version: 0.6.7
 url: "https://github.com/rzk-lang/rzk"
diff --git a/README.md b/README.md
@@ -3,6 +3,7 @@
 [![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)
+[![Rzk Zulip chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://rzk-lang.zulipchat.com)
 
 An experimental proof assistant for synthetic ∞-categories.
 
@@ -19,6 +20,11 @@ An important part of `rzk` is a tope layer solver, which is essentially a theore
 
 See the list of contributors at [docs/docs/CONTRIBUTORS.md](docs/docs/CONTRIBUTORS.md).
 
+## Discussing Rzk and getting help
+
+A Zulip chat is available for all to join and chat about Rzk, including formalization projects, development of Rzk, and related projects:
+<https://rzk-lang.zulipchat.com/register/>
+
 ## How to use `rzk`
 
 For relatively small single-file formalisations, you can use the online playground at <https://rzk-lang.github.io/rzk/develop/playground>
@@ -28,6 +34,7 @@ However, for larger and multi-file formalisations you should install a version o
 - You can install the latest "stable" version of `rzk` from Hackage:
 
   ```sh
+  cabal update
   cabal install rzk
   ```
 

diff --git a/docs/docs/CHANGELOG.md b/docs/docs/CHANGELOG.md
@@ -6,6 +6,17 @@ 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.6.7 — 2023-10-07
+
+- Fix build on some systems (fix `BNFC:bnfc` executable dependency, see [#125](https://github.com/rzk-lang/rzk/pull/125))
+- Improve Rzk Playground (see [#124](https://github.com/rzk-lang/rzk/pull/124) by @deemp):
+  - Add `snippet_url` parameter
+  - Migrated from NextJS to Vite
+  - Use `setText` on `params` attribute
+- Slightly improve documentation:
+  - Add links to Rzk Zulip (see [#131](https://github.com/rzk-lang/rzk/pull/131))
+  - Add `cabal update` to instructions (see [`3aa8fd3`](https://github.com/rzk-lang/rzk/commit/3aa8fd38902fc8cbb29f86122410d24398a15b0b))
+
 ## v0.6.6 — 2023-10-02
 
 - Fix builds on Windows (and macOS) (see [#121](https://github.com/rzk-lang/rzk/pull/121))

diff --git a/docs/docs/community.md b/docs/docs/community.md
@@ -0,0 +1,7 @@
+# Rzk Community
+
+## Chat
+
+A Zulip chat is available for all to join and chat about Rzk, including formalization projects, development of Rzk, and related projects:
+
+[Join Rzk Zulip](https://rzk-lang.zulipchat.com/register/){ .md-button .md-button--primary }
diff --git a/docs/docs/getting-started/install.md b/docs/docs/getting-started/install.md
@@ -7,26 +7,26 @@ These instructions will walk you through setting up Rzk using the "basic" setup
 1. Install [VS Code](https://code.visualstudio.com/).
 2. Launch VS Code and install the [`rzk` extension](https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting).
 3. Create a new file using "File > New Text File" (<kbd>Ctrl+N</kbd>). Click the `Select a language` prompt, type in `rzk`, and select "Literate Rzk Markdown".
-  ![VS Code rzk language selector.](../../assets/images/vscode-rzk-select-language.png)
+   ![VS Code rzk language selector.](../../assets/images/vscode-rzk-select-language.png)
 4. You should see the following popup:
-  ![VS Code rzk install prompt.](../../assets/images/vscode-rzk-install-prompt.png)
+   ![VS Code rzk install prompt.](../../assets/images/vscode-rzk-install-prompt.png)
 5. Click "Yes" button.
 6. While it is installing, you can paste the following literate Rzk program into the new file:
 
-    ````markdown
-    # Sample literate Rzk markdown
+   ````markdown
+   # Sample literate Rzk markdown
 
-    ```rzk
-    #lang rzk-1
-    
-    #define id (A : U)
-      : A -> A
-      := \ x -> x
-    ```
-    ````
+   ```rzk
+   #lang rzk-1
+
+   #define id (A : U)
+     : A -> A
+     := \ x -> x
+   ```
+   ````
 
 7. When the installation is done you should see the following popup:
-  ![VS Code rzk reload prompt.](../../assets/images/vscode-rzk-install-success-reload-prompt.png)
+   ![VS Code rzk reload prompt.](../../assets/images/vscode-rzk-install-success-reload-prompt.png)
 8. Click "Reload button".
 9. Save your file as `example.rzk.md`.
 10. Open local Terminal (<kbd>Ctrl+`</kbd>).
@@ -84,6 +84,7 @@ stack build && stack install
 To build and install with `cabal-install` from Hackage:
 
 ```sh
+cabal v2-update
 cabal v2-install rzk
 ```
 
@@ -99,4 +100,5 @@ cabal v2-build && cabal v2-install
 ### Nix
 
 !!! warning "Work-in-progress"
+
     To be done.
diff --git a/docs/docs/index.md b/docs/docs/index.md
@@ -15,3 +15,9 @@ Using such representation is motivated by automatic handling of binders and easi
 An important part of `rzk` is a tope layer solver, which is essentially a theorem prover for a part of the type theory. A related project, dedicated just to that part is available at <https://github.com/fizruk/simple-topes>. `simple-topes` supports used-defined cubes, topes, and tope layer axioms. Once stable, `simple-topes` will be merged into `rzk`, expanding the proof assistant to the type theory with shapes, allowing formalisations for (variants of) cubical, globular, and other geometric versions of HoTT.
 
 See the list of contributors at [CONTRIBUTORS.md](CONTRIBUTORS.md).
+
+## Discussing Rzk and getting help
+
+A Zulip chat is available for all to join and chat about Rzk, including formalization projects, development of Rzk, and related projects:
+
+[Join Rzk Zulip](https://rzk-lang.zulipchat.com/register/){ .md-button .md-button--primary }
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
@@ -33,6 +33,7 @@ nav:
       - Rendering Diagrams: reference/render.rzk.md
   - Examples:
     - Weak tope disjunction elimination: examples/recId.rzk.md
+  - Community: community.md
   - Tools:
     - Syntax Highlighting: tools/highlight.md
     - IDE support: tools/ide.md

diff --git a/nix/scripts.nix b/nix/scripts.nix
@@ -49,14 +49,11 @@ let scripts =
 
     release-rzk-playground = pkgs.writeShellApplication {
       name = "release-rzk-playground";
-      runtimeInputs = [ pkgs.nodejs_18 packages.build-rzk-js ];
+      runtimeInputs = [ pkgs.nodejs_18 ];
       text =
         let
           playground = "rzk-playground";
           playground-rzk-js = "${playground}/public/rzk.js";
-          config = "next.config.js";
-          configTmp = "${config}.tmp";
-          configBackup = "${config}.bk";
           release = "rzk-playground-release";
         in
         ''
@@ -67,26 +64,11 @@ let scripts =
           (
             cd ${playground}
             npm i
-                
-            # empty string by default
-                
-            : "''${BASEPATH:=""}"
-
-            # substitute basepath in config
-
-            < ${config} sed "s|'''|'$BASEPATH'|" > ${configTmp}
-            mv ${config} ${configBackup}
-            mv ${configTmp} ${config}
-
-            # restore backup anyway
-                
-            npm run build || true
-            mv ${configBackup} ${config}
           )
 
           rm -rf ${release}
           mkdir ${release}
-          cp -r ${playground}/out/* ${release}
+          cp -r ${playground}/dist/* ${release}
 
           printf "Wrote release files to '${release}'\n"
         '';

diff --git a/rzk-playground/.eslintrc.cjs b/rzk-playground/.eslintrc.cjs
@@ -0,0 +1,18 @@
+module.exports = {
+  root: true,
+  env: { browser: true, es2020: true },
+  extends: [
+    'eslint:recommended',
+    'plugin:@typescript-eslint/recommended',
+    'plugin:react-hooks/recommended',
+  ],
+  ignorePatterns: ['dist', '.eslintrc.cjs'],
+  parser: '@typescript-eslint/parser',
+  plugins: ['react-refresh'],
+  rules: {
+    'react-refresh/only-export-components': [
+      'warn',
+      { allowConstantExport: true },
+    ],
+  },
+}
diff --git a/rzk-playground/.eslintrc.json b/rzk-playground/.eslintrc.json
diff --git a/rzk-playground/app/layout.tsx b/rzk-playground/app/layout.tsx
diff --git a/rzk-playground/app/page.tsx b/rzk-playground/app/page.tsx
diff --git a/rzk-playground/index.html b/rzk-playground/index.html
@@ -0,0 +1,17 @@
+<!DOCTYPE html>
+<html lang="en">
+
+    <head>
+        <meta charset="UTF-8" />
+        <meta name="viewport"
+            content="width=device-width, initial-scale=1.0, maximum-scale=1.0, minimum-scale=1.0, user-scalable=no" />
+        <title>Try Rzk proof assistant!</title>
+    </head>
+
+    <body>
+        <script src='/rzk.js'> </script>
+        <div id="root"></div>
+        <script type="module" src="/src/main.tsx"></script>
+    </body>
+
+</html>