在Scala 2.10中运行Scala^Z3

Question

我在我的Mac OSX（Mountain Lion，JDK 7，Scala 2.10，Z3 4.3）上成功安装了Scala^Z3（按照这个链接：http://lara.epfl.ch/w/ScalaZ3）。一切都进行得很顺利，但是我无法运行该网站上的任何示例（http://lara.epfl.ch/w/jniz3-scala-examples），因为会出现以下错误：

java.lang.NoClassDefFoundError: scala/reflect/ClassManifest
    at .<init>(<console>:8)
    at .<clinit>(<console>)
    at .<init>(<console>:7)
        ...
Caused by: java.lang.ClassNotFoundException: scala.reflect.ClassManifest
    at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
    at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
    at java.security.AccessController.doPrivileged(Native Method)
    at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
    ... 29 more

我认为这是由于Scala 2.9.x和2.10.x在处理反射方面的不兼容性导致的。因为我能够在Scala 2.9.x下运行相同的示例集。我的问题是，是否有办法在Scala 2.10下运行Scala^Z3？

- Amanj Sherwany

Answer 1

从查看项目属性和构建文件（https://github.com/psuter/ScalaZ3/blob/master/project/build.properties 和 https://github.com/psuter/ScalaZ3/blob/master/project/build/scalaZ3.scala）来看，我推断 scalaZ3 目前仅提供给 scala 2.9.2。目前没有跨版本支持。

你可以尝试获取代码并在“build.properties”文件中将版本更改为 scala 2.10.0 后自行编译它。 请参阅此页面以获取有关如何编译它的说明：https://github.com/psuter/ScalaZ3。 如果你很幸运，代码将按照 scala 2.10 的要求编译。如果不是，可能需要进行一些小修复。祝你好运。

如果你不急于使用，也可以麻烦 Scala^Z3 的作者，要求他们提供该库的 scala 2.10 版本。

- Régis Jean-Gilles

---

我不确定是否正确理解了。你所说的“Reflection API在编译时未被检测到”是什么意思？如果它“未被检测到”，那么它怎么能编译呢？你得到的异常确实指向一个问题：你正在运行针对Scala 2.9编译的代码，但是你正在使用Scala 2.10库运行此代码。你确定在运行sbt package之前更改了Scala版本吗？如果是这样，请确保你正在使用sbt package在“target”文件夹中生成的新的scalaz3.jar来运行测试（而不是旧的jar）。 - Régis Jean-Gilles

它在loadClass时失败，因此问题肯定是你正在使用的某些代码编译为Scala 2.9。反射API与此毫无关系的可能性极小。也许Scala^Z3依赖于某个使用2.9编译的库？ - Eugene Burmako

@Amanj Sherwany：同时，您可以尝试清理ivy缓存（换句话说，在您的主目录中删除“.ivy2”文件夹）吗？如果库的scala 2.9版本和scala 2.10版本具有相同的名称（没有通常的“_<scala-version>”后缀），那么ivy将为您提供旧版（scala 2.9）。清理缓存并在scalaZ3中重新运行“sbt package”应该可以解决问题。 - Régis Jean-Gilles

我可以确认Scala^Z3不使用反射（Java或Scala）。它所使用的是动态加载本地库（好老的Java System.loadLibrary）。我不明白为什么这会成为2.10的问题。虽然我们自己还没有在2.10中使用过它，但我们将感激您提供的任何见解。 - Philippe

@Philippe 如果你是 Scala^Z3 的开发者/贡献者之一，这里有一个我提交的关于这个问题的 bug：https://github.com/psuter/ScalaZ3/issues/23 - Amanj Sherwany

Answer 2

我将从我的回复中复制指令，与您的 GitHub问题 有关，这可能有助于未来的某个人。

目前的情况是，旧的sbt项目似乎无法与Scala 2.10混合使用。以下是Linux“手动”编译该项目的说明。这对我来说适用于Z3 4.3（从Z3 git repo获取）和Scala 2.10。按照原始说明安装Z3后：

首先编译Java文件：

$ mkdir bin
$ find src/main -name '*.java' -exec javac -d bin {} +

