Блог

Главная - Вопросы по программированию - Z3-OCaml не работает: Несвязанный модуль Z3 Merlin

Z3-OCaml не работает: Несвязанный модуль Z3 Merlin

#visual-studio-code #ocaml #z3 #opam #merlin

Вопрос:

Я пытаюсь использовать Z3 в OCaml в VSCode (Mac).

Чтобы воспользоваться этим, я написал следующий код: 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 ошибки. Так ли это на самом деле? Есть какая-нибудь помощь в этом?

Комментарии:

1. Из того, что я вижу, я могу сказать, что ваша версия компилятора C очень старая, поэтому вам необходимо обновить ее либо путем обновления операционной системы, либо установки более нового компилятора от некоторых сторонних менеджеров пакетов. Честно говоря, я сам не могу установить z3 на свою машину macOS из-за очень старой версии macOS. Возможно, более простым вариантом было бы запустить виртуальную машину Linux.

2. Вы уверены, что это связано с z3? Мне кажется, что компиляция не выполняется для какой-то другой части цепочки инструментов. (Возможно, вызвано из z3, но, похоже, не имеет прямого отношения к самим источникам z3.)

3. В качестве идеи: посмотрите, можете ли вы удалить часть Visual-Studio из своей среды. т. Е. Попробуйте посмотреть, можете ли вы установить обычные привязки O’Caml для z3, которые будут использоваться непосредственно из командной строки. Как только это будет сделано, вы сможете изучить часть Visual-Studio. (Я предполагаю, что эта ошибка напрямую связана с битами Visual-Studio.)

4. Спасибо вам обоим, я постараюсь это исправить!

Метки: