DevDays2017Fall-Cokoune — различия между версиями
Материал из SEWiki
(Новая страница: «== Суть == Добавить в kakoune (http://kakoune.org/) следующую функциональность: * Возможность запуска…») |
(→Участники) |
||
| Строка 11: | Строка 11: | ||
== Участники == | == Участники == | ||
| − | + | * Тагир Гумеров: интеграция kakoune с Python, подсветка синтаксиса Coq, внесение функциональности показа служебных сообщений от Coq в Python-интерфейс. | |
| − | + | * Халанский Дмитрий: программирование плагина для kakoune, правка Python-интерфейса к Coq. | |
| − | + | * Чернышёв Ярослав: написание скриптов для десериализации ответов от Coq в текстовое представление, которое и видно на экране, а также интеграция kakoune с Python. | |
== Ссылки == | == Ссылки == | ||
Версия 18:28, 3 ноября 2017
Суть
Добавить в kakoune (http://kakoune.org/) следующую функциональность:
* Возможность запускать демон Coq версии не менее 8.5 (coqtop); * Передача coqtop команды для проверки теорем вплоть до текущей позиции главного курсора; * Получение из coqtop сведений о текущих целях доказательства и найденных ошибках.
kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства.
Участники
- Тагир Гумеров: интеграция 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.
