使用 opam (Ubuntu 14.04 LTS) 安装 Frama-C 时出错
Error installing Frama-C with opam (Ubuntu 14.04 LTS)
尝试使用推荐的 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
我能够重现这个问题,罪魁祸首似乎是 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
成功)。如果我在没有 -j
的情况下手动编译 Frama-C,我也没有问题。
如果您无法更新您的 Make 版本,您可以尝试使用 opam install -j 1 frama-c
,它应该会覆盖 jobs
变量并禁用 Frama-C 的并行编译,从而避免错误。
不过,我的一般建议是:
安装更新的 OCaml(至少 4.02.3,它应该兼容 OCaml 4.02.1 中几乎所有可用的包)以确保最新版本的 Frama-C 可用( Frama-C Silicon 在 OCaml 4.02.1 中不可用);
如果可以,安装 frama-c
本身,而不是 frama-c-base
,因为唯一的区别是所需的包,即 GUI 的包。您可能需要在 运行 opam install frama-c
之前执行以下操作:
opam install depext
opam depext frama-c
第一行将安装depext
,它能够为您的发行版找到外部依赖项,第二行将 depext 应用于 Frama-C,从而提示您安装您的发行版中可用的外部依赖项.
尝试使用推荐的 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
我能够重现这个问题,罪魁祸首似乎是 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
成功)。如果我在没有 -j
的情况下手动编译 Frama-C,我也没有问题。
如果您无法更新您的 Make 版本,您可以尝试使用 opam install -j 1 frama-c
,它应该会覆盖 jobs
变量并禁用 Frama-C 的并行编译,从而避免错误。
不过,我的一般建议是:
安装更新的 OCaml(至少 4.02.3,它应该兼容 OCaml 4.02.1 中几乎所有可用的包)以确保最新版本的 Frama-C 可用( Frama-C Silicon 在 OCaml 4.02.1 中不可用);
如果可以,安装
frama-c
本身,而不是frama-c-base
,因为唯一的区别是所需的包,即 GUI 的包。您可能需要在 运行opam install frama-c
之前执行以下操作:opam install depext opam depext frama-c
第一行将安装
depext
,它能够为您的发行版找到外部依赖项,第二行将 depext 应用于 Frama-C,从而提示您安装您的发行版中可用的外部依赖项.