区分自制软件中的 z3 选项

Distinguishing between z3 options in homebrew

homebrew中,如果我选择安装z3,我得到以下结果:

▶ brew install z3
Error: Formulae found in multiple taps: 
 * homebrew/science/z3
 * mht208/formal/z3

Please use the fully-qualified name e.g. homebrew/science/z3 to refer the formula.

一方面,homebrew 公式可能看起来更规范,因为它是主存储库(或者在 homebrew 中称为顶级项目的任何东西),但另一方面 mht208 据我所知是 z3 的开发者。有没有一种简单的方法可以确定这两者中哪一个具有最新版本或最稳定的版本?

编辑以添加其他信息: 当我在每个完全限定名称上 运行 brew info 时,我得到以下结果:

▶ brew info homebrew/science/z3
homebrew/science/z3: stable 4.4.0 (bottled), HEAD
A high-performance theorem prover
https://github.com/Z3Prover/z3
/usr/local/Cellar/z3/4.4.0_1 (50 files, 38M) *
  Poured from bottle
From: https://github.com/Homebrew/homebrew-science/blob/master/z3.rb

▶ brew info mht208/formal/z3
mht208/formal/z3: stable 4.4.0
https://github.com/Z3Prover/z3
/usr/local/Cellar/z3/4.4.0_1 (50 files, 38M) *
  Poured from bottle
From: https://github.com/mht208/homebrew-formal/blob/master/z3.rb
==> Dependencies
Build: autoconf ✔
==> Options
--with-ocaml
    Build ocaml bindings with the ocaml from Homebrew.
--with-opam
    Build ocaml bindings with the ocaml from OPAM.

所以,理论上,这两个 似乎 是相同的版本 (4.4.0_1),除了 mht208 版本有一些选项并且取决于在 autoconf 上(已安装)。这也引出了一个问题,即 ocaml 绑定的构建方式是否有所不同(ocamlopam 都已安装)。

通过 Homebrew 查看更多信息非常容易:

$ brew info homebrew/science/z3
homebrew/science/z3: stable 4.4.0 (bottled), HEAD
A high-performance theorem prover
https://github.com/Z3Prover/z3
Not installed
From: https://github.com/Homebrew/homebrew-science/blob/master/z3.rb

这向我们表明此公式包含版本 4.4.0,它是 bottled,并且您可以安装 HEAD 版本(通过 brew install homebrew/science/z3 --HEAD)。

看看另一个公式:

$ brew info mht208/formal/z3
mht208/formal/z3: stable 4.4.0
https://github.com/Z3Prover/z3
Not installed
From: https://github.com/mht208/homebrew-formal/blob/master/z3.rb
==> Dependencies
Build: autoconf ✔
==> Options
--with-ocaml
        Build ocaml bindings with the ocaml from Homebrew.
--with-opam
        Build ocaml bindings with the ocaml from OPAM.

我们看到现在有一​​些选项可用于此公式,而其他公式中没有。现在,我们不知道这是因为不同的默认值还是其他原因,除非我们真的去看看公式。这是 the homebrew/science one (very simple formula, essentially just calling make install), and here's the mht208/formal one(复杂得多)。

它们都是同一个版本,所以就稳定性而言,我认为这是一个折腾。 Homebrew 的人在他们所做的事情上做得很好,所以我建议其他人坚持使用 Homebrew,除非你能证明软件中没有解决的问题。当然,如果可以的话,在主线 Homebrew 存储库中修复它通常不会太困难。 :) 但是,如果您需要第二个公式的更复杂功能(构建 ocaml 绑定等等),那么您当然应该使用第二个公式。