如何为MacOSX构建leon？

Question

我试着按照指示从github上的MacOSX文件构建leon (yosemite)。

它运行得很好，只是在运行基本测试时，没有找到scalaz3库时遇到了问题：

 $ ./leon ./testcases/verification/sas2011-testcases/RedBlackTree.scala
java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1865)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1122)
    at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
    at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
    at z3.scala.Z3Config.<init>(Z3Config.scala:6)
    at leon.solvers.z3.FairZ3Solver.<init>(FairZ3Solver.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1$$anon$1.<init>(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anon$12.getNewSolver(SolverFactory.scala:18)
    at leon.verification.AnalysisPhase$.checkVC(AnalysisPhase.scala:129)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:111)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:110)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at leon.verification.AnalysisPhase$.checkVCs(AnalysisPhase.scala:110)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:45)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:15)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:236)
    at leon.Main$.main(Main.scala:220)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

我试图从EPFL构建ScalaZ3包，这需要构建微软的Z3 (来自github)。构建z3本身可以找到，但是构建ScalaZ3失败了，缺少了一个"gomp“库：

[error] ld: library not found for -lgomp
[error] clang: error: linker command failed with exit code 1 (use -v to see invocation)
[info] Bundling files:
[info]  - /Users/rouquett/git.leon/ScalaZ3/lib-bin/libscalaz3.dylib -> lib-bin/libscalaz3.dylib
[info]  - /Users/rouquett/git.leon/ScalaZ3/z3/4.3-osx-64b/lib/libz3.dylib -> lib-bin/libz3.dylib
[info]  - /Users/rouquett/git.leon/ScalaZ3/z3/4.3-osx-64b/lib/python2.7 -> lib-bin/python2.7
[info] Packaging /Users/rouquett/git.leon/ScalaZ3/target/scala-2.10/scalaz3_2.10-2.1.jar ...
[info] Done packaging.

我发现这里有一个用于MacOSX的Clang库：

http://brewformulas.org

然而，这可能需要调整一些构建脚本，以指向brew安装clang。

有没有人经历过类似的问题或解决过这些问题？

• 尼古拉斯。

Answer 1

下面是我在OSX上运行Leon的最新版本所遵循的步骤：

git clone git@github.com:epfl-lara/leon.git
cd leon
git remote add osx git@github.com:mantognini/leon.git
git fetch osx
git checkout osx
git rebase origin/master # adds precompiled OSX binaries
sbt clean compile script

确保将leon二进制文件链接到您的$PATH，例如，在最后一步运行ln -sv $(pwd)/leon /usr/local/bin/leon之后。

若要将二进制更新为Leon的最新版本，请运行

git fetch origin
git rebase origin/master
sbt clean compile script

假设您在osx分支上。