无法使用 opam 安装 frama-c-Phosphorus

Question

我已经按照说明使用 opam 成功安装了 frama-c-Silicon，但是当我想升级到 Phosphorus 时，opam 不起作用。

我使用了命令：

opam pin add frama-c Downloads/frama-c-Phosphorus20170501.tar.gz

它说：

[NOTE] Package frama-c is already path-pinned to
       /home/talos/Downloads/frama-c-Phosphorus-20170501.tar.gz.
       This will erase any previous custom definition.
Proceed ? [Y/n] y

[frama-c] /home/talos/Downloads/frama-c-Phosphorus-20170501.tar.gz synchronized

frama-c needs to be installed.
The following actions will be performed:
  ∗  install frama-c-base 20161101*           [required by frama-c]
       Why3 can be used by the WP plug-in for running additional automatic solvers
       Coq can be used with the WP plug-in for proving interactively proof obligations
  ∗  install frama-c      20161101*
       Alt-Ergo Graphical Interface can be used by the WP plug-in
===== ∗  2 =====
Do you want to continue ? [Y/n] y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[frama-c.20161101] /home/talos/Downloads/frama-c-Phosphorus-20170501.tar.gz already up-to-date
[frama-c-base.20161101] /home/talos/Downloads/frama-c-Phosphorus-20170501.tar.gz already up-to-date

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

#=== ERROR while installing frama-c-base.20161101 =============================#
These patches didn't apply at /home/talos/.opam/system/build/frama-c-base.20161101:
  - 4.05-support.patch



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions were aborted
  ∗  install frama-c 20161101
The following actions failed
  ∗  install frama-c-base 20161101
No changes have been performed
[NOTE] Pinning command successful, but your installed packages may be out of
       sync.

Answer 1

我认为您的问题更多地与 OPAM 本身（尤其是opam pin）的使用有关，而不是 Frama-C。

这一行特别表明您在 OPAM 安装中有pinned 一个 Frama-C 包：

[NOTE] Package frama-c is already path-pinned to
       /home/talos/Downloads/frama-c-Phosphorus-20170501.tar.gz.
       This will erase any previous custom definition.

这仅在 OPAM 中提供 Phosphorus 包之前是必需的。您应该通过删除它然后通过“标准”（非固定）方式安装它来恢复到默认配置：

opam pin remove frama-c
# just in case, you may want to unpin the frama-c-base package, if it is pinned
opam pin remove frama-c-base
# then install the package normally; you may need to update OPAM to make
# sure the package is available in your repository
opam update
opam install frama-c

请注意，如果您仍然显示如下消息：

The following actions will be performed:
  ∗  install frama-c-base 20161101*           [required by frama-c]

这可能表明 OPAM 的约束存在问题。

Phosphorus 版本的版本号是20170501。除此之外的任何东西都意味着你不会得到磷，而是旧版本。不值得继续：问题必须事先解决。