Coq: Ошибка: невозможно найти библиотеку Coq.extraction.Extraction - PullRequest
Новая
       11

Coq: Ошибка: невозможно найти библиотеку Coq.extraction.Extraction

0 голосов
/ 18 мая 2019

Я прохожу курс «Основы программного обеспечения». Не удается запустить главу «Извлечение». Ошибка в первой строке Require Coq.extraction.Extraction. с сообщением Coq: Error: Unable to locate library Coq.extraction.Extraction.

Я запускаю его в CoqIde.

coqc -v: Coq Proof Assistant, версия 8.6 (октябрь 2017 г.) скомпилировано 28 октября 2017 года 14:23:55 с OCaml 4.05.0

Версия CoqIde: 8,6

Аргументы CoqTop: -Q / home / evgenii / mysources / coq / coq-excercises / lf LF

Чего мне не хватает?

1 Ответ

2 голосов
/ 18 мая 2019

Попробуйте заменить эту строку на Require Extraction. (Coq.extraction.Extraction представляется обратно несовместимой формой.)

8.6 довольно старая, поэтому могут возникнуть другие проблемы совместимости, если она не соответствуетверсия, используемая вашим дистрибутивом Программных фондов.Посмотрите в Preface.v ожидаемую версию Coq и рассмотрите возможность обновления, если есть несоответствие.

...