Merge pull request #150 from rzk-lang/mkdocs-languages

Add support for multiple languages in the documentation

.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

docs/config/base.yml

@@ -0,0 +1,66 @@
+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
+    - 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,72 @@
+INHERIT: "../base.yml"
+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:
+  - Home:
+    - About: index.md
+    - Community: community.md
+    - Tools: tools.md
+    - Contributors: CONTRIBUTORS.md
+    - Changelog: CHANGELOG.md
+  - Getting Started:
+    - 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
+
+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,73 @@
+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
+  - Первые шаги:
+    - Установка: 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
+
+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