Pin*_*hio 5 ocaml coq camlp4 coq-plugin
我正在尝试安装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
Run Code Online (Sandbox Code Playgroud)
有人知道吗:
我在网上看到了相关的帖子:
https://coq-club.inria.narkive.com/h4i0KOH0/problem-compiling-coq
但这并不是很有帮助。我做了:
ocaml -I +camlp5
Run Code Online (Sandbox Code Playgroud)
正如他们建议的那样,它似乎工作正常...
我确实做了,make clean
但这没有帮助。
我只是意识到我跳过了INSTALL的第3步,但是如果它与问题或Im打算怎么做有关,则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.
Run Code Online (Sandbox Code Playgroud)
我正在尝试安装游戏手柄,并且需要按照说明进行操作。特别是我运行了以下3个命令:
opam switch 4.05.0
opam install camlp4
opam install ocamlfind
Run Code Online (Sandbox Code Playgroud)
最新错误:
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
Run Code Online (Sandbox Code Playgroud)
读取错误奇迹般地发生,我同时打印的版本之后ocaml
和camlp5
:
$ camlp5 -v
Camlp5 version 7.07 (ocaml 4.07.0)
Run Code Online (Sandbox Code Playgroud)
和:
ocaml
OCaml version 4.05.0
Run Code Online (Sandbox Code Playgroud)
所以很明显那是错误的,所以也许第一步就是要修复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
Run Code Online (Sandbox Code Playgroud)
看来您已经知道错误的含义。本地camlp5
可执行文件所针对的OCaml版本与您通过所使用的OCaml版本不同opam
。让我直接切换(双关语)到您的问题的第二部分。
这里的主要问题来自以下事实:您为OCaml软件包使用了两种不同的来源,即软件包管理器(例如brew
)和opam
。为了解决您的问题,您应该仅从一个来源安装这些软件包。我建议使用opam
,因为它可以让您通过开关轻松管理不同的OCaml版本。
只需卸载本地版本即可camlp5
,例如,
brew uninstall camlp5
Run Code Online (Sandbox Code Playgroud)
然后使用安装opam
:
opam install camlp5
Run Code Online (Sandbox Code Playgroud)
这个建议也适用于其他OCaml的包,比如ocamlbuild
,camlp4
等