DevDays2017Fall-Cokoune — различия между версиями
Материал из SEWiki
(→Участники) |
|||
| Строка 8: | Строка 8: | ||
kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства. | kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства. | ||
| + | |||
| + | == Функциональность == | ||
| + | |||
| + | Запланировано и сделано: | ||
| + | * Подсветка синтаксиса Coq в kakoune; | ||
| + | * Поддержка трёхпанельного вида в kakoune; | ||
| + | * Вывод ошибок в панель ошибок; | ||
| + | * Вывод целей в панель целей; | ||
| + | * Подсветка региона, который уже был проверен Coq'ом; | ||
| + | * Команды управления Coq в kakoune: доказательство вплоть до указанной позиции, доказательство следующего из ещё не проверенных высказываний; | ||
| + | * Запуск демона Coq изнутри редактора (чтобы не было необходимости держать его включенным рядом). | ||
| + | |||
| + | Запланировано и не сделано: | ||
| + | * Подсветка синтаксиса в дополнительных панелях (панель целей и панель ошибок); | ||
| + | * Отказ от Python-интерфейса к Coq в пользу обычных плагинов к kakoune на чистом sh. | ||
| + | |||
| + | Не запланировано, но сделано: | ||
| + | * Подсветка следующей ошибки; | ||
| + | * Автоматическое обновление сведений о том, какие области проверены, в случае внесения правок в одной из уже проверенных областей. | ||
== Участники == | == Участники == | ||
Версия 18:37, 3 ноября 2017
Содержание
Суть
Добавить в 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.
