DevDays2017Fall-Cokoune - История изменений

Dkhalansky в 09:35, 7 ноября 2017

2017-11-07T09:35:18Z

Dkhalansky: /* Ссылки */

2017-11-07T09:14:34Z

‎Ссылки

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

2017-11-07T08:54:58Z

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

Dkhalansky: /* Ссылки */

2017-11-07T08:08:18Z

‎Ссылки

Dkhalansky: /* Ссылки */

2017-11-07T08:07:41Z

‎Ссылки

Dkhalansky: /* Ссылки */

2017-11-06T19:40:44Z

‎Ссылки

Dkhalansky: /* Функциональность */

2017-11-04T10:35:08Z

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

Dkhalansky в 20:18, 3 ноября 2017

2017-11-03T20:18:56Z

Dkhalansky в 15:37, 3 ноября 2017

2017-11-03T15:37:05Z

Dkhalansky: /* Участники */

2017-11-03T15:28:23Z

‎Участники

@@ Строка 57: / Строка 57: @@
 == Ссылки ==
-* https://github.com/dkhalansky/coqoune -- репозиторий;
+* https://github.com/dkhalansky/coqoune -- репозиторий.
-* https://github.com/dkhalansky/coqoune/issues -- багтрекер;
+* https://github.com/dkhalansky/coqoune/issues -- багтрекер.
 * https://github.com/the-lambda-church/coquille -- схожий плагин для Vim.
 * https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. В субтитрах приведены комментарии к происходящему.

@@ Строка 60: / Строка 60: @@
 * https://github.com/dkhalansky/coqoune/issues -- багтрекер;
 * https://github.com/the-lambda-church/coquille -- схожий плагин для Vim.
-* https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. На этом видео показаны процесс запуска, способы переходить вперёд и назад по ходу доказательства, обработка ошибок в доказательстве, а также тот приятный момент, что правки ранее доказанного тут же инвалидируют доказательство, но только если меняется сам текст доказательства: правки, относящиеся к выравниванию текста, не приводят к инвалидации.
+* https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. В субтитрах приведены комментарии к происходящему.

← Предыдущая		Версия 08:54, 7 ноября 2017
Строка 4:		Строка 4:

	==== Coq. Редакторы с поддержкой языка Coq ====		==== Coq. Редакторы с поддержкой языка Coq ====
		+
		+	Видео с примером работы CoqIDE: https://drive.google.com/file/d/1OMIC97yge9SH6At7ymadnd4tDdKW4XNP/view?usp=sharing

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

@@ Строка 58: / Строка 58: @@
 * https://github.com/dkhalansky/coqoune/issues -- багтрекер;
 * https://github.com/the-lambda-church/coquille -- схожий плагин для Vim.
-* https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. На этом видео показаны процесс запуска, способы переходить вперёд и назад по ходу доказательства, а также тот приятный момент, что правки ранее доказанного тут же инвалидируют доказательство, но только если меняется сам текст доказательства: правки, относящиеся к выравниванию текста, не приводят к инвалидации.
+* https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. На этом видео показаны процесс запуска, способы переходить вперёд и назад по ходу доказательства, обработка ошибок в доказательстве, а также тот приятный момент, что правки ранее доказанного тут же инвалидируют доказательство, но только если меняется сам текст доказательства: правки, относящиеся к выравниванию текста, не приводят к инвалидации.

@@ Строка 58: / Строка 58: @@
 * https://github.com/dkhalansky/coqoune/issues -- багтрекер;
 * https://github.com/the-lambda-church/coquille -- схожий плагин для Vim.
-* https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина.
+* https://drive.google.com/file/d/1fAIKkKSbQfTrZ8rQZLnIJ76CnGfGgIm2/view?usp=sharing -- демонстрация работы плагина. На этом видео показаны процесс запуска, способы переходить вперёд и назад по ходу доказательства, а также тот приятный момент, что правки ранее доказанного тут же инвалидируют доказательство, но только если меняется сам текст доказательства: правки, относящиеся к выравниванию текста, не приводят к инвалидации.

@@ Строка 40: / Строка 40: @@
 Запланировано и не сделано:
 * Подсветка синтаксиса в дополнительных панелях (панель целей и панель ошибок);
-* Отказ от Python-интерфейса к Coq в пользу обычных плагинов к kakoune на чистом sh.
+* Отказ от Python-интерфейса к Coq в пользу обычных плагинов к kakoune на чистом sh;
 Не запланировано, но сделано:

@@ Строка 1: / Строка 1: @@
 == Суть ==
-Добавить в kakoune (http://kakoune.org/) следующую функциональность:
+=== Теоретический минимум ===
-  * Возможность запускать демон Coq версии не менее 8.5 (coqtop);
+==== Coq. Редакторы с поддержкой языка Coq ====
-  * Передача coqtop команды для проверки теорем вплоть до текущей позиции главного курсора;
-  * Получение из coqtop сведений о текущих целях доказательства и найденных ошибках.
-kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства.
+Существует язык Coq для доказательства математических высказываний. Этот язык совершенно нечитаемый, поэтому без инструментальной поддержки им пользоваться невозможно.
 == Функциональность ==

← Предыдущая		Версия 15:37, 3 ноября 2017
Строка 8:		Строка 8:

	kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства.		kakoune должен в процессе работы иметь три буфера, один из которых содержит предоставляемый пользователем код доказательства, второй -- сведения о возникших ошибках, третий -- сведения о текущей цели доказательства.
		+
		+	== Функциональность ==
		+
		+	Запланировано и сделано:
		+	* Подсветка синтаксиса Coq в kakoune;
		+	* Поддержка трёхпанельного вида в kakoune;
		+	* Вывод ошибок в панель ошибок;
		+	* Вывод целей в панель целей;
		+	* Подсветка региона, который уже был проверен Coq'ом;
		+	* Команды управления Coq в kakoune: доказательство вплоть до указанной позиции, доказательство следующего из ещё не проверенных высказываний;
		+	* Запуск демона Coq изнутри редактора (чтобы не было необходимости держать его включенным рядом).
		+
		+	Запланировано и не сделано:
		+	* Подсветка синтаксиса в дополнительных панелях (панель целей и панель ошибок);
		+	* Отказ от Python-интерфейса к Coq в пользу обычных плагинов к kakoune на чистом sh.
		+
		+	Не запланировано, но сделано:
		+	* Подсветка следующей ошибки;
		+	* Автоматическое обновление сведений о том, какие области проверены, в случае внесения правок в одной из уже проверенных областей.

	== Участники ==		== Участники ==

@@ Строка 11: / Строка 11: @@
 == Участники ==
-  * Тагир Гумеров;
+* Тагир Гумеров: интеграция kakoune с Python, подсветка синтаксиса Coq, внесение функциональности показа служебных сообщений от Coq в Python-интерфейс.
-  * Халанский Дмитрий;
+* Халанский Дмитрий: программирование плагина для kakoune, правка Python-интерфейса к Coq.
-  * Чернышёв Ярослав.
+* Чернышёв Ярослав: написание скриптов для десериализации ответов от Coq в текстовое представление, которое и видно на экране, а также интеграция kakoune с Python.
 == Ссылки ==