DevDays2017Fall-Cokoune

Материал из SEWiki
Версия от 12:35, 7 ноября 2017; Dkhalansky (обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск

Суть

Теоретический минимум

Coq. Редакторы с поддержкой языка Coq

Видео с примером работы CoqIDE: https://drive.google.com/file/d/1OMIC97yge9SH6At7ymadnd4tDdKW4XNP/view?usp=sharing

Существует язык Coq для доказательства математических высказываний. Этот язык совершенно нечитаемый, поэтому без инструментальной поддержки им пользоваться невозможно.

Типичный редактор с поддержкой Coq выглядит так. Имеется три окна. В одном окне расположен код доказательства. Разные его части имеют разную подсветку в зависимости от того, считает ли Coq, что они успешно доказаны. В другом окне расположены цели доказательства: набор высказываний, которые сейчас нужно доказать, чтобы Coq принял истинность утверждения, а также сведения, которые могут в доказательстве помочь. В третьем окне расположена служебная информация: сведения об ошибках и мета-результатах выполнения команд, таких как успешное объявление функции.

Когда пользователь решает, что доказал некоторое утверждение, он приказывает редактору отправить это утверждение на обработку демону Coq. Демон в результате может принять эту команду и обновить набор высказываний, которые осталось доказать, или же вывести ошибку с описанием того, почему команда некорректная.

Текстовый редактор kakoune

kakoune (http://kakoune.org/) -- редактор, подобный vim. Для него тоже режим ввода текста не является основным режимом работы, он тоже работает в консоли и у него схожий с vim набор команд. При этом kakoune построен на идее минималистичности: базовых команд в нём очень мало, но они построены так, что их должно быть легко компоновать в сложные. Не нужно, как в vim, запоминать сотню клавиш и тысячу команд: здесь весь язык учится за вечер.

Проблема

Нет удобных текстовых редакторов с поддержкой Coq.

  • CoqIDE -- стандартная среда для работы с Coq -- по методу набора текста напоминает "Блокнот" из Windows. Средств быстро перемещаться по тексту, оперировать сразу блоками текста, эффективно корректировать опечатки практически нет, если сравнивать с более мощными редакторами вроде Emacs, vim, kakoune или даже Sublime Text, Atom, Notepad++ или чем-то вроде этого.
  • vim с библиотекой coquille -- очень сырой проект. Обнаружилось, что в этой среде возможно заставить Coq принять неправильное доказательство; что нет возможности в ней получать сообщения в третье окно; что при появлении ошибки редактор выдаёт исключение, пусть и не падает совсем; что правила перевода курсора проверки в текущую позицию курсора текстового не совпадают с интуитивными представлениями и с тем, как это происходит в CoqIDE.
  • emacs с библиотекой ProofGeneral -- это emacs. emacs сам по себе очень неудобный редактор, что признают даже его адепты, что вынуждает накручивать тучу плагинов, чтобы можно было хоть как-то работать. Неплохим сочетанием является комбинация evil-mode (возможности использовать в emacs клавиши vim) и ProofGeneral, но это довольно громоздкое решение. В силу этого оно кажется слишком далёким от оптимального, особенно если учесть, что после kakoune модель редактирования vim кажется неэффективной. К тому же... https://proofgeneral.github.io/doc/userman/ProofGeneral_12/#Coq_002dspecific-commands : Ctrl-C - Ctrl-A - Ctrl-S? Серьёзно? Последовательность из _трёх_ клавиш?

Задача

Добавить в kakoune поддержку Coq такую, что можно будет использовать исключительно этот текстовый редактор для написания доказательств на Coq, не ощущать нехватки функциональности по сравнению с vim + coquille и при этом не встречаться с теми жуткими багами, которые обитают в coquille.

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

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

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

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

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

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

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

Участники

  • Тагир Гумеров: интеграция kakoune с Python, подсветка синтаксиса Coq, внесение функциональности показа служебных сообщений от Coq в Python-интерфейс.
  • Халанский Дмитрий: программирование плагина для kakoune, правка Python-интерфейса к Coq.
  • Чернышёв Ярослав: написание скриптов для десериализации ответов от Coq в текстовое представление, которое и видно на экране, а также интеграция kakoune с Python.

Ссылки

Источник — «http://mit.spbau.ru/sewiki/index.php?title=DevDays2017Fall-Cokoune&oldid=13641»