Scala^Z3 on Scala 2.10 - Githubissues

amanjpro commented 11 years ago

Hello guys,

I think there is a bug in the ScalaZ3 library on Scala 2.10. For example running the follwoing example in the interpreter will lead to an exception.

z3.scala.version

The exception which is thrown is related to Java Reflection (I think)

java.lang.NoClassDefFoundError: scala/reflect/ClassManifest
    at .(:8)
    at .()
    at .(:7)
    at .()
    at $print()
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:601)
    at scala.tools.nsc.interpreter.IMain$ReadEvalPrint.call(IMain.scala:731)
    at scala.tools.nsc.interpreter.IMain$Request.loadAndRun(IMain.scala:980)
    at scala.tools.nsc.interpreter.IMain.loadAndRunReq$1(IMain.scala:570)
    at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:601)
    at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:565)
    at scala.tools.nsc.interpreter.ILoop.reallyInterpret$1(ILoop.scala:745)
    at scala.tools.nsc.interpreter.ILoop.interpretStartingWith(ILoop.scala:790)
    at scala.tools.nsc.interpreter.ILoop.command(ILoop.scala:702)
    at scala.tools.nsc.interpreter.ILoop.processLine$1(ILoop.scala:566)
    at scala.tools.nsc.interpreter.ILoop.innerLoop$1(ILoop.scala:573)
    at scala.tools.nsc.interpreter.ILoop.loop(ILoop.scala:576)
    at scala.tools.nsc.interpreter.ILoop$$anonfun$process$1.apply$mcZ$sp(ILoop.scala:867)
    at scala.tools.nsc.interpreter.ILoop$$anonfun$process$1.apply(ILoop.scala:822)
    at scala.tools.nsc.interpreter.ILoop$$anonfun$process$1.apply(ILoop.scala:822)
    at scala.tools.nsc.util.ScalaClassLoader$.savingContextLoader(ScalaClassLoader.scala:135)
    at scala.tools.nsc.interpreter.ILoop.process(ILoop.scala:822)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:83)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:96)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:105)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)
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

But when I run the same example with Scala 2.9 I will get this expected result: res0: String = Z3 4.3 (build 1, rev. 0), ScalaZ3 4.0.a (in dev.)

How to reproduce the bug

In Mac OSX (Mountain Lion) -and probably other OSes too-
Install JDK 7, Scala 2.10 and Z3 4.3 (I couldn't find version 3.2 of the solver)
Install Scala^Z3 as mentioned in this webpage (http://lara.epfl.ch/w/ScalaZ3)
Open the terminal, and write this: ``` LD_LIBRARY_PATH=${Z3_LIB_PATH} scala -classpath scalaz3.jar ``` Where ${Z3_LIB_PATH} is the path to Z3 lib and scalaz3.jar is the path to the scala^z3 jar
Run this into your REPL: ``` scala z3.scala.version ```

psuter commented 11 years ago

How did you compile Scala^Z3? Using sbt and the online instructions? sbt uses its own, local, copy of Scala, and the version it uses is determined by what's inside build.sbt. If you have compiled the library using the default configuration and are trying to use it from Scala 2.10, it will not work. Scala is not backwards binary compatible.

amanjpro commented 11 years ago

Hello,

I modified my build.properties script to this:

#Project properties
#Tue Mar 05 15:54:31 CET 2013
project.organization=EPFL/LARA
project.name=ScalaZ3
sbt.version=0.12.2
project.version=4.0a
build.scala.versions=2.10.0
project.initialize=false

and I guess this should tell the compiler that it should use scala 2.10. But I got no success still! (I even removed my .ivy2 folder before I compile it!)

rjean-gilles commented 11 years ago

Sorry to point the obvious, but after compiling in scala 2.10, did you copy the new jar (that should now be in your "target" folder) over the old one? Apparently you are running your tests in a standalone scala console, and explictly setting the classpath to point to a scala^Z3 jar. So you have to make sure that the scala^z3 jar that you specify in the classpath is indeed the new one that you have yourrself recompiled with scala 2.10.

amanjpro commented 11 years ago

@rjean-gilles I am sure that I am using the one that I myself compiled (actually I have removed all the old versions).

Have anyone else (other than me) tried to run/compile it under 2.10?

rjean-gilles commented 11 years ago

I could not manage to compile it. I'm under windows, and on windows the compiling process is not as simpl as sbt package. It turns out I had an access violation with LD, and stopped trying after that.

Another last obvious one: you did switch to a scala 2.10 console, right? If you're still using a scala 2.9 console things will get awry. If you are, I guess I will just let @psuter investigate further. Good luck.

psuter commented 11 years ago

I just tried to modify build.properties as you did, and it won't compile here. I suspect the rather old sbt 0.7.4 does not play nice with Scala 2.10. I'll try later to port the compilation script to a more recent version of sbt and see what happens.

Unless you want to repeatedly change the library, you may be better off with a manual compilation at this point, using javac, javah, gcc and the desired version of scalac. Sorry for the trouble.

amanjpro commented 11 years ago

@rjean-gilles Do you mean if I use scala 2.10 REPL instead of 2.9? Yeah, I use scala 2.10

@psuter I couldn't compile it under 2.10 either until I changed the sbt version in the build properties to (0.12.2). BTW, I didn't get what you mean by this:

Unless you want to repeatedly change the library, you may be better off with a manual 
compilation at this point, using javac, javah, gcc and the desired version of scalac.

Thanks in advance!

psuter commented 11 years ago

I just meant to say that if you just plan to use the lib, as oppose to develop/contribute to it, then you may want to try to compile it "by hand", bypassing sbt completely, as you would only need to do it once.

You can try the following steps (after installing Z3 per the original instructions).

First compile the Java files:

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

Then compile the C files. For this, you need to generate the JNI headers first, then compile the shared library. The options in the commands below are for Linux. To find our where the JNI headers are, I run (new java.io.File(System.getProperty("java.home")).getParent in a Scala console (and add /include to the result).

$ 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]

Now compile the Scala files:

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

You'll get "feature warnings", which is typical when moving to 2.10, and another warning about a non-exhaustive pattern match.

Now let's make a jar file out of everything...

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

...and now you should have bin/scalaz3.jar containing everything you need. Let's try it out:

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

Hope this helps!

koksal commented 11 years ago

Hi everyone,

If this is still an issue, I managed to package the library with Z3 4.3.2, Scala 2.10 and sbt 0.12.0 by adding a (very simplistic) build definition build.sbt to the top-level folder, with the following definition:

scalaVersion := "2.10.0"

Hope this helps.

colder commented 11 years ago

I've just pushed changes on the master branch that should enable support for Scala 2.10.2. The SBT definition has been upgraded to 0.12.2 with all the packaging magic.

Users of Scala 2.9.x should checkout the 2.9.x branch.

epfl-lara / ScalaZ3

Scala^Z3 on Scala 2.10 #23