diff --git a/.github/workflows/binaries.yml b/.github/workflows/binaries.yml new file mode 100644 index 000000000..d35f621bc --- /dev/null +++ b/.github/workflows/binaries.yml @@ -0,0 +1,48 @@ +# Inspired by https://github.com/JustusAdam/create-haskell-binaries-with-actions + +name: Create Release Binaries +on: + release: + types: [published] + +jobs: + build: + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-latest, windows-latest, macos-latest] + + steps: + - uses: actions/checkout@v3 + + - name: Cache Stack files + uses: actions/cache@v3 + env: + cache-name: cache-tools-and-libraries + with: + path: ~/.stack + key: ${{ runner.os }}-ca-${{ env.cache-name }}-${{ hashFiles('**/stack.yaml.lock') }} + restore-keys: | + ${{ runner.os }}-ca-${{ env.cache-name }}- + ${{ runner.os }}-ca- + ${{ runner.os }}- + + - name: Build the project + run: stack build + + - name: Tar and strip the binary + run: | + export PROGRAM=program + cp `stack exec -- which $PROGRAM` $PROGRAM + tar -cavf program.tar.gz $PROGRAM + + - name: Upload assets + id: upload-release-asset + uses: actions/upload-release-asset@v1 + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + with: + upload_url: ${{ github.event.release.upload_url }} + asset_path: ./program.tar.gz + asset_name: rzk-${{ github.ref_name }}-${{ runner.os }}-${{ runner.arch }}.tar.gz + asset_content_type: application/tar.gz diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml index 42d62dbd2..6b44059d4 100644 --- a/.github/workflows/ghcjs.yml +++ b/.github/workflows/ghcjs.yml @@ -73,6 +73,7 @@ jobs: folder: dist target-folder: ${{ github.ref_name }} clean: false + single-commit: true - name: "πŸ“˜ Publish JS \"binaries\"" if: ${{ github.ref_name == 'main' && github.event_name == 'push' }} @@ -81,3 +82,4 @@ jobs: token: ${{ secrets.GITHUB_TOKEN }} folder: dist clean: false + single-commit: true diff --git a/.github/workflows/haddock.yml b/.github/workflows/haddock.yml index dbc877247..d0cfd8bb7 100644 --- a/.github/workflows/haddock.yml +++ b/.github/workflows/haddock.yml @@ -59,3 +59,4 @@ jobs: github_token: ${{ secrets.GITHUB_TOKEN }} folder: dist/haddock target-folder: haddock + single-commit: true diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml index a4827773d..cff1cdb07 100644 --- a/.github/workflows/mkdocs.yml +++ b/.github/workflows/mkdocs.yml @@ -17,6 +17,12 @@ jobs: - name: πŸ“₯ Checkout repository uses: actions/checkout@v3 + - name: πŸ”¨ Install rzk proof assistant + uses: jaxxstorm/action-install-gh-release@v1.10.0 + with: + repo: fizruk/rzk + rename-to: rzk + - name: πŸ”¨ Build MkDocs uses: Tiryoh/actions-mkdocs@v0 with: @@ -37,6 +43,7 @@ jobs: folder: dist target-folder: ${{ github.ref_name }} clean: false + single-commit: true - name: πŸ“˜ Publish Generated MkDocs if: ${{ github.ref_name == 'main' }} @@ -45,3 +52,4 @@ jobs: github_token: ${{ secrets.GITHUB_TOKEN }} folder: dist clean: false + single-commit: true diff --git a/.gitignore b/.gitignore index f61a4d7ed..364f2fae6 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ docs/out/ dist dist-* cabal-dev +build *.o *.hi *.hie @@ -25,4 +26,6 @@ cabal.project.local~ .ghc.environment.* docs/site result -.direnv \ No newline at end of file +.direnv +venv +__pycache__ diff --git a/docs/custom_theme/js/rzk.js b/docs/custom_theme/js/rzk.js index 2fd48cf5c..c4c93ea5e 100644 --- a/docs/custom_theme/js/rzk.js +++ b/docs/custom_theme/js/rzk.js @@ -2,107 +2,162 @@ Language: rzk Author: Nikolai Kudasov Category: functional -Website: https://fizruk.github.io/rzk/split.html +Website: https://github.com/fizruk/highlightjs-rzk */ hljs.registerLanguage('rzk', -function(hljs) { - const COMMENT = { variants: [ - hljs.COMMENT('--', '$'), - ] }; - const TYPE = { - begin: /CUBE|TOPE|U|βˆ‘|2/, - className: "type" - }; - const SHAPE = { - begin: /TOP|BOT/, - className: "number" - }; - const BUILTIN = { - begin: /recOR|recBOT|idJ|refl/, - className: "title.class" - }; - const IDENT_RE = /[^\(\)\[\]\{\}\s]+/; - const POINT_VAR = { - begin: [ - /\{/, - /\s*/, - IDENT_RE, - /\s*:\s*/, - /[^\}|]+/, - /\s+\|\s+/, - /[^\}|]+/, - /\}/ - ], - className: { - 3: "variable", - // 5: "type", - 7: "number" - }, - contains: [ COMMENT, TYPE, SHAPE, BUILTIN ] - }; - const CONTEXTS = { variants: [ - { + function (hljs) { + const COMMENT = { + variants: [ + hljs.COMMENT('--', '$'), + ] + }; + const TYPE = { + begin: /(\b(CUBE|TOPE|U|𝒰|Sigma|1|2|πŸ™|𝟚)\b|(βˆ‘|Ξ£))/, + className: "type" + }; + const SHAPE = { + begin: /((\*_1|⋆)|\b(0_2|1_2|TOP|BOT)\b|(===|<=|\\\/ | \/\\|⊀|βŠ₯))/, + className: "number" + }; + const BUILTIN = { + begin: /\b(recOR|rec∨|recBOT|recβŠ₯|idJ|refl|first|second|π₁|Ο€β‚‚)\b/, + className: "title.class" + }; + const IDENT_RE = /[^\-\?\!\.\\;:,#\"\]\[\)\(\}\{><\| \t\n\r][^\.\\;:,#\"\]\[\)\(\}\{><\| \t\n\r]*/; + const MANY_IDENT_RE = /[^\-\?\!\.\\;:,#\"\]\[\)\(\}\{><\| \t\n\r][^\.\\;:,#\"\]\[\)\(\}\{><\|]*/; + const POINT_VAR = { begin: [ - /\(/, + /\{/, /\s*/, IDENT_RE, - /\s+:/ + /\s*:\s*/, + /[^\}|]+/, + /\s+\|\s+/, + /[^\}|]+/, + /\}/ ], - className: { 3: "variable" }, - }, - { - begin: [ - /\[/, - /\s*/, - /[^\|]+/, - /\s+\|->/ - ], - className: { 3: "number" } - }, - { - begin: /_\{/, - end: /\}/, - scope: "string" - } - ], - contains: [ - 'self', COMMENT, POINT_VAR, TYPE, SHAPE, BUILTIN - ] - }; - return { - name: 'rzk', - aliases: [ 'rzk' ], - illegal: ' + {{ super() }} {% endblock %} diff --git a/docs/docs/examples/hom.md b/docs/docs/examples/hom.rzk.md similarity index 100% rename from docs/docs/examples/hom.md rename to docs/docs/examples/hom.rzk.md diff --git a/docs/docs/examples/section4.md b/docs/docs/examples/section4.rzk.md similarity index 100% rename from docs/docs/examples/section4.md rename to docs/docs/examples/section4.rzk.md diff --git a/docs/docs/examples/short.md b/docs/docs/examples/short.rzk.md similarity index 100% rename from docs/docs/examples/short.md rename to docs/docs/examples/short.rzk.md diff --git a/docs/docs/examples/test.md b/docs/docs/examples/test.rzk.md similarity index 100% rename from docs/docs/examples/test.md rename to docs/docs/examples/test.rzk.md diff --git a/docs/docs/rzk-1/introduction.md b/docs/docs/rzk-1/introduction.rzk.md similarity index 100% rename from docs/docs/rzk-1/introduction.md rename to docs/docs/rzk-1/introduction.rzk.md diff --git a/docs/docs/rzk-1/recId.md b/docs/docs/rzk-1/recId.rzk.md similarity index 100% rename from docs/docs/rzk-1/recId.md rename to docs/docs/rzk-1/recId.rzk.md diff --git a/docs/docs/rzk-1/render.md b/docs/docs/rzk-1/render.md deleted file mode 100644 index a1d9fd153..000000000 --- a/docs/docs/rzk-1/render.md +++ /dev/null @@ -1,415 +0,0 @@ -# Rendering Diagrams - -Starting from version `0.3.0`, `rzk` supports rendering of topes, types, and terms as diagrams. - -This is a literate `rzk` file: - -```rzk -#lang rzk-1 -``` - -To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`): - -```rzk -#set-option "render" = "svg" -- enable rendering in SVG -``` - -Rendering is completely automatic, and works in the following situations: - -1. Mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes; -2. Type of mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes. -3. Mappings from a shape that is a section of an existing shape. - -The rendering assigns the following colors: - -- purple is assigned for parameters (context) variables; -- blue is used for fillings for types (e.g. for `hom` and `hom2`); -- red is used for terms (e.g. `Segal-comp-witness`); -- orange is used for shapes in the tope layer; -- grey is used for discarded parts of a (larger) mapping (e.g. when extracting a diagonal/face from a larger shape). - -The SVG pictures can be inserted directly into `.md` files before a corresponding `rzk` code block. At the bottom of a markdown file, you might want to add stylization, e.g.: - -```html - - - - - - - - - - - - -``` - -## Examples - -### Visualising Simplicial Topes - -Topes are visualised with **orange** color: - - - - - - - - - - - β€’ - β€’ - β€’ - - -```rzk --- 2-simplex -#def Δ² : (2 * 2) -> TOPE - := \(t, s) -> s <= t -``` -

