Merge branch 'release-v0.7.2'

* release-v0.7.2: (31 commits)
  Bump version and update changelogs
  Move the blog out of versioned docs
  Replace manual string manipulation with tokens
  Update rzk/src/Rzk/Main.hs
  Throw an error when rzk.yaml `include` is empty
  Replace `setDifference` with `stripInfix`
  Add RSS feed for the blog
  Fix first post's date
  Add a page mentioning/comparing with other HoTT assistants
  Fix rzk.yaml
  Set up blog (in English version), use navigation.indexes
  Fix site_url
  Use mkdocs-material[imaging]
  Ignore .cache/
  Fix plugins (no deep merge), integrate ToC, social
  Select better fonts for English and Russian
  Update global rzk.yaml to match English docs
  Fix Rzk check for docs
  Clean up some docs and translate some to Russian
  Remove redundant emoji plugin (supported natively since MkDocs Material 9.4)
  ...

.github/workflows/mkdocs.yml

@@ -2,7 +2,7 @@ name: MKDocs
 
 on:
   push:
-    branches: [develop]
+    branches: [develop,mkdocs-*]
     tags: [v*]
     paths:
       - .github/workflows/mkdocs.yml
@@ -37,6 +37,12 @@ jobs:
           rename-to: rzk
           chmod: 0755
 
+      - name: Check Rzk files for each language
+        run:
+          for lang_dir in $(ls -d docs/docs/*/); do
+            pushd ${lang_dir} && rzk typecheck; popd ;
+          done
+
       - name: 🔨 Install MkDocs Material and mike
         run: pip install -r docs/requirements.txt
 
@@ -46,11 +52,16 @@ jobs:
           git config --local user.name "github-actions[bot]"
 
       - name: 🚀 Deploy with mike (${{ github.ref_name }}, latest)
-        if: ${{ github.ref_name != 'develop' }}
+        if: ${{ github.ref_name != 'develop' && !startsWith(github.ref_name, 'mkdocs') }}
         run: |
-          mike deploy --push --update-aliases --config-file docs/mkdocs.yml ${{ github.ref_name }} latest
+          for config in $(ls docs/config/*/mkdocs.yml); do
+            mike deploy --push --update-aliases --config-file ${config} ${{ github.ref_name }} latest;
+            mike set-default latest --config-file ${config} --push;
+          done
 
       - name: 🚀 Deploy with mike (${{ github.ref_name }})
-        if: ${{ github.ref_name == 'develop' }}
+        if: ${{ github.ref_name == 'develop' || startsWith(github.ref_name, 'mkdocs') }}
         run: |
