【问题标题】:Error installing Frama-C with opam (Ubuntu 14.04 LTS)使用 opam 安装 Frama-C 时出错(Ubuntu 14.04 LTS)
【发布时间】:2017-04-21 00:41:12
【问题描述】:

尝试使用推荐的 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

【问题讨论】:

  • 需要更多信息。您能否提供opam install -v frama-c-base 的输出,以便我们获得编译期间启动的命令的输出?请注意,生成的输出会很大,因此您可能希望将其重定向到文件,例如使用opam install -v frama-c-base | tee opam.log 并提供指向opam.log 的链接。
  • 这不是您安装问题的直接解决方案,但您能切换到 OCaml 4.02.3 吗?该编译器提供了更新版本的 Frama-C (20161101),有望防止该问题发生。与以前的版本相比,它还具有一般改进和错误修复的额外好处。
  • 我还建议直接安装包frama-c,而不是frama-c-base。唯一的区别是frama-c 包含一些额外的依赖项,例如,如果您希望能够运行 GUI。如果您不能直接安装frama-c,您应该只选择frama-c-base(例如,您的系统对于某些依赖项没有兼容的C 包)。您可以使用opam install depext; opam depext frama-c 来帮助安装 Frama-C 使用的外部依赖项(例如 C 库)。

标签: frama-c opam


【解决方案1】:

我能够重现该问题,罪魁祸首似乎是 Make 4.2,尤其是由于 this bug

错误 #44742:未构建双冒号规则的双深度 [并行构建]

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 的并行编译,从而避免错误。

不过,我的一般建议是:

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

  2. 如果可以的话,安装frama-c 本身,而不是frama-c-base,因为唯一的区别是所需的包,即那些用于GUI 的包。在运行 opam install frama-c 之前,您可能需要执行以下操作:

    opam install depext
    opam depext frama-c
    

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

【讨论】:

  • 感谢这工作。我不确定为什么我最终使用了 OCaml 4.02.1,在安装 opam 之前,我的系统上没有 ocaml 编译器。
  • 4.02.1 是opam_installer.sh 安装的默认版本。也许他们现在应该更新它,但这可能会破坏现有的脚本,我想......
  • 顺便说一句,如果您可以将您正在使用的发行版添加到问题中,这可以帮助指导经常使用 google 使用诸如“frama-c opam error ubuntu”之类的表达式的用户。 .. 它还可以帮助我们了解是否存在受此 Make 问题影响的主要发行版。
  • 完成。 Ubuntu 14.04 LTS 存储库提供了 Make 3.81,由于模式替换规则 stackoverflow.com/a/42748870/2466305 中的一个错误,我最近已经更新了它
猜你喜欢
  • 1970-01-01
  • 1970-01-01
  • 1970-01-01
  • 2015-05-31
  • 2015-08-30
  • 1970-01-01
  • 2015-09-25
  • 2016-02-24
  • 1970-01-01
相关资源
最近更新 更多