DevDays2017Fall-Cokoune — различия между версиями
Материал из SEWiki
(Новая страница: «== Суть == Добавить в kakoune (http://kakoune.org/) следующую функциональность: * Возможность запуска…») |
|||
| (не показано 9 промежуточных версий этого же участника) | |||
| Строка 1: | Строка 1: | ||
== Суть == | == Суть == | ||
| − | + | === Теоретический минимум === | |
| − | + | ==== 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. | |
== Ссылки == | == Ссылки == | ||
| − | + | * https://github.com/dkhalansky/coqoune -- репозиторий. | |
| − | + | * https://github.com/dkhalansky/coqoune/issues -- багтрекер. | |
| − | + | * https://github.com/the-lambda-church/coquille -- схожий плагин для Vim. | |
| + | * https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. В субтитрах приведены комментарии к происходящему. | ||
| + | * http://mit.spbau.ru/sewiki/images/e/e9/Coqoune_slides.pdf -- презентация. | ||
Текущая версия на 12:35, 7 ноября 2017
Содержание
Суть
Теоретический минимум
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.
Ссылки
- https://github.com/dkhalansky/coqoune -- репозиторий.
- https://github.com/dkhalansky/coqoune/issues -- багтрекер.
- https://github.com/the-lambda-church/coquille -- схожий плагин для Vim.
- https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. В субтитрах приведены комментарии к происходящему.
- http://mit.spbau.ru/sewiki/images/e/e9/Coqoune_slides.pdf -- презентация.
