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.