Bundle libz3 within scalaz3.jar

The loading of the libz3 is now deterministic, no more LD_LIBRARY_PATH
needed. libscalaz3/libz3 are always expected to be extracted to
<tmp>/SCALAZ3_<checksum>.

Works on linux and mac, compiles on windows but errors when running.

Author: colder

README.md

@@ -4,82 +4,53 @@ ScalaZ3 for Scala 2.10
 This is ScalaZ3 for Scala 2.10 and Z3 4.3. Switch to the branch '2.9.x' for
 Scala 2.9 support.
 
-
-Downloading Z3
-=================
-
-Z3 can be downloaded from the [Z3 download site](http://z3.codeplex.com/)
-
-
 Compiling ScalaZ3
 =================
 
-Setup steps, for Linux
+Prerequisites
 ----------------------
+You should have Java and SBT 0.13.x installed.
 
-1) Download Z3, and copy the include and lib files to z3/[z3version]/include and
-z3/[z3version]/lib respectively. (eg: z3/4.3-unix-64b/include/z3.h and
-z3/4.3-unix-64b/lib/libz3.so).
-
-2) Download sbt 0.12.x.
-
-3) Run 'sbt package' to create the jar file. It will be in
-target/[scalaversion]/scalaz3....jar and will contain the shared
-library required by the bindings.
-
-4) For testing, run
-
-    LD_LIBRARY_PATH=z3/[z3version]/lib sbt test
-
-Alternatively, start a console by running
-
-    LD_LIBRARY_PATH=z3/[z3version]/lib scala -cp target/[scalaversion]scalaz3.jar
-
-then try, e.g.,
-
-    println(z3.scala.version).
-
-Setup steps, for Mac
+Linux
 ----------------------
 
-1) Download Z3, and copy the include and lib files to z3/[z3version]/include and
-z3/[z3version]/lib respectively. (eg: z3/4.3-osx-64b/include/z3.h and
-z3/4.3-osx-64b/lib/libz3.so).
-
-2) Download sbt 0.12.x.
-
-3) Run 'sbt package' to create the jar file. It will be in
-target/[scalaversion]/scalaz3....jar and will contain the shared
-library required by the bindings.
-
-4) For testing, run
+1) Download Z3 source code from http://z3.codeplex.com/, compile it, and copy
+the headers and built library to z3/[z3version]/include and z3/[z3version]/lib
+respectively. (eg: z3/4.3-unix-64b/include/z3.h and
+z3/4.3-unix-64b/lib/libz3.so).
 
-    DYLD_LIBRARY_PATH=z3/[z3version]/lib sbt test
+2) Run 'sbt package' to create the jar file. It will be in
+'target/scala-2.10/scalaz3\_2.10-2.0.jar' and will contain the shared library
+dependencies.
 
-Alternatively, start a console by running
+3) For testing, run
 
-    DYLD_LIBRARY_PATH=z3/[z3version]/lib scala -cp target/[scalaversion]scalaz3.jar
+    sbt test
 
-then try, e.g.,
+Mac
+----------------------
 
-    println(z3.scala.version).
+1) Download Z3 source code from http://z3.codeplex.com/, compile it, and copy
+the headers and built library to z3/[z3version]/include and z3/[z3version]/lib
+respectively. (eg: z3/4.3-unix-64b/include/z3.h and
+z3/4.3-unix-64b/lib/libz3.dnylib).
 
-Setup steps, for Windows
-------------------------
+2) Run 'sbt package' to create the jar file. It will be in
+'target/scala-2.10/scalaz3\_2.10-2.0.jar' and will contain the shared library
+dependencies.
 
-A) Download and install Z3 using the .msi installer
+3) For testing, run
 
-B) Download sbt (see 2 above).
+    sbt test
 
-C) The 'package' command in the current build script does not work with
-Windows; there is no equivalent for the gcc command. Run 'javah' so that it
-compiles the Java/Scala sources and generates the JNI header files.
+Windows
+----------------------
 
