QuickChick "Ошибка: не удалось скомпилировать файл mli"

Question

Я успешно установил coq 8.9.1 и coq-quickchick 1.1.0 с opam 2.0.4 , и я программирую на emacs 26.1 .

Однако при выполнении команды QuickChick я получил следующую ошибку:

Ошибка: не удалось скомпилировать файл mli

Любые идеи о том, что я могу сделать?

Кроме того, перед попыткой команды QuickChick я попытался включить следующую команду: «QuickChickDebug Debug On.»

Тем не менее, никакого успеха и никаких инструктивных сообщений не было.

Answer 1

Вы можете попробовать извлечь и скомпилировать вручную.

Первая идея - заменить QuickChick my_prop. на Extraction TestCompile my_prop., что также попытается скомпилировать.

Также есть Separate Extraction my_prop. (при условии, что my_prop - это идентификатор), который просто выводит .ml файлов, чтобы вы могли скомпилировать их вручную и посмотреть, что не так.

Существуют и другие варианты извлечения, о которых стоит знать:

https://coq.inria.fr/distrib/current/refman/addendum/extraction.html#generating-ml-code