Перейти к содержанию

Инструменты

Решатель теорем Rzk включает в себя языковой сервер и возможность автоматичекого форматирования.

Другие инструменты улучшают пользовательский опыт и/или автоматизируют частные задачи.

Расширение для VS Code

См. rzk-lang/vscode-rzk. Расширение предлагает много удобств и использование VS Code с ним рекомендуется, особенно новичкам, поскольку это наиболее распространённый способ работы с Rzk и ему уделяется больше внимания со стороны разработчиков.

Движок интерактивных игр для Rzk

См. rzk-lang/rzk-game. Этот движок позволяет создавать интерактивные игры-доказательства в стиле игр для Lean 4, но для синтетической теории ∞-категорий. Он компилируется в WebAssembly и связывается с библиотекой Rzk, поэтому проверка типов выполняется прямо в браузере. Игрок заполняет дырки (?) в терме, а для каждой дырки движок показывает её цель и локальный контекст.

Две игры доступны прямо в браузере, без установки:

Чтобы написать свою игру, Haskell не нужен: игра — это оглавление и по файлу на уровень. Начать проще всего с шаблона, который сам по себе играбелен и показывает возможности движка.

Плагин для MkDocs

См. rzk-lang/mkdocs-plugin-rzk. Плагин улучшает документацию, получаемую из литературных файлов с формализациями (.rzk.md):

  • добавляет SVG-диаграммы по определениям/доказательствам, если возможно (экспериментальная поддержка)
  • добавляет якоря для определний (полезно для создания ссылок на конкретные определения)

Скрипт для GitHub Action

См. rzk-lang/rzk-action. Этот скрипт позволяет проверять формализации на Rzk для проектов на GitHub автоматически. Скрипт также экспериментально поддерживает проверку форматирования.

Подсветка синтаксиса (Pygments)

См. rzk-lang/pygments-rzk. Это простая реализация подсветки синтаксиса (используется при генерации документации с MkDocs и пакетом minted package в LaTeX). Учтите, что подсветка может отличатся от подсветки в VS Code, т.к. последний использует языковой сервер Rzk для более точной "семантической подсветки".