DevDays2017Fall-Cokoune

Суть

Добавить в kakoune (http://kakoune.org/) следующую функциональность:

 * Возможность запускать демон Coq версии не менее 8.5 (coqtop);
 * Передача coqtop команды для проверки теорем вплоть до текущей позиции главного курсора;
 * Получение из coqtop сведений о текущих целях доказательства и найденных ошибках.

kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства.

Функциональность

Запланировано и сделано:

• Подсветка синтаксиса Coq в kakoune;
• Поддержка трёхпанельного вида в kakoune;
• Вывод ошибок в панель ошибок;
• Вывод целей в панель целей;
• Подсветка региона, который уже был проверен Coq'ом;
• Команды управления Coq в kakoune: доказательство вплоть до указанной позиции, доказательство следующего из ещё не проверенных высказываний;
• Запуск демона Coq изнутри редактора (чтобы не было необходимости держать его включенным рядом).

Запланировано и не сделано:

• Подсветка синтаксиса в дополнительных панелях (панель целей и панель ошибок);
• Отказ от Python-интерфейса к Coq в пользу обычных плагинов к kakoune на чистом sh.

Не запланировано, но сделано:

• Подсветка следующей ошибки;
• Автоматическое обновление сведений о том, какие области проверены, в случае внесения правок в одной из уже проверенных областей.

Участники

• Тагир Гумеров: интеграция 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.