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

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

0 голосов
/ 26 декабря 2018

Я пытался установить 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 Ответ

0 голосов
/ 28 декабря 2018

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

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

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

brew uninstall camlp5

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

opam install camlp5

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

...