LINUX.ORG.RU

Coq 8.9

 , , , ,


3

3

Состоялся релиз Coq 8.9. Его разработка заняла 7 месяцев с момента выпуска Coq 8.8. Этот релиз является результатом ≈2000 коммитов и ≈500 pull request’ов.

Coq — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования с зависимыми типами.

Особенностью Coq является широкое использование тактик для построения доказательств, в отличие от таких систем, как Agda или Idris.

Основные изменения в этой версии:

  • Поддержка взаимно рекурсивных record’ов (Pierre-Marie Pédrot).
  • Добавлена команда Numeral Notation для перегрузки десятичных чисел сторонними типами (Daniel de Rauglaudre, Pierre Letouzey и Jason Gross).
  • { теперь поддерживает именованные цели, например [x]:{ (Théo Zimmermann).
  • Удалены команды Arguments Scope и Implicit Arguments.
  • coqtop и coqide теперь могут подсвечивать разницу в шагах доказательства, используя команду Diffs.
  • Изменения в стандартной библиотеке: в библиотеках VectorDef, Ascii, String.
  • Удалена утилита gallina.
  • Многочисленные исправления в новой документации, основанной на Sphinx.

>>> Подробности

Одна из причин по которой я люблю линукс - открываешь для себя весь мир. Если бы не lor, никогда бы не узнал про Coq, и уж тем более не стал бы им интересоваться, если бы он был закрытым, ведь в закрытом софте не поощряется изучение никак, а наоборот препятствуется этому. А ещё пишешь в командной строке aptitude, раскрываешь неустановленные и, например, раздел net и начинаешь читать подряд описания. Ящик пандоры открыт.

anonymous ()