-D) Assuming you have copied the 'include' and 'bin' directories from the Z3
-distribution in z3/[z3version], the following command should compile the shared
-library, assuming you have installed MinGW:
+1) Download Cygwin, and install packages for gcc.
 
-    gcc -shared -o lib-bin\scalaz3.dll -D_JNI_IMPLEMENTATION_ -Wl,--kill-at -I "[jdkpath]\include" -I "[jdkpath]\include\win32" -I z3\[z3version]\include src\c\*.h src\c\*.c z3\[z3version]\bin\z3.lib
+2) Download Z3 4.3 release, and copy libz3.dll to z3/[z3version]/bin and
+include/\*.h to /z3/[z3version]/include/. (eg: z3/4.3-win-64b/bin/libz3.dll)
 
-E) You can manually create a jar with the contents of target/[scalaversion] and
-lib-bin.
+3) Run 'sbt package' to create the jar file. It will end up in
+'target/scala2.10/scalaz3\_2.10-2.0.jar' and will contain the shared library
+dependencies.

project/Build.scala

@@ -5,10 +5,17 @@ object ScalaZ3build extends Build {
 
   val natives = List("z3.Z3Wrapper")
 
+  lazy val PS               = java.io.File.pathSeparator
+  lazy val DS               = java.io.File.separator
+
   lazy val cPath            = file("src") / "c"
   lazy val cFiles           = file("src") / "c" * "*.c"
   lazy val soName           = System.mapLibraryName("scalaz3")
+
+  lazy val z3Name     = if (isMac) "libz3.dylib" else if(isWindows) "libz3.dll" else System.mapLibraryName("z3")
+
   lazy val libBinPath       = file("lib-bin")
+  lazy val z3BinFilePath    = z3LibPath / z3Name
   lazy val libBinFilePath   = libBinPath / soName
   lazy val jdkIncludePath   = file(System.getProperty("java.home")) / ".." / "include"
   lazy val jdkUnixIncludePath = jdkIncludePath / "linux"
@@ -54,7 +61,7 @@ object ScalaZ3build extends Build {
 
   val javahKey    = TaskKey[Unit]("javah", "Prepares the JNI headers")
   val gccKey      = TaskKey[Unit]("gcc", "Compiles the C sources")
-  val checksumKey = TaskKey[Unit]("checksum", "Generates checksum file.")
+  val checksumKey = TaskKey[String]("checksum", "Generates checksum file.")
 
   val checksumTask = (streams, sourceDirectory in Compile) map {
     case (s, sd) =>
@@ -97,25 +104,31 @@ object ScalaZ3build extends Build {
       fw.close
 
       s.log.info("Wrote checksum " + md5String + " as part of " + checksumFilePath.asFile + ".")
+
+      md5String
   }
 
 
   val javahTask = (streams, dependencyClasspath in Compile, classDirectory in Compile) map {
     case (s, deps, cd) =>
 
-      deps.map(_.data.absolutePath).find(_.endsWith("lib/scala-library.jar")) match {
+      deps.map(_.data.absolutePath).find(_.endsWith("lib" + DS + "scala-library.jar")) match {
         case Some(lib) =>
           s.log.info("Preparing JNI headers...")
-          exec("javah -classpath " + cd.absolutePath + ":"+lib+" -d " + cPath.absolutePath + " " + natives.mkString(" "), s)
+          exec("javah -classpath " + cd.absolutePath + PS + lib + " -d " + cPath.absolutePath + " " + natives.mkString(" "), s)
 
         case None =>
           s.log.error("Scala library not found in dependencies ?!?")
 
       }
   } dependsOn(compile.in(Compile))
 
+  def extractDir(checksum: String): String = {
+    System.getProperty("java.io.tmpdir") + DS + "SCALAZ3_" + checksum + DS + "lib-bin" + DS   
+  }
+
 
-  val gccTask = (streams) map { case (s) =>
+  val gccTask = (streams, checksumKey) map { case (s, cs) =>
     s.log.info("Compiling C sources ...")
 
     // First, we look for z3
@@ -131,17 +144,20 @@ object ScalaZ3build extends Build {
              "-I" + jdkUnixIncludePath.absolutePath + " " +
              "-I" + z3IncludePath.absolutePath + " " +
              "-L" + z3LibPath.absolutePath + " " +
-             "-g -lc -Wl,--no-as-needed -Wl,--copy-dt-needed -lz3 -fPIC -O2 -fopenmp " +
+             "-g -lc " +
+             "-Wl,-rpath,"+extractDir(cs)+" -Wl,--no-as-needed -Wl,--copy-dt-needed " +
+             "-lz3 -fPIC -O2 -fopenmp " +
              cFiles.getPaths.mkString(" "), s)
 
       } else if (isWindows) {
         exec("gcc -shared -o " + libBinFilePath.absolutePath + " " +
              "-D_JNI_IMPLEMENTATION_ -Wl,--kill-at " +
-             "-I " + "\"" + jdkIncludePath.absolutePath + "\"" + " " +
-             "-I " + "\"" + jdkWinIncludePath.absolutePath + "\"" + " " +
-             "-I " + z3IncludePath.absolutePath + " " +
-             cFiles.getPaths.mkString(" ") + " " +
-             z3LibPath.absolutePath, s)
+             "-D__int64=\"long long\" " +
+             "-I " + "\"" + jdkIncludePath.absolutePath + "\" " +
+             "-I " + "\"" + jdkWinIncludePath.absolutePath + "\" " +
+             "-I " + "\"" + z3IncludePath.absolutePath + "\" " +
+             cFiles.getPaths.mkString(" ") +
+             " " + z3BinFilePath.absolutePath + "\" ", s)
       } else if (isMac) {
         val frameworkPath = "/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers"
 
@@ -151,7 +167,9 @@ object ScalaZ3build extends Build {
              "-I" + frameworkPath + " " +
              "-I" + z3IncludePath.absolutePath + " " +
              "-L" + z3LibPath.absolutePath + " " +
-             "-g -lc -lz3 -fPIC -O2 -fopenmp " +
+             "-g -lc " +
+             "-Wl,-rpath,"+extractDir(cs)+" " +
+             "-lz3 -fPIC -O2 -fopenmp " +
              cFiles.getPaths.mkString(" "), s)
       } else {
         s.log.error("Unknown arch: "+osInf+" - "+osArch)
@@ -161,9 +179,25 @@ object ScalaZ3build extends Build {
 
   val packageTask = (Keys.`package` in Compile).dependsOn(javahKey, gccKey)
 
-  val newMappingsTask = mappings in (Compile, packageBin) <<= (mappings in (Compile, packageBin)) map {
-    case maps =>
-      (libBinFilePath.getAbsoluteFile -> ("lib-bin/"+soName)) +: maps
+  val newMappingsTask = mappings in (Compile, packageBin) <<= (mappings in (Compile, packageBin), streams) map {
+    case (normalFiles, s) =>
+      val newFiles = 
+        (libBinFilePath.getAbsoluteFile -> ("lib-bin/"+libBinFilePath.getName)) ::
+        (z3LibPath.listFiles.toList.map { f =>
+	  f.getAbsoluteFile -> ("lib-bin/"+f.getName)
+        })
+
+      s.log.info("Bundling files:")
+      for ((from, to) <- newFiles) {
+	  s.log.info(" - "+from+" -> "+to)
+      }
+
+      newFiles ++ normalFiles
+  }
+
+  val newTestClassPath = internalDependencyClasspath in (Test) <<= (artifactPath in (Compile, packageBin)) map {
+    case jar =>
+      List(Attributed.blank(jar))
   }
 
   lazy val root = Project(id = "ScalaZ3",
@@ -174,6 +208,7 @@ object ScalaZ3build extends Build {
                             javahKey <<= javahTask,
                             compile.in(Compile) <<= compile.in(Compile).dependsOn(checksumTask),
                             Keys.`package`.in(Compile) <<= packageTask,
+                            newTestClassPath,
                             newMappingsTask
                           )
                      )

project/build.properties

@@ -1 +1 @@
-sbt.version=0.12.2
+sbt.version=0.13.0