Coq файл, сгенерированный WP не компилируется - PullRequest
2 голосов
/ 08 марта 2019

Я установил frama-c (18.0) и coqide (8.9) через opam (плюс, конечно, другие необходимые зависимости, но здесь это может быть не так). Дело в том, что я просто установил его через opam, а не сделал ничего странного (и я не увидел какой-либо конкретной инструкции, которую я должен был бы сделать иначе).

Frama-c работает, как и ожидалось, когда я использую Alt-ergo с WP, но если я пытаюсь использовать coq или coqide вместо Alt-ergo, то я получаю следующую ошибку для каждой цели, которую Qed не удается доказать немедленно :

[wp] 13 goals scheduled
[wp] [Coq] 'Qed.v' compilation failed.
------------------------------------------------------------
--- Coqc (stderr) :
------------------------------------------------------------
File "/tmp/wp7fe5dc.dir/coqwp/Qed.v", line 27, characters 8-17:
Error:
Cannot find a physical path bound to logical path matching suffix bool.

------------------------------------------------------------
[wp] [Coq] Goal typed_nondet_loop_inv_preserved : Failed
  Compilation of 'Qed.v' failed.

Как примечание, перед отображением ошибки ему удается скомпилировать некоторые другие файлы .v. Я попытался вручную открыть файлы в coqide, и я получил тот же результат. Для справки вот строки, на которые жалуется coq:

Require bool.Bool.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require real.Real.
Require real.RealInfix.
Require real.FromInt.

Я также попытался немного понизить coq, но не ниже 8.7 (так как в противном случае opam жалуется на несовместимый базовый установочный пакет, и я не хочу испортить мою установку), и получил тот же результат.

Если бы кто-то имел представление о том, что является причиной этого, и как я могу это настроить, это было бы неплохо. Даже если для того, что я сейчас делаю с ним, достаточно Alt-ergo, мне бы хотелось немного поиграть с coq, чтобы посмотреть, как его можно использовать.

С уважением,

-

Винсент Пенель.

1 Ответ

1 голос
/ 08 марта 2019

Во-первых, действительно, вам нужно coq <<code>8.8 (например, 8.7.2), если вы хотите использовать его с Frama-C / WP, так как более новые версии на данный момент не поддерживаются.

Во-вторых, важен порядок установки пакетов. В частности, если соответствующая версия coq была установлена ​​после frama-c, WP не скомпилировал и не установил библиотеки coq, которые здесь отсутствуют. Таким образом, вы можете захотеть сделать opam reinstall frama-c для компиляции пакета с совместимой coq версией.

Добро пожаловать на сайт PullRequest, где вы можете задавать вопросы и получать ответы от других членов сообщества.
...