DevDays2017Fall-Cokoune

Суть

Теоретический минимум

Coq. Редакторы с поддержкой языка Coq

Видео с примером работы CoqIDE: https://drive.google.com/file/d/1OMIC97yge9SH6At7ymadnd4tDdKW4XNP/view?usp=sharing

Существует язык 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 -- демонстрация работы плагина. На этом видео показаны процесс запуска, способы переходить вперёд и назад по ходу доказательства, обработка ошибок в доказательстве, а также тот приятный момент, что правки ранее доказанного тут же инвалидируют доказательство, но только если меняется сам текст доказательства: правки, относящиеся к выравниванию текста, не приводят к инвалидации.