frama-c - 使用 opam 安装 Frama-C 时出错 (Ubuntu 14.04 LTS)

Question

尝试使用推荐的 opam 方法安装 Frama-C 会出现以下错误:

### stdout ###
# Cleaning     Installation directory
# Installing   WP shared files
### stderr ###
# /bin/sh: 1: src/plugins/wp/share/instwp: not found
# make: *** [src/plugins/wp/Makefile:355: install] Error 127

这里是使用的命令:

# install opam
$ wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin
# configure opam
$ eval `opam config env`
$ opam config setup -a
# install frama-c
$ opam install frama-c-base

编辑:这是 opam install -v frama-c-base 的输出:https://pastebin.com/eMH08ugA

Edit2:有问题的系统正在运行 Linux Mint 17.3(Ubuntu 14.04 LTS 上游)；软件存储库中的 Ubuntu 软件包是 Make 3.81(未经测试)，尽管遇到此错误时已经升级到 Make 4.2

Answer 1

我能够重现这个问题，罪魁祸首似乎是 Make 4.2，因为 this bug特别是:

bug #44742: Double-dep with double-colon rule not built [in parallel builds]

Frama-C makefile 中的多个规则使用双冒号，默认情况下，-j%{jobs}% 在 opam Frama-C 文件中设置为加快编译速度。

不幸的是，在使用特定版本的 Make 时，尽管 WP makefile 中存在其规则，但似乎这两个结果的组合导致 instwp 文件(以及其他文件)无法构建.

我默认使用 Make 4.2.1，没有这个问题(所有文件都按预期生成，并且 make install 成功)。如果我手动编译 Frama-C 而不使用 -j，我也不会遇到这个问题。

如果您无法更新 Make 版本，可以尝试使用 opam install -j 1 frama-c，它应该覆盖 jobs 变量并禁用并行Frama-C的编译，从而避免了错误。

不过，我的一般建议是:

1. 安装较新的 OCaml(至少 4.02.3，它应该兼容 OCaml 4.02.1 中几乎所有可用的软件包)，以确保最新版本的 Frama-C 可用(Frama-C Silicon在 OCaml 4.02.1 中不可用)；

2. 如果可以的话，请安装 frama-c 本身，而不是 frama-c-base，因为唯一的区别是所需的软件包，即图形用户界面。在运行 opam install frama-c 之前，您可能需要执行以下操作:

   opam install depext
   opam depext frama-c
   

   第一行将安装 depext，它能够为您的发行版找到外部依赖项，第二行将把 depext 应用到 Frama-C，从而提示您安装您的发行版中可用的外部依赖项分布。