0

我正在尝试在 VSCode (Mac) 的 OCaml 中使用 Z3。

为了使用它，我编写了以下代码：open Z3但它向我提出了以下错误：Unbound module Z3 Merlin所以我理解 Z3 没有安装。

但是，我刚刚运行：opam install z3，所以它应该可以工作。

我也意识到这open Num是可行的，所以可能与使用旧版本的 OCaml 有关（因为Num现在已弃用）。

有什么帮助吗？

编辑：

我刚刚发现 Z3 没有正确安装在opam install z3零件中。这是抛出的消息：

[ERROR] The compilation of z3 failed at
        "/Users/.../.opam/opam-init/hooks/sandbox.sh build make -C
        build -j 3".

#=== ERROR while compiling z3.4.8.9-1 =========================================#
# context     2.0.8 | macos/x86_64 | ocaml-base-compiler.4.10.2 | https://opam.ocaml.org#ff95b837
# path        ~/.opam/4.10.2/.opam-switch/build/z3.4.8.9-1
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -C build -j 3
# exit-code   2
# env-file    ~/.opam/log/z3-21131-e7966f.env
# output-file ~/.opam/log/z3-21131-e7966f.out
### output ###
# /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:641:18: error: no template named 'numeric_limits'
# [...]
#                  ^
# /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:641:50: error: no template named 'numeric_limits'
#     int _Bits = (numeric_limits<_IntT>::digits - numeric_limits<_FloatT>::digits)>
#                                                  ^
# /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:646:17: error: no template named 'numeric_limits'
#   static_assert(numeric_limits<_FloatT>::radix == 2, "FloatT has incorrect radix");
#                 ^
# fatal error: too many errors emitted, stopping now [-ferror-limit=]
# 20 errors generated.
# make: *** [util/luby.o] Error 1
# make: *** Waiting for unfinished jobs....



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>   
┌─ The following actions failed
│ λ build z3 4.8.9-1

它给了我一个与 Xcode 相关的错误...

我想纠正这个会产生纠正原来的unbound module错误。是这样吗？有什么帮助吗？

4

0 回答 0