Merge branch 'release-v0.4.1'

* release-v0.4.1:
  Bump version and update changelog
  Add rzk version command
  Add action to release binaries
  Remove hardcoded tag for the release
  Configure the SVG generator to only run on .rzk.md
  Combine both classes into one
  Move styles from Haskell source code to HTML
  Enable squashing gh-pages history
  Add a step to setup rzk before MkDocs
  Remove hardcoded diagrams from the markdown source
  Add a MkDocs hook to automatically generate SVGs
  Add MkDocs to Python's list of requirements
  Add Python venv to gitignore
  Read stdin when no filepaths are given
  Improve slightly the Pygments highlighter
  Fix Pygments highlighter for params
  Fix Pygments highlighter for lambda abstraction
  Add information about highlighting to the docs
  Add Pygments highlighting
  Update highlighting for rzk v0.4.0

.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

.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

.github/workflows/haddock.yml

@@ -59,3 +59,4 @@ jobs:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist/haddock
           target-folder: haddock
+          single-commit: true

.github/workflows/mkdocs.yml

@@ -17,6 +17,12 @@ jobs:
       - name: 📥 Checkout repository
         uses: actions/checkout@v3
 
+      - name: 🔨 Install rzk proof assistant
+        uses: jaxxstorm/[email protected]
+        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

.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
+.direnv
+venv
+__pycache__

docs/custom_theme/js/rzk.js

@@ -2,107 +2,162 @@
 Language: rzk
 Author: Nikolai Kudasov <[email protected]>
 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: '</',
-    contains: [
-      COMMENT,
-      POINT_VAR,
-      CONTEXTS,
-      TYPE,
-      SHAPE,
-      BUILTIN,
-      {
-        begin: [
-          /#lang/,
-          /\s+/,
-          /rzk-1/
-        ],
-        className: {
-          1: "meta",
-          3: "keyword"
-        }
+      className: {
+        3: "variable",
+        // 5: "type",
+        7: "number"
       },
-      {
-        begin: [
-          /#def/,
-          /\s+/,
-          IDENT_RE,
-        ],
-        className: {
-          1: "meta",
-          3: "title.function"
+      contains: [COMMENT, TYPE, SHAPE, BUILTIN]
+    };
+    const CONTEXTS = {
+      variants: [
+        {
+          begin: /\b(as)\b/,
+          className: "keyword"
+        },
+        {
+          begin: [
+            /\(/,
+            /\s*/,
+            MANY_IDENT_RE,
+            /\s+:/
+          ],
+          className: { 3: "variable" },
+        },
+        {
+          begin: /_\{/,
+          end: /\}/,
+          scope: "string"
+        }
+      ],
+      contains: [
+        'self', COMMENT, POINT_VAR, TYPE, SHAPE, BUILTIN
+      ]
+    };
+    return {
+      name: 'rzk',
+      aliases: ['rzk'],
+      illegal: '</',
+      contains: [
+        COMMENT,
+        POINT_VAR,
+        CONTEXTS,
+        TYPE,
+        SHAPE,
+        BUILTIN,
+        {
+          begin: [
+            /#lang/,
+            /\s+/,
+            /rzk-1/
+          ],
+          className: {
+            1: "meta",
+            3: "keyword"
+          }
+        },
+        {
+          begin: [
+            /(#def|#define|#postulate)\b/,
+            /\s+/,
+            IDENT_RE,
+            /\s+/,
+            /\buses\b/,
+            /\s*\(\s*/,
+            MANY_IDENT_RE,
+            /\)/
+          ],
+          className: {
+            1: "meta",
+            3: "title.function",
+            5: "meta",
+            7: "variable"
+          }
+        },
+        {
+          begin: [
+            /(#def|#define|#postulate)\b/,
+            /\s+/,
+            IDENT_RE
+          ],
+          className: {
+            1: "meta",
+            3: "title.function"
+          }
+        },
+        {
+          begin: [
+            /(#section|#end)\b/,
+            /\s+/,
+            IDENT_RE
+          ],
+          className: {
+            1: "keyword",
+            3: "section.name"
+          }
+        },
+        {
+          begin: [
+            /(#section|#end)\b/
+          ],
+          className: {
+            1: "keyword"
+          }
+        },
+        {
+          begin: [
+            /(#check|#compute(-whnf|-nf)?|#set-option|#unset-option)\b/
+          ],
+          className: {
+            1: "type.command"
+          }
+        },
+        {
+          begin: [
+            /(#assume|#variable|#variables)\b/,
+            /\s+/,
+            MANY_IDENT_RE,
+          ],
+          className: {
+            1: "meta",
+            3: "variable"
+          }
         }
-      }
-    ]
-  };
-}
+      ]
+    };
+  }
 );

docs/custom_theme/main.html

@@ -17,5 +17,11 @@
       hljs.addPlugin(new CopyButtonPlugin());
       hljs.highlightAll();
     </script>
+    <style>
+      .rzk-render {
+        float: right;
+        clear: both;
+      }
+    </style>
     {{ super() }}
 {% endblock %}