-Boundary of a tope: - - - - - - - - - β€’ - β€’ - β€’ - - -```rzk --- boundary of a 2-simplex -#def βˆ‚Ξ”Β² : Δ² -> TOPE - := \(t, s) -> s === 0_2 \/ t === 1_2 \/ s === t -``` - -The busiest tope diagram involves the entire 3D cube: -

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - β€’ - β€’ - β€’ - β€’ - β€’ - β€’ - β€’ - β€’ - - -```rzk --- 3-dim cube -#def 2Β³ : (2 * 2 * 2) -> TOPE - := \_ -> TOP -``` -


- - - - - - - - - - - - - - - - - - - - - - β€’ - β€’ - β€’ - β€’ - - -```rzk --- 3-simplex -#def Δ³ : (2 * 2 * 2) -> TOPE - := \((t1, t2), t3) -> t3 <= t2 /\ t2 <= t1 -``` - -

-### Visualising Simplicial Types - -Types are visualised with **blue** color. Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a type is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color. - - - - - x - y - - -```rzk --- [RS17, Definition 5.1] --- The type of arrows in A from x to y. -#def hom - (A : U) -- A type. - (x y : A) -- Two points in A. - : U -- (hom A x y) is a 1-simplex (an arrow) - := (t : 2) -> A [ -- in A where - t === 0_2 |-> x, -- * the left endpoint is exactly x - t === 1_2 |-> y -- * the right endpoint is exactly y - ] -``` - - - - - f - f - h - h - g - g - x - y - z - - -```rzk --- [RS17, Definition 5.2] --- the type of commutative triangles in A -#def hom2 - (A : U) -- A type. - (x y z : A) -- Three points in A. - (f : hom A x y) -- An arrow in A from x to y. - (g : hom A y z) -- An arrow in A from y to z. - (h : hom A x z) -- An arrow in A from x to z. - : U -- (hom2 A x y z f g h) is a 2-simplex (triangle) - := { (t1, t2) : Δ² } -> A [ -- in A where - t2 === 0_2 |-> f t1, -- * the top edge is exactly f, - t1 === 1_2 |-> g t2, -- * the right edge is exactly g, and - t2 === t1 |-> h t2 -- * the diagonal is exactly h - ] -``` - -### Visualising Terms of Simplicial Types - -Terms (with non-trivial labels) are visualised with **red** color (you can see a detailed label on hover). Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a term is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color. - -We can visualise terms that fill a shape: - - - second a (second xβ‚‚, first xβ‚‚) - - second a (first xβ‚‚, second xβ‚‚) - - f - f - f - f - first a (second (first xβ‚‚, second xβ‚‚)) - - g - g - g - g - x - y - y - z - - -```rzk -#def square - (A : U) - (x y z : A) - (f : hom A x y) - (g : hom A y z) - (h : hom A x z) - (a : Sigma (h' : hom A x z), hom2 A x y z f g h') - : (2 * 2) -> A - := \(t, s) -> recOR( s <= t |-> second a (t, s) , t <= s |-> second a (s, t)) -``` - -If a term is extracted as a part of a larger shape, generally, the whole shape will be shown (in gray): - - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - first a (second xβ‚‚) - - first a (second xβ‚‚) - - f - f - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - second a xβ‚‚ - - first a (second xβ‚‚) - - y - y - first a (second xβ‚‚) - - z - z - first a (second xβ‚‚) - - x - y - y - z - y - z - - -```rzk -#def face - (A : U) - (x y z : A) - (f : hom A x y) - (a : Sigma (g : hom A y z), {((t1, t2), t3) : 2 * 2 * 2 | t3 <= t1 \/ t2 <= t1} -> A [ t1 === 0_2 |-> f t2, t1 === 1_2 |-> g t3 ]) - : Δ² -> A - := \(t, s) -> second a ((t, t), s) -``` - - - - - - - - - - - - - - diff --git a/docs/docs/rzk-1/render.rzk.md b/docs/docs/rzk-1/render.rzk.md new file mode 100644 index 000000000..c006818b4 --- /dev/null +++ b/docs/docs/rzk-1/render.rzk.md @@ -0,0 +1,183 @@ +# Rendering Diagrams + +Starting from version `0.3.0`, `rzk` supports rendering of topes, types, and terms as diagrams. + +This is a literate `rzk` file: + +```rzk +#lang rzk-1 +``` + +To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`): + +```rzk +#set-option "render" = "svg" -- enable rendering in SVG +``` + +Rendering is completely automatic, and works in the following situations: + +1. Mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes; +2. Type of mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes. +3. Mappings from a shape that is a section of an existing shape. + +The rendering assigns the following colors: + +- purple is assigned for parameters (context) variables; +- blue is used for fillings for types (e.g. for `hom` and `hom2`); +- red is used for terms (e.g. `Segal-comp-witness`); +- orange is used for shapes in the tope layer; +- grey is used for discarded parts of a (larger) mapping (e.g. when extracting a diagonal/face from a larger shape). + +The SVG pictures can be inserted directly into `.md` files before a corresponding `rzk` code block. At the bottom of a markdown file, you might want to add stylization, e.g.: + +```html + + + + + + + + + + + + +``` + +## Examples + +### Visualising Simplicial Topes + +Topes are visualised with **orange** color: + +```rzk +-- 2-simplex +#def Δ² : (2 * 2) -> TOPE + := \(t, s) -> s <= t +``` +

