在没有python的posix系统上安装Z3? [英] Installation of Z3 on a posix system without python?

问题描述

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

Is it possible to get Z3 running on a system providing posix API without having python installed?

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

I have seen the new version 4.3 uses python already in the build-process (scripts/mk_make.py). Whats about older versions like 4.1? Is it imaginable to get it to run on posix without python?

推荐答案

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

Is Python not available in your system?

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

Python was always used to automatically generate some parts of the Z3 code base. In the first source code release, we have included the automatically generated code. Actually, at that time, we were using a combination of python + sed + awk + grep to generate these parts of the code. Another problem with the first release is that the build system for Windows (+ Visual Studio) was completely different from the build system for the other platforms. The Makefiles for Linux and OSX were derived from Visual Studio Project files. Some users also started to report problems with the build system for Linux and OSX. So, to reduce these problems and have a uniform build system, we decided to use python (and python only) to:

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

Python 对我们非常有吸引力，因为它适用于大多数系统(甚至不符合 posix 的系统).我们可以轻松编写可移植的脚本.而且，我们做了切换之后，可以在更多平台上编译Z3.我们在 Windows、Linux(Mint、Ubuntu、Suse 等)、OSX、Cygwin 和 FreeBSD 上成功编译了它.在unstable"(即working-in-progress)分支中，我们甚至不再需要autoconf，我们使用python 来完成所有系统特定的配置.要构建 Z3，我们只需要:python、C++ 编译器(Visual Studio C++、g++ 或 clang++)、ar(在非 Windows 平台上)、make(或 nmake).这是非常小的一组要求.默认情况下，Python 在大多数平台上都可用.

Python is very attractive for us because it works in most systems (even non posix compliant ones). We can easily write portable scripts. Moreover, after we made the switch, we can compile Z3 in more platforms. We successfully compiled it on Windows, Linux (Mint, Ubuntu, Suse, etc), OSX, Cygwin, and FreeBSD. In the "unstable" (aka working-in-progress) branch, we don't even require autoconf anymore, we use python to do all system specific configuration. To build Z3, we just need: python, C++ compiler (Visual Studio C++, g++ or clang++), ar (on non-windows platform), make (or nmake). This is very small set of requirements. Python is available in most platforms by default.

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

That being said, is it possible to remove the python requirement? Yes, it is, but it would have to replace python with something else. Something, that would allows us to perform all tasks described above. Take a look in the directory scripts at http://z3.codeplex.com/SourceControl/changeset/view/0c1f2a82818a, we would have to port all these automation scripts to something that can be used on all platforms we support.

这篇关于在没有python的posix系统上安装Z3?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！