Опции

Команды #set-option и #unset-option управляют опциями тайпчекера.

Синтаксис

#set-option "<option-name>" = "<value>"
#unset-option "<option-name>"

Доступные опции

verbosity

Управляет уровнем детализации прогресса в выводе при проверке типов.

• "silent" — без вывода логов
• "normal" — вывод прогресса проверки типов (по умолчанию)
• "debug" — вывод каждого промежуточного действия (полезно для отладки)

render

Управляет бэкендом визуализации для диаграмм.

• "svg" — включить визуализацию в формате SVG
• "latex" — включить визуализацию в формате LaTeX
• "none" — отключить визуализацию (по умолчанию)

warn-meta-prefix

Метапрефикс объявления заканчивается на последнем схематическом параметре: вселенной, CUBE, TOPE или функции, квантифицирующей по ним либо принимающей в них значения. Эти параметры задают семейство утверждений объектной теории (§3.2 статьи о Rzk¹). Проверка сообщает об использовании объявления с недостаточным числом схематических аргументов, например при помещении его в пару.

• "strict" — дополнительно требовать, чтобы ненасыщенные схематические аргументы передавались внутри метапрефикса другого объявления (по умолчанию).
• "structural" — разрешать ненасыщенные аргументы на любом схематическом параметре.
• "off" — отключить проверку при выключенном RSTT-safe.

Коды диагностики — MetaPrefixWarning и MetaPrefixWarningStrictOnly. Псевдонимы и аргументы схематических параметров допустимы. Насыщенность не обеспечивает проверку уровней вселенных; см. ограничение непротиворечивости.

rstt-safe

Проверяет объявления на принадлежность фрагменту RSTT, для которого доказана консервативность.¹

• "warn" — сообщать об обнаруженных нарушениях.
• "error" — отклонять объявления с нарушениями или незавершёнными проверками.
• "off" — использовать отдельные настройки предупреждений (по умолчанию).

По умолчанию режим выключен: его проверки увеличивают время проверки большой библиотеки в несколько раз. Для запуска его включают параметрами --rstt-safe=warn или --rstt-safe=error, для области в файле — командой #set-option.

Активный режим RSTT-safe задаёт следующие настройки:

Опция	RSTT-safe "warn" / "error"	По умолчанию при выключенном RSTT-safe
warn-meta-prefix	"strict"	"strict"
warn-free-standing-restriction	"yes"	"no"
warn-meta-binder	"yes"	"no"
warn-shape-dependency	"yes"	"no"

Режим также сообщает о незавершённых обязательствах и неподдерживаемых конструкциях, включая модальные и индуктивные расширения, вспомогательные интервалы, инволюции и кубические sup и inf. У этих проверок нет отдельных опций. Нарушения в исходных выражениях отмечаются, даже если вычисление их устраняет. Типы, полученные вычислением, также проверяются; незавершённая проверка даёт RSTTIncompleteWarning.

warn-overhang и warn-tope-family-domain остаются независимыми предупреждениями. Они не приводят к ошибке в режиме RSTT-safe.

Параметры rzk typecheck --rstt-safe=warn, --rstt-safe=error и --rstt-safe=off задают режим для всего запуска, включая все входные модули. Опции в исходных файлах не могут его изменить. В режиме ошибок нарушения дают неуспешный код завершения, в том числе с --json и --allow-holes. Исходная команда #set-option действует только в своей области; включение режима не запускает полную повторную проверку предшествующих объявлений.

Схематические параметры проверяются отдельно от обычных типов. Параметр (A : U) требует обычный тип; передача U, рода семейства вроде X → U или схематического правила даёт RSTTSchematicWarning. Проверка раскрывает определения, учитывает вычисления и проверяет зависимости доказательства, даже если они были введены при выключенном режиме. Проверка зависимости не использует предположения о топах из места её применения.

Предположения и постулаты остаются доверенными: проверяются их формулировки, но не непротиворечивость. Эта проверка отвергает контрпример Хюркенса, не вводя уровни вселенных. Она дополняет проверку типов Rzk, но не является отдельным ядром RSTT. Проверка консервативна: применение обычных полиморфных комбинаторов к схематическим данным может потребовать прямого схематического определения.

warn-overhang

Предупреждает, когда грань ограничения или условие ветви recOR пересекается с локальным контекстом топов, но не содержится в нём. Проверяется, влечёт ли грань или условие весь контекст. Такой выход за пределы контекста допустим.

• "yes" — сообщать о выходе за пределы контекста с кодом OverhangWarning.
• "no" — не проверять выход за пределы контекста (по умолчанию).

