How to build leon for MacOSX? -

i tried follow instructions build leon macosx (yosemite) readme.md file on github.

it worked except when run basic test, problem scalaz3 library not found:

 $ ./leon ./testcases/verification/sas2011-testcases/redblacktree.scala java.lang.unsatisfiedlinkerror: no scalaz3 in java.library.path     @ java.lang.classloader.loadlibrary(classloader.java:1865)     @ java.lang.runtime.loadlibrary0(runtime.java:870)     @ java.lang.system.loadlibrary(system.java:1122)     @ z3.z3wrapper.loadfromjar(z3wrapper.java:97)     @ z3.z3wrapper.<clinit>(z3wrapper.java:47)     @ z3.scala.z3config.<init>(z3config.scala:6)     @ leon.solvers.z3.fairz3solver.<init>(fairz3solver.scala:50)     @ leon.solvers.solverfactory$$anonfun$leon$solvers$solverfactory$$getsolver$1$1$$anon$1.<init>(solverfactory.scala:50)     @ leon.solvers.solverfactory$$anonfun$leon$solvers$solverfactory$$getsolver$1$1.apply(solverfactory.scala:50)     @ leon.solvers.solverfactory$$anonfun$leon$solvers$solverfactory$$getsolver$1$1.apply(solverfactory.scala:50)     @ leon.solvers.solverfactory$$anon$12.getnewsolver(solverfactory.scala:18)     @ leon.verification.analysisphase$.checkvc(analysisphase.scala:129)     @ leon.verification.analysisphase$$anonfun$10.apply(analysisphase.scala:111)     @ leon.verification.analysisphase$$anonfun$10.apply(analysisphase.scala:110)     @ scala.collection.traversablelike$withfilter$$anonfun$map$2.apply(traversablelike.scala:728)     @ scala.collection.immutable.list.foreach(list.scala:381)     @ scala.collection.traversablelike$withfilter.map(traversablelike.scala:727)     @ leon.verification.analysisphase$.checkvcs(analysisphase.scala:110)     @ leon.verification.analysisphase$.run(analysisphase.scala:45)     @ leon.verification.analysisphase$.run(analysisphase.scala:15)     @ leon.pipeline$$anon$1.run(pipeline.scala:12)     @ leon.pipeline$$anon$1.run(pipeline.scala:12)     @ leon.main$.execute(main.scala:236)     @ leon.main$.main(main.scala:220)     @ leon.main.main(main.scala)     @ sun.reflect.nativemethodaccessorimpl.invoke0(native method)     @ sun.reflect.nativemethodaccessorimpl.invoke(nativemethodaccessorimpl.java:62)     @ sun.reflect.delegatingmethodaccessorimpl.invoke(delegatingmethodaccessorimpl.java:43)     @ java.lang.reflect.method.invoke(method.java:497)     @ scala.reflect.internal.util.scalaclassloader$$anonfun$run$1.apply(scalaclassloader.scala:70)     @ scala.reflect.internal.util.scalaclassloader$class.ascontext(scalaclassloader.scala:31)     @ scala.reflect.internal.util.scalaclassloader$urlclassloader.ascontext(scalaclassloader.scala:101)     @ scala.reflect.internal.util.scalaclassloader$class.run(scalaclassloader.scala:70)     @ scala.reflect.internal.util.scalaclassloader$urlclassloader.run(scalaclassloader.scala:101)     @ scala.tools.nsc.commonrunner$class.run(objectrunner.scala:22)     @ scala.tools.nsc.objectrunner$.run(objectrunner.scala:39)     @ scala.tools.nsc.commonrunner$class.runandcatch(objectrunner.scala:29)     @ scala.tools.nsc.objectrunner$.runandcatch(objectrunner.scala:39)     @ scala.tools.nsc.maingenericrunner.runtarget$1(maingenericrunner.scala:65)     @ scala.tools.nsc.maingenericrunner.run$1(maingenericrunner.scala:87)     @ scala.tools.nsc.maingenericrunner.process(maingenericrunner.scala:98)     @ scala.tools.nsc.maingenericrunner$.main(maingenericrunner.scala:103)     @ scala.tools.nsc.maingenericrunner.main(maingenericrunner.scala) 

i tried build scalaz3 package epfl requires building microsoft's z3 (from github). building z3 works find building scalaz3 fails missing "gomp" library:

[error] ld: library not found -lgomp [error] clang: error: linker command failed exit code 1 (use -v 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. 

i found there clang omp library here macosx:

http://brewformulas.org

however, may require tweaking build scripts point brew's installation of clang-omp.

has experienced similar problems or solved them?

• nicolas.

these steps followed latest version of leon running on osx:

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 

make sure link leon binary $path, example after last step run ln -sv $(pwd)/leon /usr/local/bin/leon.

to update binary latest version of leon, run

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

assuming on osx branch.