diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
index 12369d05c..9bdf67935 100644
--- 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
index 3518f0999..2b8940092 100644
--- 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
index 5a0ce5a32..40623508a 100644
--- a/README.md
+++ b/README.md
@@ -3,6 +3,7 @@
[](https://rzk-lang.github.io/rzk/)
[](https://rzk-lang.github.io/rzk/haddock/index.html)
[](https://github.com/rzk-lang/rzk/actions/workflows/ghcjs.yml)
+[](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:
+
+
## How to use `rzk`
For relatively small single-file formalisations, you can use the online playground at
@@ -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
index 39a65be92..58a024af4 100644
--- 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
new file mode 100644
index 000000000..46ab96599
--- /dev/null
+++ 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
index 11fa583c7..2f0276ab2 100644
--- 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" (Ctrl+N). Click the `Select a language` prompt, type in `rzk`, and select "Literate Rzk Markdown".
- 
+ 
4. You should see the following popup:
- 
+ 
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:
- 
+ 
8. Click "Reload button".
9. Save your file as `example.rzk.md`.
10. Open local Terminal (Ctrl+`).
@@ -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
index a6a8b1340..0ec6e3a0b 100644
--- 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 . `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
index 0860dfe4a..2792c41d2 100644
--- 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
index 8687cd2a4..a4248f020 100644
--- 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
new file mode 100644
index 000000000..d6c953795
--- /dev/null
+++ 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
deleted file mode 100644
index 73601b742..000000000
--- a/rzk-playground/.eslintrc.json
+++ /dev/null
@@ -1,5 +0,0 @@
-{
- "extends": [
- "next"
- ]
-}
\ No newline at end of file
diff --git a/rzk-playground/app/layout.tsx b/rzk-playground/app/layout.tsx
deleted file mode 100644
index 3df54bf87..000000000
--- a/rzk-playground/app/layout.tsx
+++ /dev/null
@@ -1,21 +0,0 @@
-import './globals.css'
-import type { Metadata } from 'next'
-import { Inter } from 'next/font/google'
-
-const inter = Inter({ subsets: ['latin'] })
-
-export const metadata: Metadata = {
- title: 'Try Rzk proof assistant!'
-}
-
-export default function RootLayout({
- children,
-}: {
- children: React.ReactNode
-}) {
- return (
-
- {children}
-
- )
-}
diff --git a/rzk-playground/app/page.tsx b/rzk-playground/app/page.tsx
deleted file mode 100644
index ef07d4f6f..000000000
--- a/rzk-playground/app/page.tsx
+++ /dev/null
@@ -1,136 +0,0 @@
-'use client';
-
-import { useCallback, useEffect, useState } from 'react';
-import Editor from '../components/editor/Editor';
-import Script from 'next/script';
-import { Resizable } from 're-resizable';
-import React from 'react';
-import * as rzk from '../src/rzk';
-import { KeyBindProvider, ShortcutType } from 'react-keybinds';
-import dynamic from 'next/dynamic';
-
-var typecheckedOnStart = false
-
-declare var window: Window & typeof globalThis;
-
-function HomeNoSSR() {
- const [message, setMessage] = useState("Starting...");
-
- const [windowHeight, setWindowHeight] = useState(window.innerHeight)
- const [needTypecheck, setNeedTypecheck] = useState(false)
-
- useEffect(() => {
- const handleWindowResize = () => {
- setWindowHeight(window.innerHeight)
- };
-
- window.addEventListener('resize', handleWindowResize);
-
- return () => {
- window.removeEventListener('resize', handleWindowResize);
- };
- }, []);
-
- const [text, setText] = useState("")
-
- const typecheck = useCallback(() => {
- const result = rzk.typecheck(text)
- if (result.status == 'ok') {
- setMessage(`Everything is OK!`)
- } else {
- setMessage(result.result)
- }
- }, [text])
-
- useEffect(() => {
- function checkFlag() {
- if ((!((window as any).rzkTypecheck_) || (text === "")) && !typecheckedOnStart) {
- console.warn("something bad")
- console.warn((window as any).rzkTypecheck_)
- window.setTimeout(checkFlag, 100); /* this checks the flag every 100 milliseconds*/
- } else if (!typecheckedOnStart) {
- typecheck()
- typecheckedOnStart = true
- }
- }
-
- if (!typecheckedOnStart) {
- checkFlag();
- }
- }, [typecheck, text])
-
- useEffect(() => {
- if (needTypecheck) {
- typecheck()
- setNeedTypecheck(false)
- }
- }, [setNeedTypecheck, needTypecheck, typecheck])
-
- const KEYBINDINGS: ShortcutType[] =
- [
- {
- keys: {
- Mac: ['Shift', 'Enter'],
- Windows: ['Shift', 'Enter'],
- Linux: ['Shift', 'Enter'],
- },
- label: 'Test command',
- callback: () => {
- setNeedTypecheck(true)
- },
- },
- ]
- ;
-
- const [outputHeight, setOutputHeight] = useState(windowHeight * 30 / 100)
- const [editorHeight, setEditorHeight] = useState(windowHeight * 70 / 100)
-
- return (
-
-
-
-
-
-
-
-
-
{
- setOutputHeight(outputHeight + d.height)
- }}
- onResize={(_e, _direction, _ref, d) => {
- setEditorHeight(window.innerHeight - (outputHeight + d.height))
- }}
- style={{ padding: '20px' }}
- >
-
- {message}
-
-
-
+
+
+
+
+
+
{
+ setOutputHeight(outputPanelHeight + delta.height)
+ }}
+ onResize={(_event, _direction, _elementRef, delta) => {
+ setEditorHeight(window.innerHeight - (outputPanelHeight + delta.height))
+ }}
+ style={{ padding: '20px' }}
+ >
+
+ {output}
+
+
+