Предупреждение выводится в тексте, JSON и диагностике языкового сервера, в том числе при verbosity = "silent". Оно не становится ошибкой в режиме RSTT-safe.

warn-tope-family-domain

Управляет предупреждением о семействе топов, не содержащемся в своей объявленной области. Семейство χ : ψ → TOPE обозначает топ внутри ψ, и тайпчекер читает его как пересечение с областью: конкретное семейство \ t → φ, проверяемое против {t : I | ψ} → TOPE, элаборируется в \ t → ψ ∧ φ, если только из φ уже не следует ψ. Когда конъюнкт добавляется, проверенное семейство отличается от записанного, о чём и сообщает предупреждение. Например, внутренний рог, объявленный над Δ³ с гранями, записанными на всём кубе, читается как рог внутри Δ³, что обычно и имеется в виду. Проверка не требует ничего сверх вывода, который решает, нужен ли конъюнкт.

• "yes" — предупреждать о семействе, не содержащемся в своей объявленной области (по умолчанию); код предупреждения — TopeFamilyDomainWarning
• "no" — не предупреждать (семейство всё равно читается как пересечение с областью)

warn-free-standing-restriction

Предупреждает о свободно стоящих ограничениях в предпосылках, которые выходят за рамки фрагмента с доказанной консервативностью.¹ Ограничение считается свободно стоящим, если оно не расположено непосредственно на кодомене Π по форме. Граничные условия проверяются внутри этой формы, поэтому граница может выходить за её пределы.

Проверка охватывает типы связанных переменных, мотивы элиминаторов, базовые типы типов тождества и типы, переданные как данные. Проверяются и типы, полученные вычислением. Ограничения вдоль выводимых кодоменов допустимы, в том числе под обычным Π. Постулат задаёт предпосылку, поэтому его тип проходит ту же проверку ограничений, что и другие предпосылки.

• "yes" — сообщать о свободно стоящих ограничениях в предпосылках с кодом FreeStandingRestrictionWarning.
• "no" — отключить предупреждение (по умолчанию при выключенном RSTT-safe).

Активный режим RSTT-safe включает проверку.

warn-shape-dependency

Предупреждает о внешних кубических точках в кубах областей, условиях форм и предполагаемых границах типов расширения, следуя RS17, приложению A.2.² Учитываются зависимости, раскрываемые через псевдонимы и вычисление. Координаты, связанные вместе в кубе-произведении, допустимы. Граничные значения также могут зависеть от внешних точек. Граница может выходить за пределы области: при переводе в RSTT её можно пересечь с этой областью.

• "yes" — сообщать о зависимостях с кодом RSTTShapeDependencyWarning.
• "no" — отключить предупреждение при выключенном RSTT-safe (по умолчанию).

Активный режим RSTT-safe включает проверку; #unset-option восстанавливает "no". Предупреждение не исключает эквивалентной переформулировки в RSTT.

warn-meta-binder

Предупреждает о схематических параметрах, связанных внутри термов, в том числе термов со значениями в типах. Например, помещение \ (A : U) → A в пару даёт MetaBinderWarning. Схематический параметр имеет тип U, CUBE, TOPE или тип функции, квантифицирующей по ним либо принимающей в них значения.

Ведущие параметры определения и схематические аргументы других объявлений допустимы (см. warn-meta-prefix).

• "yes" — сообщать о схематических связываниях внутри термов.
• "no" — отключить предупреждение (по умолчанию при выключенном RSTT-safe).

Активный режим RSTT-safe включает проверку.

Примеры

#lang rzk-1
-- Установить подробность в тихий режим
#set-option "verbosity" = "silent"

-- Включить визуализацию SVG
#set-option "render" = "svg"

-- Позже отключить визуализацию
#unset-option "render"

-- Вернуть подробность в нормальный режим
#set-option "verbosity" = "normal"

Примечания

• Опции устанавливаются на оставшуюся часть файла (или до сброса)
• #unset-option возвращает опцию к её значению по умолчанию
• Неизвестные имена опций или недопустимые значения приведут к ошибке проверки типов

---

1. Nikolai Kudasov, Violetta Sim, and Benedikt Ahrens. Rzk: a Proof Assistant for Synthetic ∞-Categories. 2026. https://arxiv.org/abs/2607.12207 — §3.2 о слое параметров, §5 о консервативном фрагменте. ↩↩↩

2. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. 2017. https://arxiv.org/abs/1705.07442 — в приложении A.2 объясняется, почему формы типов расширения не должны зависеть от внешнего контекста кубов. ↩