c++17在Linux vm上安装问题

Posted 2023-02-22

【中文标题】c++17在Linux vm上安装问题

【英文标题】：c++17 install problems on Linux vm

【发布时间】：2021-08-30 07:25:03

【问题描述】：

我正在使用 Travis CI 部署一个使用 z3 的 python 脚本。当我在我的（Windows）笔记本电脑和 VirtualBox 的 Linux VM 上运行它时，它可以工作。但是，使用 Travis CI，我无法正确下载 z3。我忘记了我尝试过的所有事情.. 现在我的 .travis.yml 文件中有这些命令

script:
  - git clone https://github.com/Z3Prover/z3.git
  - cd z3
  - python3 scripts/mk_make.py --python
  - cd build
  - make
  - sudo make install
  - cd ..
  - cd fall-2021/project
  - python -m unittest formula_gen_tests.py

但它在 make 命令上出错。我不知道该怎么办。

Type 'cd build; make' to build Z3
The command "python3 scripts/mk_make.py --python" exited with 0.
0.00s$ cd build
The command "cd build" exited with 0.
0.37s$ make
src/shell/gparams_register_modules.cpp
In file included from ../src/ast/normal_forms/nnf.h:22:0,
                 from ../src/shell/gparams_register_modules.cpp:5:
../src/ast/ast.h:50:19: fatal error: variant: No such file or directory
compilation terminated.
Makefile:4513: recipe for target 'shell/gparams_register_modules.o' failed
make: *** [shell/gparams_register_modules.o] Error 1
The command "make" exited with 2.
0.16s$ sudo make install
src/shell/gparams_register_modules.cpp
In file included from ../src/ast/normal_forms/nnf.h:22:0,
                 from ../src/shell/gparams_register_modules.cpp:5:
../src/ast/ast.h:50:19: fatal error: variant: No such file or directory
compilation terminated.
Makefile:4513: recipe for target 'shell/gparams_register_modules.o' failed
make: *** [shell/gparams_register_modules.o] Error 1
The command "sudo make install" exited with 2.

以前我尝试在 requirements.txt 中只使用 z3、z3-solver 或两者的组合，但它们都会导致错误，例如“z3 ImportError: cannot import name 'Solver'”等。所以我尝试了这个是我如何让它在我的 linux vm 上工作的。帮助！不确定哪些细节是相关的，请随时询问更多信息！

【参考方案1】：

variant 是 C++17 功能。 CI 机器上的编译器很可能不支持 C++17 的所有功能。如果可以，请确保您在该机器上获得了最新版本的 g++。

这里有一些进一步的讨论：c++ variant No such file or directory

【讨论】：

但是你在哪里放置 -std=c++17 标志我尝试了几个地方（除了你发送的链接中的其他命令）并且我收到了诸如 $ g++ -std=c++17 -o testcode1 ../src/shell/gparams_register_modules.cpp ../src/shell/gparams_regis 之类的错误不明白为什么z3提供的Makefile中不包含这个。我只有一个 .travis.yml 文件

确保您的 CI g++ 是最新版本。 g++ --version 产生什么？此外，最好将此标记为 C++ 问题，因为它与z3py 无关。

$ g++ --version g++ (Ubuntu 5.4.0-6ubuntu1~16.04.12) 5.4.0 20160609 不确定这意味着什么，根据谷歌最新的 g++ 版本是 1.42。另外，你说得对，我对这一切都非常不熟悉，所以当我问的时候，我没有意识到这不是 z3py 问题。

如果 Github 对文件大小有限制，那么你就不走运了。我假设您使用的是免费回购，它可能有这些限制。有一些方法可以使用 Travis 从 Internet 上下载文件，但它们都很挑剔。我建议您使用适当的 travis/CI 标签提出一个新问题，以寻求专家的帮助。

看看这一行，例如，几年前我是如何做到这一点的：github.com/LeventErkok/sbv/blob/…，它在 Travis 上“下载”了一个 z3 版本并将其解压缩。但我应该警告你，我自己已经放弃了；下载很挑剔，z3-release 的名称发生了变化；自动化很痛苦。但如果你真的需要这样的东西，它可以给你一个起点。