4

是否可以在没有安装 python 的情况下让 Z3 在提供 posix API 的系统上运行？

我已经看到新版本 4.3 已经在构建过程中使用了 python (scripts/mk_make.py)。像 4.1 这样的旧版本呢？可以想象让它在没有 python 的情况下在 posix 上运行吗？

4

1 回答 1

2

Python 在您的系统中不可用吗？

Python 一直用于自动生成 Z3 代码库的某些部分。在第一个源代码版本中，我们已经包含了自动生成的代码。实际上，当时我们正在使用 python + sed + awk + ​​grep 的组合来生成这部分代码。第一个版本的另一个问题是 Windows (+ Visual Studio) 的构建系统与其他平台的构建系统完全不同。Linux 和 OSX 的 Makefile 源自 Visual Studio 项目文件。一些用户还开始报告 Linux 和 OSX 的构建系统存在问题。因此，为了减少这些问题并拥有统一的构建系统，我们决定使用 python（和仅 python）来：

  • 自动生成代码（用于不同语言的绑定、API 日志支持等）
  • 检查系统的要求
  • 生成 Makefile
  • 以及任何其他形式的自动化

Python 对我们来说非常有吸引力，因为它适用于大多数系统（甚至是不符合 posix 的系统）。我们可以轻松编写可移植脚本。而且，我们进行切换后，我们可以在更多平台上编译Z3。我们在 Windows、Linux（Mint、Ubuntu、Suse 等）、OSX、Cygwin 和 FreeBSD 上成功编译了它。在“不稳定”（又名正在工作的）分支中，我们甚至不再需要 autoconf，我们使用 python 来进行所有系统特定的配置。要构建 Z3，我们只需要：python、C++ 编译器（Visual Studio C++、g++ 或 clang++）、ar（在非 Windows 平台上）、make（或 nmake）。这是非常小的一组要求。默认情况下，Python 在大多数平台上都可用。

话虽如此，是否可以删除 python 要求？是的，它是，但它必须用其他东西替换 python。可以让我们执行上述所有任务的东西。scripts查看http://z3.codeplex.com/SourceControl/changeset/view/0c1f2a82818a的目录，我们必须将所有这些自动化脚本移植到可以在我们支持的所有平台上使用的东西。

于 2012-11-30T16:54:02.040 回答