Я установил 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, чтобы посмотреть, как его можно использовать.
С уважением,
-
Винсент Пенель.