然后编译C文件。为此，您需要首先生成JNI标头，然后编译共享库。以下命令中的选项适用于Linux。要找到JNI标头所在的位置，我在Scala控制台中运行(new java.io.File(System.getProperty("java.home")).getParent（并将/include添加到结果中）。

$ javah -classpath bin -d src/c z3.Z3Wrapper
$ gcc -o lib-bin/libscalaz3.so -shared -Wl,-soname,libscalaz3.so \
        -I/usr/lib/jvm/java-6-sun-1.6.0.26/include \
        -I/usr/lib/jvm/java-6-sun-1.6.0.26/include/linux \
        -Iz3/4.3/include -Lz3/4.3/lib \
        -g -lc -Wl,--no-as-needed -Wl,--copy-dt-needed -lz3 -fPIC -O2 -fopenmp \
        src/c/*.[ch]

现在编译Scala文件：

$ find src/main -name '*.scala' -exec scalac -classpath bin -d bin {} +

你会收到“特性警告”，这在升级到2.10时很常见，并且会收到有关非穷尽模式匹配的另一个警告。

现在让我们将所有内容制作成一个jar文件...

$ cd bin
$ jar cvf scalaz3.jar z3
$ cd ..
$ jar uf bin/scalaz3.jar lib-bin/libscalaz3.so

现在你应该有一个bin/scalaz3.jar，其中包含你所需的一切。让我们试一下：

$ export LD_LIBRARY_PATH=z3/4.3/lib
$ scala -cp bin/scalaz3.jar
scala> z3.scala.version

希望这有所帮助！

- Philippe

---

Java的分离编译对我不起作用。构建时出现有关z3.scala包中某些类的引用错误（该包尚未构建）的错误。您为什么要延迟Scala编译步骤呢？此外，必须手动生成LibraryChecksum.java文件。 - dips

Answer 3

这并不是直接回答问题，但可能有助于其他试图使用Scala 2.10构建scalaz3的人。我在Windows 7上使用Scala 2.10.1和Z3 4.3.0构建了ScalaZ3，并在http://lara.epfl.ch/w/jniz3-scala-examples中测试了它的整数约束示例，一切正常。

构建Z3：

Codeplex上的Z3 4.3.0下载不包括libZ3.lib文件。因此，我不得不在我的机器上下载源代码并进行构建。构建过程非常简单。

构建ScalaZ3：

目前，build.properties中的sbt版本为0.7.4，scala版本为2.9.2。这个版本可以成功构建。（我不得不对build.scala文件进行一些小修改。在gcc任务中，将z3LibPath（z3VN）.absolutePath修改为z3LibPath（z3VN）.absolutePath + "\\libz3.lib"。）

现在，如果我在build.properties中将scala版本更改为2.10.1，则在启动sbt时会出现"Error compiling sbt component 'compiler-interface'"错误。我不知道为什么会出现这种情况。

我将sbt版本更改为0.12.2，scala版本更改为2.10.1，并从新的源代码开始。我还在项目根文件夹中添加了build.sbt，其中包含scalaVersion：=“2.10.1”。这是必需的，因为在sbt 0.12.2中，文件build.properties仅用于指定sbt版本。有关sbt版本差异的更多信息，请参见（https://github.com/harrah/xsbt/wiki/Migrating-from-SBT-0.7.x-to-0.10.x）。

我遇到了错误Z3Wrapper.java:27: cannot find symbol LibraryChecksum。这是因为文件LibraryChecksum.java没有被生成，而该文件应该由构建文件(project\build\build.scala)生成。看起来package任务没有执行(project\build\build.scala)中的任务。任务compute-checksum、javah和gcc没有被执行。这可能是因为sbt 0.12.2期望build.scala文件直接位于project文件夹下面。

然后我复制了上一次构建生成的LibraryChecksum.java文件，然后构建成功了。生成的jar文件不包含scalaz3.dll。

我随后手动执行了javah和gcc任务。这些任务的命令可以从成功构建scala 2.9.2的日志中复制（我对scala 2.10.1的命令进行了相应修改）。同样，在这里，我不得不做一些更改。我必须在javah任务的类路径中显式添加scala-library.jar的完整路径。

接着，我使用jar uf target\scala-2.10\scalaz3.jar lib-bin/scalaz3.dll将lib-bin\scalaz3.dll添加到jar文件中。

- dips

---

请注意，由于Etienne Kneuss的贡献，ScalaZ3现已移植到2.10版本。 - Philippe

@Philippe 谢谢。我会在有时间测试这个版本的时候分享我在Windows平台上的发现。 - dips