z3 ocaml переплет не работает (Windows 7)

Question

У меня не работает привязка z3 ocaml для Windows 7. Вот процесс, которому я следовал.

1. Установлено Objective Caml версия 3.11.0 (набор инструментов Microsoft)
2. Установленоcamlidl-1.05 (построено с использованием Microsoft Visual Studio 2008 + cygwin)
3. Установлено z3-3.0
4. Построена привязка z3 ocaml с помощью команды build.cmd. Сборка прошла успешно.
5. Скопировал файлы, сгенерированные "build.cmd" из z3 / ocaml в ObjectiveCaml / lib

6. Запустил интерактивный ocaml и загрузил "z3.cma"

   # #load "z3.cma";;
   Characters -1--1:
     #load "z3.cma";;
   
   Error: The external function `get_theory_callbacks' is not available
   
   # Z3.mk_context;;
   Characters -1--1:
     Z3.mk_context;;
   
   Error: The external function `camlidl_z3_Z3_mk_context' is not available
   

Может кто-нибудь дать мне несколько советов?

РЕДАКТИРОВАТЬ 1: Создание примера в "Z3-3.0 \ examples \ ocaml":

Выдержка из build.cmd

set XCFLAGS=/nologo /MT /DWIN32
ocamlopt -ccopt "%XCFLAGS%" -o test_mlapi.exe -I ..\..\ocaml ole32.lib %OCAMLLIB%\libcamlidl.lib z3.cmxa test_mlapi.ml

При выполнении build.cmd в командной строке Visual Studio 2008

я получил следующую ошибку

** Fatal error: Cannot find file "/nologo"
File "caml_startup", line 1, characters 0-1:
Error: Error during linking

При удалении -ccopt "%XCFLAGS%" работает нормально.Сгенерированный exe также выполняется должным образом.(Обратите внимание, что у меня есть flexdll в PATH).Есть идеи, почему это может происходить?

Answer 1

OCaml версии 3.11 и более поздних версий вызывает компоновщик через flexdll, который не нуждается или не знает о флагах "/ nologo / MT / DWIN32". Сценарий ocaml \ build.cmd проверяет версию ocaml и соответствующим образом устанавливает XCFLAGS. Я думаю, что примеры \ ocaml \ build.cmd должны быть изменены, чтобы сделать то же самое.

Использование Z3 из верхнего уровня работает для меня, если я создаю пользовательский верхний уровень, выполняя 'ocamlmktop -o ocamlz3 z3.cma' из каталога привязок Z3 ocaml.

Answer 2

Вот что у меня получилось (Windows 7):

1. Загрузить и установить Ocaml 3.08+
2. Загрузить и установить Visual Studio C ++
3. Загрузитьи распакуйте CamlIDL
4. . Загрузите и установите cygwin, при установке выберите пакет make , а также ваш любимый пакет редактора linux в окне «Выбор пакета».
5. Открыть cygwin
6. В cygwin перейдите в корневой каталог CamlIDL
7. Переименовать config/Makefile.win32 в config/Makefile
8. Открыть config/Makefile с помощьюредактор
9. Редактирование BINLIB и OCAMLLIB переменных
10. Сохранение и выход из компилятора Makefile
11. Setup c для cygwin: Вызовcl.exe (компилятор MSVC) в оболочке Cygwin
12. Запуск make all из корневого каталога CamlIDL
13. Запуск make install
14. Выход из Cygwin
15. Загрузка и установка Z3
16. Загрузка и установка FlexDLL: http://alain.frisch.fr/flexdll.html
17. Нажмите Пуск, выберите Мой компьютер, щелкните правой кнопкой мыши, выберите Свойства, укажитев System Protection, выберите вкладку Advanced, укажите значения среды ...
18. Добавьте C:\Program Files\flexdll\ и C:\Program Files\Microsoft Research\Z3-<version-number>\bin\ к переменной Path
19. Нажмите кнопку Пуск, выберите Все программы, укажитеMicrosoft Visual Studio, выберите Инструменты Visual Studio, а затем нажмите Командная строка Visual Studio.
20. В командной строке Visual Studio перейдите на C:\Program Files\Microsoft Research\Z3-<version-number>\ocaml
21. Открыть build.cmd с помощью редактора
22. Удалить переменную %CD% из двух последних команд
23. Сохраните и закройте build.cmd
24. Запустите build.cmd
25. Скопируйте файлы z3 * и libz3.lib, созданные build.cmd, из z3/ocaml в %OCAMLLIB%
26. Выполнить ocamlmktop -o ocamlz3 z3.cma %OCAMLLIB%\libcamlidl.lib ole32.lib
27. Выполнить ocamlz3.exe
28. Тип #use "../examples/ocaml/test_mlapi.ml";;

29. Попробуйте simple_example();;​

30. На последнем шаге должен быть получен правильный вывод из Z3.

Для Debian / Ubuntu:

1. Установите Ocaml 3.09+ 1. sudo apt-get install camlidl​
2. git clone git://github.com/polazarus/z3-installer.git (от Микаэля Делахэ)
3. cd z3-installer
4. make # скачать Z3 И собрать библиотеку Ocaml (нативную и байтовую)
5. sudo make install # установить двоичный файл Z3, DLL и библиотеку Ocaml
6. sudo cp z3/lib/libz3.so /usr/lib/
7. cd z3/ocaml
8. ocamlmktop -o ocamlz3 z3.cma
9. . /ocamlz3
10. Попробуйте следующий фрагмент кода:

let simple_example() =
begin
Printf.printf "\nsimple_example\n";
let ctx = Z3.mk_context_x (Array.append [|("MODEL", "true")|] [||]) in
Printf.printf "CONTEXT:\n%sEND OF CONTEXT\n" (Z3.context_to_string ctx); Z3.del_context ctx;
end;;
simple_example();;​