Опции¶

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

Синтаксис¶

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

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

`verbosity`¶

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

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

`render`¶

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

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

`warn-overhang`¶

Управляет нефатальной подсказкой, которая печатается, когда грань ограничения или условие recOR выходит за пределы локального контекста топов (не следует из него, но пересекается с ним). Такой «выход за пределы» допустим — например, при ограничении уже определённой фигурой, грани которой заданы на всём кубе, — поэтому подсказка носит информационный характер. Проверка требует обращения к решателю для каждой грани, поэтому по умолчанию она выключена.

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

Примеры¶

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

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

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

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

Примечания¶

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