DevDays2017Fall-Cokoune
Содержание
Суть
Теоретический минимум
Coq. Редакторы с поддержкой языка Coq
Существует язык Coq для доказательства математических высказываний. Этот язык совершенно нечитаемый, поэтому без инструментальной поддержки им пользоваться невозможно.
Типичный редактор с поддержкой Coq выглядит так. Имеется три окна. В одном окне расположен код доказательства. Разные его части имеют разную подсветку в зависимости от того, считает ли Coq, что они успешно доказаны. В другом окне расположены цели доказательства: набор высказываний, которые сейчас нужно доказать, чтобы Coq принял истинность утверждения, а также сведения, которые могут в доказательстве помочь. В третьем окне расположена служебная информация: сведения об ошибках и мета-результатах выполнения команд, таких как успешное объявление функции.
Когда пользователь решает, что доказал некоторое утверждение, он приказывает редактору отправить это утверждение на обработку демону Coq. Демон в результате может принять эту команду и обновить набор высказываний, которые осталось доказать, или же вывести ошибку с описанием того, почему команда некорректная.
Текстовый редактор kakoune
kakoune (http://kakoune.org/) -- редактор, подобный vim. Для него тоже режим ввода текста не является основным режимом работы, он тоже работает в консоли и у него схожий с vim набор команд. При этом kakoune построен на идее минималистичности: базовых команд в нём очень мало, но они построены так, что их должно быть легко компоновать в сложные. Не нужно, как в vim, запоминать сотню клавиш и тысячу команд: здесь весь язык учится за вечер.
Проблема
Нет удобных текстовых редакторов с поддержкой Coq.
- CoqIDE -- стандартная среда для работы с Coq -- по методу набора текста напоминает "Блокнот" из Windows. Средств быстро перемещаться по тексту, оперировать сразу блоками текста, эффективно корректировать опечатки практически нет, если сравнивать с более мощными редакторами вроде Emacs, vim, kakoune или даже Sublime Text, Atom, Notepad++ или чем-то вроде этого.
- vim с библиотекой coquille -- очень сырой проект. Обнаружилось, что в этой среде возможно заставить Coq принять неправильное доказательство; что нет возможности в ней получать сообщения в третье окно; что при появлении ошибки редактор выдаёт исключение, пусть и не падает совсем; что правила перевода курсора проверки в текущую позицию курсора текстового не совпадают с интуитивными представлениями и с тем, как это происходит в CoqIDE.
- emacs с библиотекой ProofGeneral -- это emacs. emacs сам по себе очень неудобный редактор, что признают даже его адепты, что вынуждает накручивать тучу плагинов, чтобы можно было хоть как-то работать. Неплохим сочетанием является комбинация evil-mode (возможности использовать в emacs клавиши vim) и ProofGeneral, но это довольно громоздкое решение. В силу этого оно кажется слишком далёким от оптимального, особенно если учесть, что после kakoune модель редактирования vim кажется неэффективной. К тому же... https://proofgeneral.github.io/doc/userman/ProofGeneral_12/#Coq_002dspecific-commands : Ctrl-C - Ctrl-A - Ctrl-S? Серьёзно? Последовательность из _трёх_ клавиш?
Задача
Добавить в kakoune поддержку Coq такую, что можно будет использовать исключительно этот текстовый редактор для написания доказательств на Coq, не ощущать нехватки функциональности по сравнению с vim + coquille и при этом не встречаться с теми жуткими багами, которые обитают в coquille.
Функциональность
Запланировано и сделано:
- Подсветка синтаксиса Coq в kakoune;
- Поддержка трёхпанельного вида в kakoune;
- Вывод ошибок в панель ошибок;
- Вывод целей в панель целей;
- Подсветка региона, который уже был проверен Coq'ом;
- Команды управления Coq в kakoune: доказательство вплоть до указанной позиции, доказательство следующего из ещё не проверенных высказываний;
- Запуск демона Coq изнутри редактора (чтобы не было необходимости держать его включенным рядом).
Запланировано и не сделано:
- Подсветка синтаксиса в дополнительных панелях (панель целей и панель ошибок);
- Отказ от Python-интерфейса к Coq в пользу обычных плагинов к kakoune на чистом sh;
- Поддержка вывода диагностических сообщений от Coq в области, где обычно указываются ошибки.
Не запланировано, но сделано:
- Подсветка следующей ошибки;
- Автоматическое обновление сведений о том, какие области проверены, в случае внесения правок в одной из уже проверенных областей.
Участники
- Тагир Гумеров: интеграция kakoune с Python, подсветка синтаксиса Coq, внесение функциональности показа служебных сообщений от Coq в Python-интерфейс.
- Халанский Дмитрий: программирование плагина для kakoune, правка Python-интерфейса к Coq.
- Чернышёв Ярослав: написание скриптов для десериализации ответов от Coq в текстовое представление, которое и видно на экране, а также интеграция kakoune с Python.
Ссылки
- https://github.com/dkhalansky/coqoune -- репозиторий;
- https://github.com/dkhalansky/coqoune/issues -- багтрекер;
- https://github.com/the-lambda-church/coquille -- схожий плагин для Vim.
- https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. На этом видео показаны процесс запуска, способы переходить вперёд и назад по ходу доказательства, а также тот приятный момент, что правки ранее доказанного тут же инвалидируют доказательство, но только если меняется сам текст доказательства: правки, относящиеся к выравниванию текста, не приводят к инвалидации.