Возможно ли, что Z3 работает в системе, предоставляющей posix API без установки python?Установка Z3 на систему posix без python?
Я видел, что новая версия 4.3 использует python уже в процессе сборки (scripts/mk_make.py). Что такое более старые версии, такие как 4.1? Можно ли заставить его работать на posix без python?
Является ли Python недоступным в вашей системе?
Python всегда использовался для автоматического создания некоторых частей базы кода Z3. В первом выпуске исходного кода мы включили автоматически сгенерированный код. Фактически, в то время мы использовали комбинацию python + sed + awk + grep для генерации этих частей кода. Еще одна проблема с первым выпуском заключается в том, что система сборки для Windows (+ Visual Studio) полностью отличалась от системы сборки для других платформ. Makefile для Linux и OSX были получены из файлов проекта Visual Studio. Некоторые пользователи также начали сообщать о проблемах с системой сборки для Linux и OSX. Таким образом, чтобы уменьшить эти проблемы и имеют единую систему сборки, мы решили использовать Python (и только Python) для:
Python является очень привлекательным для нас, потому что он работает в большинстве систем (даже и не соответствует POSIX один с). Мы можем легко писать переносные скрипты. Более того, после того, как мы сделали коммутатор, мы можем скомпилировать Z3 на других платформах. Мы успешно скомпилировали его на Windows, Linux (Mint, Ubuntu, Suse и т. Д.), OSX, Cygwin и FreeBSD. В ветке «нестабильной» (так называемой «незавершенной работы») мы даже не требуем autoconf, мы используем python для выполнения всей конфигурации системы. Для сборки Z3 нам просто нужно: python, компилятор C++ (Visual Studio C++, g ++ или clang ++), ar (на платформе без окон), make (или nmake). Это очень маленький набор требований. По умолчанию Python доступен на большинстве платформ.
Это, как говорится, можно удалить требование python? Да, это так, но нужно заменить python чем-то другим. Что-то, что позволило бы нам выполнить все задачи, описанные выше. Взгляните в каталог scripts на http://z3.codeplex.com/SourceControl/changeset/view/0c1f2a82818a, , мы должны были бы перенести все эти сценарии автоматизации на что-то, что можно использовать на всех поддерживаемых нами платформах.