-          mike deploy --push --config-file docs/mkdocs.yml ${{ github.ref_name }}
+          for config in $(ls docs/config/*/mkdocs.yml); do
+            mike deploy --push --config-file ${config} ${{ github.ref_name }};
+          done

.gitignore

@@ -1,5 +1,7 @@
+.cache/
 .DS_Store
 docs/out/
+docs/generated/
 dist
 dist-*
 cabal-dev
@@ -33,4 +35,4 @@ __pycache__
 *.fls
 *.log
 rzk/doc/
-/rzk-playground-release
+/rzk-playground-release

CITATION.cff

@@ -8,5 +8,5 @@ authors:
   - family-names: Danko
     given-names: Danila
 title: "Rzk: a  proof assistant for synthetic $\\infty$-categories"
-version: 0.7.1
+version: 0.7.2
 url: "https://github.com/rzk-lang/rzk"

docs/config/base.yml

@@ -0,0 +1,67 @@
+repo_url: https://github.com/rzk-lang/rzk
+repo_name: rzk-lang/rzk
+
+theme:
+  name: material
+  custom_dir: '../../overrides/'
+  favicon: assets/images/favicon.png
+  logo: assets/images/logo-1000x1000.png
+  icon:
+    repo: fontawesome/brands/github
+    edit: material/pencil
+    view: material/eye
+  features:
+    - content.code.copy
+    - content.action.edit
+    - navigation.footer
+    - navigation.tabs
+    - navigation.tabs.sticky
+    - navigation.sections
+    - navigation.prune
+    - navigation.path
+    - navigation.indexes
+    - toc.integrate
+
+extra_javascript:
+  - javascript/mathjax.js
+  - https://polyfill.io/v3/polyfill.min.js?features=es6
+  - https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js
+
+extra_css:
+  - https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.16.7/katex.min.css
+  - https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.7.0/styles/default.min.css
+  - assets/css/rzk-render.css
+
+markdown_extensions:
+  - admonition
+  - footnotes
+  - pymdownx.details
+  - pymdownx.snippets:
+      base_path:
+        - .
+        - ..
+      check_paths: true
+  - mdx_math
+  - pymdownx.highlight:
+      anchor_linenums: true
+      line_spans: __span
+      pygments_lang_class: true
+  - pymdownx.inlinehilite
+  - pymdownx.snippets
+  - pymdownx.superfences
+  - toc:
+      permalink: true
+  - pymdownx.arithmatex:
+      generic: true
+  - attr_list
+
+extra:
+  version:
+    provider: mike
+  alternate:
+    - name: English
+      link: /rzk/en/
+      lang: en
+    - name: Русский
+      link: /rzk/ru/
+      lang: ru

docs/config/en/mkdocs.yml

@@ -0,0 +1,76 @@
+INHERIT: "../base.yml"
+site_url: https://rzk-lang.github.io/rzk/en/
+site_name: "Rzk proof assistant"
+site_description: "An experimental proof assistant for simplicial type theory and synthetic ∞-categories."
+site_author: "Nikolai Kudasov"
+docs_dir: '../../docs/en'
+site_dir: '../../generated/en'
+edit_uri: edit/develop/docs/docs/en/
+
+nav:
+  - About:
+    - index.md
+    - Community: community.md
+    - Tools: tools.md
+    - Contributors: CONTRIBUTORS.md
+    - Changelog: CHANGELOG.md
+    - Other proof assistants: related.md
+  - Getting Started:
+    - getting-started/index.md
+    - Install: getting-started/install.md
+    - Quickstart: getting-started/quickstart.rzk.md
+    - Depedent Types: getting-started/dependent-types.rzk.md
+    - Setting up an Rzk project: getting-started/project.md
+  - Reference:
+    - Introduction: reference/introduction.rzk.md
+    - Cube layer: reference/cube-layer.rzk.md
+    - Tope layer: reference/tope-layer.rzk.md
+    - Dependent types: reference/type-layer.rzk.md
+    - Tope disjunction elimination: reference/tope-disjunction-elimination.rzk.md
+    - Extension types: reference/extension-types.rzk.md
+    - Organizational features:
+      - Sections and Variables: reference/sections.rzk.md
+    - Builtins:
+      - Directed interval: reference/builtins/directed-interval.rzk.md
+      - Unit type: reference/builtins/unit.rzk.md
+    - Commands:
+      - Define and Postulate: reference/commands/define-postulate.rzk.md
+      - Compute: reference/commands/compute.rzk.md
+      - Check: reference/commands/check.rzk.md
+      - Options: reference/commands/options.rzk.md
+    - Other:
+      - Rendering Diagrams: reference/render.rzk.md
+    - Examples:
+      - Weak tope disjunction elimination: examples/recId.rzk.md
+  - Playground: playground/index.html
+  - Blog: blog/index.html
+
+theme:
+  language: en
+  font:
+    text: Inria Sans
+  palette:
+    # Palette toggle for light mode
+    - media: "(prefers-color-scheme: light)"
+      primary: white
+      scheme: default
+      toggle:
+        icon: material/brightness-7
+        name: "Switch to dark mode"
+    # Palette toggle for dark mode
+    - media: "(prefers-color-scheme: dark)"
+      primary: black
+      scheme: slate
+      toggle:
+        icon: material/brightness-4
+        name: "Switch to light mode"
+
+plugins:
+  - social
+  - mike:
+      deploy_prefix: 'en/'
+  - search:
+      lang: en
+  - rzk:
+      render_svg: true
+      anchor_definitions: true

docs/config/ru/mkdocs.yml

@@ -0,0 +1,76 @@
+INHERIT: "../base.yml"
+site_url: https://rzk-lang.github.io/rzk/ru/
+site_name: "Решатель теорем Rzk"
+site_description: "Экспериментальный решатель теорем для симплициальной теории типов и синтетических ∞-категорий."
+site_author: "Николай Кудасов"
+docs_dir: '../../docs/ru'
+site_dir: '../../generated/ru'
+edit_uri: edit/develop/docs/docs/ru/
+
+nav:
+  - О проекте:
+    - index.md
+    - Сообщество: community.md
+    - Инструменты: tools.md
+    - Участники (англ.): CONTRIBUTORS.md
+    - История изменений (англ.): CHANGELOG.md
+    - Другие решатели: related.md
+  - Первые шаги:
+    - getting-started/index.md
+    - Установка: getting-started/install.md
+    - Быстрое начало: getting-started/quickstart.rzk.md
+    - Введение в зависимые типы: getting-started/dependent-types.rzk.md
+    - Настройка проекта: getting-started/project.md
+  - Руководство:
+    - Введение: reference/introduction.rzk.md
+    - Слой кубов: reference/cube-layer.rzk.md
+    - Слой форм: reference/tope-layer.rzk.md
+    - Зависимые типы: reference/type-layer.rzk.md
+    - Устранение объединений форм: reference/tope-disjunction-elimination.rzk.md
+    - Типы-расширения: reference/extension-types.rzk.md
+    - Организация кода:
+      - Разделы и предпосылки: reference/sections.rzk.md
+    - Встроенные определения:
+      - Направленный интервал: reference/builtins/directed-interval.rzk.md
+      - Единичный тип: reference/builtins/unit.rzk.md
+    - Команды:
+      - Определения и постулаты: reference/commands/define-postulate.rzk.md
+      - Вычисления: reference/commands/compute.rzk.md
+      - Проверка типов: reference/commands/check.rzk.md
+      - Опции решателя: reference/commands/options.rzk.md
+    - Другое:
+      - Отрисовка диаграм: reference/render.rzk.md
+    - Примеры:
+      - Слабое устранение объединений форм: examples/recId.rzk.md
+  - Песочница: playground/index.html
+  - Блог (англ.): blog/index.html
+
+theme:
+  language: ru
+  font:
+    text: PT Sans
+  palette:
+    # Palette toggle for light mode
+    - media: "(prefers-color-scheme: light)"
+      primary: white
+      scheme: default
+      toggle:
+        icon: material/brightness-7
+        name: "Переключить на тёмный режим"
+    # Palette toggle for dark mode
+    - media: "(prefers-color-scheme: dark)"
+      primary: black
+      scheme: slate
+      toggle:
+        icon: material/brightness-4
+        name: "Переключить на светлый режим"
+
+plugins:
+  - social
+  - mike:
+      deploy_prefix: 'ru/'
+  - search:
+      lang: ru
+  - rzk:
+      render_svg: true
+      anchor_definitions: true