DevDays2017Fall-Cokoune
Материал из SEWiki
Версия от 11:02, 1 ноября 2017; Dkhalansky (обсуждение | вклад) (Новая страница: «== Суть == Добавить в kakoune (http://kakoune.org/) следующую функциональность: * Возможность запуска…»)
Суть
Добавить в kakoune (http://kakoune.org/) следующую функциональность:
* Возможность запускать демон Coq версии не менее 8.5 (coqtop); * Передача coqtop команды для проверки теорем вплоть до текущей позиции главного курсора; * Получение из coqtop сведений о текущих целях доказательства и найденных ошибках.
kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства.
Участники
* Тагир Гумеров; * Халанский Дмитрий; * Чернышёв Ярослав.
Ссылки
* https://github.com/dkhalansky/coqoune -- репозиторий; * https://github.com/dkhalansky/coqoune/issues -- багтрекер; * https://github.com/the-lambda-church/coquille -- схожий плагин для Vim.