Невозможно настроить сертифицированное программирование с зависимыми типами - PullRequest
Новая
       56

Невозможно настроить сертифицированное программирование с зависимыми типами

2 голосов
/ 19 апреля 2020

Я работаю с книгой «Сертифицированное программирование с зависимыми типами», но каждый раз нахожу разные ошибки. Мне кажется, что ошибка происходит из-за несоответствия между процессом компиляции из Proof General и make-файлом из источников книги.

  1. Если я скомпилирую исходники с помощью make и попытаюсь запустить для экземпляр Subset.v в Proof-General я получаю:

Ошибка: файл /home/usuario/Desktop/Coq/cpdt/src/CpdtTactics.vo имеет плохой волхв c номер 81100 (ожидается 8600). Он поврежден или был скомпилирован с другой версией Coq.

Если я очищаю скомпилированные файлы makefile с помощью make clean и пытаюсь продолжить с опцией Coq -> Auto Compilation -> Compile, прежде чем require, то это строка:

Require Extraction.

, что не получается. Первоначально произошел сбой с ошибкой:

Ошибка: невозможно найти извлечение библиотеки.

, но с включенной выше опцией это дает что-то вроде:

эхо "Требуется извлечение". > /tmp/ProofGeneral-coqQPJTf0.v coqdep -Q / home / usuario / Desktop / Coq / cpdt / src / -R / home / usuario / Desktop / Coq / cpdt / sr c Cpdt / tmp / ProofGeneral-coqQPJTf0. v * Предупреждение: в файле /tmp/ProofGeneral-coqQPJTf0.v извлечение библиотеки требуется и не найдено в пути загрузки! * Предупреждение: в файле /tmp/ProofGeneral-coqQPJTf0.v извлечение библиотеки требуется и не найдено в пути загрузки! /tmp/ProofGeneral-coqQPJTf0.vo /tmp/ProofGeneral-coqQPJTf0.glob /tmp/ProofGeneral-coqQPJTf0.v.beautific: .v

Как я могу решить эту проблему?

1 Ответ

3 голосов
/ 19 апреля 2020

Дополнительные вопросы: какую ОС вы используете? Вы полагаетесь на opam?

Относительно первой ошибки, которую вы получаете, это, безусловно, исходит из следующего факта:

  • вне доказательства, двоичный файл coqc соответствует Coq 8.11, тогда как в ProofGeneral двоичный файл coqtop соответствует Coq 8.6. Возможно, потому что переменная PATH не одинакова в двух контекстах.

  • Чтобы выяснить, какой двоичный файл найден, вы можете сделать это в терминале which coqtop и в Emacs, M-! который coqtop RET , и поэтому вы должны получить разные пути.

  • Иногда открытие emacs непосредственно из терминала (emacs &) может помочь в решении этой проблемы.

  • Но если вы хотите изменить двоичный файл coqtop, используемый в ProofGeneral, вы можете установить параметр coq-prog-name, выполнив одно из следующих действий:

    • Интерактивно введите C -u C - c C -x (убить Coq), M-: (setq coq-prog -name "… / coqtop") и C - c C -n

    • Или создать файл .dir-locals.el (Стандартный conf-файл Emacs) в проекте root, содержащий: 

      ((coq-mode . ((coq-prog-name . "…/coqtop"))))

      и закрытие / повторное открытие файла ….v на карту (или просто выполните Mx нормальный режим RET или C -x C -v RET в уже открытом буфере ….v)

Относительно второго вы получаете ошибку, я немного озадачен, что Require Extraction вызывает эту ошибку, так как эта библиотека существует в Coq 8.6 и 8. 11.

На первый взгляд, я бы предложил повторно протестировать автокомпиляцию с Coq 8.11, утверждая From Coq Require Extraction. (вместо просто Require Extraction.)

Но, возможно, есть ошибка в функции PG Auto Compilation -> Compile before require; В любом случае, при необходимости откройте связанную проблему в трекере PG, сообщения об ошибках и запросы функций приветствуются: https://github.com/ProofGeneral/PG/issues

...