+Boundary of a tope: + +```rzk +-- boundary of a 2-simplex +#def βˆ‚Ξ”Β² : Δ² -> TOPE + := \(t, s) -> s === 0_2 \/ t === 1_2 \/ s === t +``` + +The busiest tope diagram involves the entire 3D cube: +

+ +```rzk +-- 3-dim cube +#def 2Β³ : (2 * 2 * 2) -> TOPE + := \_ -> TOP +``` +


+ +```rzk +-- 3-simplex +#def Δ³ : (2 * 2 * 2) -> TOPE + := \((t1, t2), t3) -> t3 <= t2 /\ t2 <= t1 +``` + +

+### Visualising Simplicial Types + +Types are visualised with **blue** color. Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a type is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color. + +```rzk +-- [RS17, Definition 5.1] +-- The type of arrows in A from x to y. +#def hom + (A : U) -- A type. + (x y : A) -- Two points in A. + : U -- (hom A x y) is a 1-simplex (an arrow) + := (t : 2) -> A [ -- in A where + t === 0_2 |-> x, -- * the left endpoint is exactly x + t === 1_2 |-> y -- * the right endpoint is exactly y + ] +``` + +```rzk +-- [RS17, Definition 5.2] +-- the type of commutative triangles in A +#def hom2 + (A : U) -- A type. + (x y z : A) -- Three points in A. + (f : hom A x y) -- An arrow in A from x to y. + (g : hom A y z) -- An arrow in A from y to z. + (h : hom A x z) -- An arrow in A from x to z. + : U -- (hom2 A x y z f g h) is a 2-simplex (triangle) + := { (t1, t2) : Δ² } -> A [ -- in A where + t2 === 0_2 |-> f t1, -- * the top edge is exactly f, + t1 === 1_2 |-> g t2, -- * the right edge is exactly g, and + t2 === t1 |-> h t2 -- * the diagonal is exactly h + ] +``` + +### Visualising Terms of Simplicial Types + +Terms (with non-trivial labels) are visualised with **red** color (you can see a detailed label on hover). Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a term is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color. + +We can visualise terms that fill a shape: + +```rzk +#def square + (A : U) + (x y z : A) + (f : hom A x y) + (g : hom A y z) + (h : hom A x z) + (a : Sigma (h' : hom A x z), hom2 A x y z f g h') + : (2 * 2) -> A + := \(t, s) -> recOR( s <= t |-> second a (t, s) , t <= s |-> second a (s, t)) +``` + +If a term is extracted as a part of a larger shape, generally, the whole shape will be shown (in gray): + +```rzk +#def face + (A : U) + (x y z : A) + (f : hom A x y) + (a : Sigma (g : hom A y z), {((t1, t2), t3) : 2 * 2 * 2 | t3 <= t1 \/ t2 <= t1} -> A [ t1 === 0_2 |-> f t2, t1 === 1_2 |-> g t3 ]) + : Δ² -> A + := \(t, s) -> second a ((t, t), s) +``` + + + + + + + + + + + + + + diff --git a/docs/docs/rzk-1/sections.md b/docs/docs/rzk-1/sections.rzk.md similarity index 100% rename from docs/docs/rzk-1/sections.md rename to docs/docs/rzk-1/sections.rzk.md diff --git a/docs/docs/tools/highlight.md b/docs/docs/tools/highlight.md new file mode 100644 index 000000000..e5e4205a1 --- /dev/null +++ b/docs/docs/tools/highlight.md @@ -0,0 +1,8 @@ +# Syntax Highlighting + +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 diff --git a/docs/generate_svgs.py b/docs/generate_svgs.py new file mode 100644 index 000000000..83eb817dc --- /dev/null +++ b/docs/generate_svgs.py @@ -0,0 +1,46 @@ +import re +import logging +import subprocess + +from mkdocs.structure.pages import Page +from mkdocs.structure.files import Files +from mkdocs.config.defaults import MkDocsConfig + + +logger = logging.getLogger('mkdocs') +rzk_code_block = re.compile(r'(^```\s*rzk[^\n]*\s+(.*?)\s+^```)', flags=re.MULTILINE | re.DOTALL) +svg_element = re.compile(r'^()', flags=re.MULTILINE | re.DOTALL) +rzk_installed = True + +try: + # Capture output to prevent logging usage + subprocess.run('rzk', capture_output=True) +except FileNotFoundError: + logger.warn('Rzk executable not found') + rzk_installed = False + + +def on_page_markdown(md: str, page: Page, config: MkDocsConfig, files: Files) -> str: + if not page.file.src_uri.endswith('.rzk.md'): return md + if not rzk_installed: return md + # Some snippets can depend on terms defined in previous snippets, so we need to store them all + previous_snippets = ['#lang rzk-1\n#set-option "render" = "svg"\n\n'] + # Since each snippet will contain previous ones, the previously printed SVGs should not be repeated + previous_svgs: set[str] = set() + code_blocks = rzk_code_block.findall(md) + for (fenced_block, code) in code_blocks: + previous_snippets.append(code.replace('#lang rzk-1', '')) + full_code = '\n'.join(previous_snippets).encode() + process = subprocess.run('rzk typecheck', capture_output=True, input=full_code) + if process.returncode != 0: continue + + output = process.stderr.decode() + svgs: list[str] = svg_element.findall(output) + # One snippet might have more than one diagram, so we shouldn't just use svgs[-1] + # However, there is probably a more efficient way than iterating over all matches everytime + for svg in svgs: + if svg in previous_svgs: continue + previous_svgs.add(svg) + md = md.replace(fenced_block, svg + '\n\n' + fenced_block) + + return md diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index 98c413bb0..20e250b9f 100644 --- a/docs/mkdocs.yml +++ b/docs/mkdocs.yml @@ -8,6 +8,7 @@ nav: - Rendering Diagrams: rzk-1/render.md - Weak tope disjunction elimination: rzk-1/recId.md - Tools: + - Syntax Highlighting: tools/highlight.md - IDE support: tools/ide.md - Continuous Verification: tools/continuous.md - Related Projects: @@ -24,3 +25,6 @@ theme: custom_dir: custom_theme/ extra_css: - https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.7.0/styles/default.min.css + +hooks: + - generate_svgs.py diff --git a/docs/requirements.txt b/docs/requirements.txt index 3a4655e33..5885f5e86 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -1 +1,2 @@ +mkdocs python-markdown-math diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index 49e06a096..d581f2b04 100644 --- a/rzk/ChangeLog.md +++ b/rzk/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.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 )); + ## 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. diff --git a/rzk/RzkLexer/README.md b/rzk/RzkLexer/README.md new file mode 100644 index 000000000..8ed1c9932 --- /dev/null +++ b/rzk/RzkLexer/README.md @@ -0,0 +1,64 @@ +# Pygments higlighter for Rzk + +This is a simple [Pygments](https://pygments.org) higlighter for Rzk, which can be used with [`minted` package](https://www.ctan.org/pkg/minted) when writing rzk code in LaTeX. + +## How to use + +### Install + +Clone this repository, and install the highlighter using [`pip` installer](https://pip.pypa.io/en/stable/): + +```sh +git clone https://github.com/fizruk/rzk.git +cd rzk # enter repository root +cd rzk/RzkLexer # enter the directory with RzkLexer +pip install . # install using pip +``` + +### Use in LaTeX + +In your LaTeX document: + +1. Include `minted` package: + +```tex +\package{minted} +``` + +2. Use `minted` environment with `rzk` language, for example: + +```tex +\begin{frame}[fragile] + \frametitle{\textsc{Rzk} highlighting in LaTeX with \texttt{minted}} + +A basic example: + +\tiny +\begin{minted}[linenos,frame=leftline,mathescape]{rzk} +#lang rzk-1 + +#section path-algebra + +#variable A : U +#variables x y z : A + +-- path reversal +#define rev uses (A x y) + (p : x = y) -- A path from x to y in A. + : y = x -- The reversal will be defined by path induction on p. + := idJ(A, x, \y' p' -> y' = x, refl, y, p) + +-- path composition by induction on the second path +#define concat + (p : x = y) -- A path from x to y in A. + (q : y = z) -- A path from y to z in A. + : (x = z) + := idJ(A, y, \z' q' -> (x = z'), p, z, q) + +#end path-algebra +\end{minted} + +\end{frame} +``` + +![Rendering rzk code in LaTeX (demo).](images/latex-highlighting-demo.png) \ No newline at end of file diff --git a/rzk/RzkLexer/images/latex-highlighting-demo.png b/rzk/RzkLexer/images/latex-highlighting-demo.png new file mode 100644 index 000000000..46029d916 Binary files /dev/null and b/rzk/RzkLexer/images/latex-highlighting-demo.png differ diff --git a/rzk/RzkLexer/rzklexer/__init__.py b/rzk/RzkLexer/rzklexer/__init__.py new file mode 100644 index 000000000..900ee237e --- /dev/null +++ b/rzk/RzkLexer/rzklexer/__init__.py @@ -0,0 +1,43 @@ +import pygments.lexer +from pygments.lexer import bygroups +from pygments.token import * +__all__ = ["RzkLexer"] +class RzkLexer(pygments.lexer.RegexLexer): + name = 'Rzk' + aliases = ['rzk'] + filenames = ['*.rzk'] + url = 'https://github.com/fizruk/rzk' + KEYWORDS = ['as', 'uses'] + def get_tokens_unprocessed(self, text): + for index, token, value in super(RzkLexer,self).get_tokens_unprocessed(text): + if token is Name and value in self.KEYWORDS: + yield index, Keyword, value + else: + yield index, token, value + tokens = { + 'root': [ + (r'--.*\n', Comment), + (r'\{-((.)(?\?\[\\\]\{\|\}][^\t\n\r !"#\(\),\.;:<>\?\[\\\]\{\|\}]*)', + bygroups(Name.Decorator, Name.Entity)), + (r' = | \* | === | <= | /\\ | \\/ ', Operator), + (r'(\(\s*)((([^\t\n\r !"#\(\),-\.;:<>\?\[\\\]\{\|\}][^\t\n\r !"#\(\),\.;:<>\?\[\\\]\{\|\}]*)\s*)+)(:)', + bygroups(Punctuation, Name.Variable, None, None, Punctuation)), + (r'(\\\s*)((([^\t\n\r !"#\(\),-\.;:\\\/=<>\?\[\\\]\{\|\}][^\t\n\r !"#\(\),\.;:<>\?\[\\\]\{\|\}]*)\s*)+)', + bygroups(Punctuation, Name.Variable)), + (r'(;|:|:=|\(|\)|_\b|,|\{|\||\}|\||\[|\]|<|>|\\|->)', Punctuation), + (r'((#assume|#variables|#variable)\b\s+)([^:]+)', + bygroups(Keyword.Declaration, None, Name.Variable)), + (r'((#postulate|#define|#def)\b\s+)([^\t\n\r !"#\(\),-\.;:<>\?\[\\\]\{\|\}][^\t\n\r !"#\(\),\.;:<>\?\[\\\]\{\|\}]*\s+)((uses\s+)(\()([^\(\)]+)(\)))?', + bygroups(Keyword, None, Name.Function, None, Keyword, Punctuation, Name.Variable, Punctuation)), + (r'"((.)(?\?\[\\\]\{\|\}])((.)(?\[\\\]\{\|\}]))*', Name), + (r'\?', Name), + (r'[a-zA-Z]([a-zA-Z]|\d|_|\')*', Name) + ] + } diff --git a/rzk/RzkLexer/setup.py b/rzk/RzkLexer/setup.py new file mode 100644 index 000000000..36d56507c --- /dev/null +++ b/rzk/RzkLexer/setup.py @@ -0,0 +1,11 @@ +from setuptools import setup, find_packages + +setup ( + name='rzklexer', + packages=find_packages(), + entry_points = + """ + [pygments.lexers] + rzklexer = rzklexer:RzkLexer + """, +) diff --git a/rzk/package.yaml b/rzk/package.yaml index 399e6c6b3..c86345ed9 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -1,5 +1,5 @@ name: rzk -version: 0.4.0 +version: 0.4.1 github: "fizruk/rzk" license: BSD3 author: "Nikolai Kudasov" @@ -24,6 +24,7 @@ dependencies: - bifunctors - mtl - template-haskell +- optparse-generic ghc-options: - -Wall diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index 7ab52c146..d26c8afd9 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -1,13 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.2. +-- This file has been generated from package.yaml by hpack version 0.35.1. -- -- see: https://github.com/sol/hpack --- --- hash: 7855530fcdfd2a28c4ea3654677ed2d18f83d419f5d1c173f4bb44a915464c06 name: rzk -version: 0.4.0 +version: 0.4.1 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types @@ -51,6 +49,7 @@ library , base >=4.7 && <5 , bifunctors , mtl + , optparse-generic , template-haskell default-language: Haskell2010 @@ -66,6 +65,7 @@ executable rzk , base >=4.7 && <5 , bifunctors , mtl + , optparse-generic , rzk , template-haskell default-language: Haskell2010 @@ -83,6 +83,7 @@ test-suite rzk-test , base >=4.7 && <5 , bifunctors , mtl + , optparse-generic , rzk , template-haskell default-language: Haskell2010 diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs index 84a11ff3d..33f65b832 100644 --- a/rzk/src/Rzk/Main.hs +++ b/rzk/src/Rzk/Main.hs @@ -1,18 +1,37 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} module Rzk.Main where import Control.Monad (forM) -import System.Environment (getArgs) +import Data.Version (showVersion) +import Options.Generic import System.Exit (exitFailure) import qualified Language.Rzk.Syntax as Rzk +import Paths_rzk (version) import Rzk.TypeCheck +data Command + = Typecheck [FilePath] + | Version + deriving (Generic, Show, ParseRecord) + main :: IO () -main = do - args <- getArgs - case args of - "typecheck" : paths -> do - modules <- forM paths $ \path -> do +main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categories" >>= \case + Typecheck paths -> do + modules <- case paths of + -- if no paths are given β€” read from stdin + [] -> do + result <- Rzk.parseModule <$> getContents + case result of + Left err -> do + putStrLn ("An error occurred when parsing stdin") + error err + Right rzkModule -> return [("", rzkModule)] + -- otherwise β€” parse all given files in given order + _ -> forM paths $ \path -> do putStrLn ("Loading file " <> path) result <- Rzk.parseModule <$> readFile path case result of @@ -20,19 +39,17 @@ main = do putStrLn ("An error occurred when parsing file " <> path) error err Right rzkModule -> return (path, rzkModule) - case defaultTypeCheck (typecheckModulesWithLocation modules) of - Left err -> do - putStrLn "An error occurred when typechecking!" - putStrLn $ unlines - [ "Type Error:" - , ppTypeErrorInScopedContext' err - ] - exitFailure - Right () -> putStrLn "Everything is ok!" - _ -> ppUsage + case defaultTypeCheck (typecheckModulesWithLocation modules) of + Left err -> do + putStrLn "An error occurred when typechecking!" + putStrLn $ unlines + [ "Type Error:" + , ppTypeErrorInScopedContext' err + ] + exitFailure + Right () -> putStrLn "Everything is ok!" -ppUsage :: IO () -ppUsage = putStrLn "rzk typecheck FILE" + Version -> putStrLn (showVersion version) typecheckString :: String -> Either String String typecheckString moduleString = do diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index e3e9919f1..23be70686 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -2936,7 +2936,7 @@ renderCube -> (String -> Maybe RenderObjectData) -> String renderCube camera rotY renderDataOf' = unlines $ filter (not . null) - [ "" + [ "" , intercalate "\n" [ " show x1 <> " " <> show y1 <> " L " <> show x2 <> " " <> show y2