OCaml и препроцессор имеют ошибку несовместимых версий при установке tcoq

Я пытался установить tcoq, и у меня была следующая ошибка:

"/Users/pinocchio/.opam/4.05.0/bin/ocamlfind" ocamlc -rectypes  -w -3-52-56 -c grammar/compat5.ml
OCAMLC -c -pp grammar/gramCompat.mlp
>> Fatal error: OCaml and preprocessor have incompatible versions
Fatal error: exception Misc.Fatal_error
make[1]: *** [grammar/gramCompat.cmo] Error 2
make: *** [submake] Error 2

кто-то знает:

  1. Что значит ошибка?
  2. Как это исправить?

Я видел похожие посты онлайн:

https://coq-club.inria.narkive.com/h4i0KOH0/problem-compiling-coq

но это было не очень полезно. Я сделал:

ocaml -I +camlp5

как они предложили, и, кажется, работает нормально...

Я сделал make clean но это не помогло


Я только что понял, что пропустил шаг 3 из INSTALL, но idk, если он связан с проблемой или что я собираюсь делать с ним:

3- The uncompression and un-tarring of the distribution file gave birth
   to a directory named "coq-8.xx". You can rename this directory and put
   it wherever you want. Just keep in mind that you will need some spare
   space during the compilation (reckon on about 300 Mb of disk space
   for the whole system in native-code compilation). Once installed, the
   binaries take about 30 Mb, and the library about 200 Mb.

Я пытаюсь установить геймпад, и для этого нужно следовать инструкциям. В частности, я выполнил следующие 3 команды:

opam switch 4.05.0
opam install camlp4
opam install ocamlfind

Самая последняя ошибка:

make
/Library/Developer/CommandLineTools/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build
OCAMLC -c -pp grammar/gramCompat.mlp
>> Fatal error: OCaml and preprocessor have incompatible versions
Fatal error: exception Misc.Fatal_error
make[1]: *** [grammar/gramCompat.cmo] Error 2
make: *** [submake] Error 2

после прочтения этой ошибки мне чудом пришло в голову распечатать версию обоих ocaml а также camlp5:

$ camlp5 -v
Camlp5 version 7.07 (ocaml 4.07.0)

а также:

ocaml
    OCaml version 4.05.0

так очевидно, что это неправильно, поэтому, возможно, первый шаг - это исправить camlp5 работать с 4.05.0 так как это тот, который мне нужен.


Я пытался удалить camlp5 но он отказался!

brew uninstall camlp5
Error: Refusing to uninstall /usr/local/Cellar/camlp5/7.07
because it is required by coq, which is currently installed.
You can override this and force removal with:
  brew uninstall --ignore-dependencies camlp5

1 ответ

Кажется, вы уже поняли, что означает ошибка. Версия OCaml, к которой относится ваш локальный camlp5 исполняемый файл отличается от версии OCaml, через которую вы используете opam, Позвольте мне перейти (каламбур) прямо ко второй части вашего вопроса.

Основная проблема заключается в том, что вы используете два разных источника для пакетов OCaml, а именно ваш менеджер пакетов (например, brew) а также opam, Чтобы решить вашу проблему, вы должны установить эти пакеты только из одного источника. Я бы посоветовал opam, поскольку он позволяет вам легко управлять различными версиями OCaml через коммутаторы.

Просто удалите свою локальную версию camlp5 используя, например,

brew uninstall camlp5

затем установите его, используя opam:

opam install camlp5

Этот совет также относится к другим пакетам OCaml, таким как ocamlbuild, camlp4, так далее.

Другие вопросы по тегам