Windows build is missing import library

[vo1stv]

First, congrats on the good work. The latest version of master is easily built with Cygwin and sbt. It also compiles under Visual Studio with minor changes to casts.h and z3_Z3Wrapper.c. However it doesn't run. I suspect the reason is that it is missing the import library that tells the O/S to load libz3.dll.

In the past I used a separate fork to link this in. With things working so well using sbt, I'd prefer to use the official fork now.

It appears the necessary libz3.lib that needs to be linked with the Windows version can be generated from Cygwin using the command:

dlltool -D libz3.dll -d z3.def -l libz3.lib

The required input file z3.def may be available from Microsoft RISE z3, but if not, the Artemis project (https://github.com/cs-au-dk/Artemis) has a usable version in the contrib/Z3/dll folder.

So, please solve this issue by:

1. locating and adding the file z3.def to your branch;
2. adding the call dlltool -D libz3.dll -d z3.def -l libz3.lib to sbt; and
3. including libz3.lib when linking scalaz3.dll under Cygwin

[vo1stv]

I double-checked to see what happens if I use the scalaz3.dll compiled by sbt package within cygwin x64.

To make it clear, there are four build processes producing two build targets in this example. The build target scalaz3_2.10-2.1.jar is produced twice by sbt in cygwin x64. The first time I produce it using sbt package, the second time using sbt packageBin. In between the two builds, I create a custom version of scalaz3.dll. I use Microsoft Visual Studio Express for that.

The test application is built in Eclipse using the Scala 2.10 IDE for Eclipse

For my test, I am using Eclipse (Indigo and also Juno), and I created a simple Scala App to output Z3Wrapper.z3VersionString(). I created an Eclipse run configuration that sets the working folder to C:\Users...\AppData\Local\Temp\SCALAZ3_af47c38751cfc36953db3b71e8ff1ea\lib-bin. I also have my Eclipse build path configured to include C:\eclipse-jee-juno-SR2-win32-x86_64\eclipse\dropins\scalaz3_2.10-2.1.jar

First, I used the jar as built by sbt. Eclipse reports an Unsatisfied Link Error.

Next I created the libz3.lib import library for libz3.dll and (using Visual Studio Express) compiled the 64-bit build of the project found in my fork to create x64/Release/scalaz3.bin. I overwrote lib-bin/scalaz3.dll with this file and ran sbt packageBin.

This time when I run my scala App in Eclipse I have success.

Let me know if there is something I can do to avoid the extra steps.

[MikaelMayer]

Can you add in your simple app new Z3Context(); and tell me if it works? For me the line Z3Wrapper.z3VersionString(). works well, but when I try to do something non trivial it does not.

[vo1stv]

Good point.. my earlier test was testing z3.dll, not ScalaZ3.dll. In my fork, branch VS2012Express, I just updated a modified project directory that now includes a VS2012Express project called scalaz3Config. It creates and destroys a Z3Config using scalaZ3 calls.

I've editted Build.scala so it now generates the import library and links it with the DLL. The remaining problem seems to be that the cygwin gcc links the dll against cygwin1.dll which is not present outside of the Cygwin shell. Recompiling with Visual Studio links against native Windows libraries. I hear MinGW doesn't have that issue, but I haven't tried it.

[MikaelMayer]

Thank you for this remark. I am trying to compile z3 with visual studio 2013 for the first time, but I am currently unavailable to. It displays me this error message:

api/z3_replayer.obj : fatal error LNK1112: type d'ordinateur module 'x64' en con
flit avec le type d'ordinateur cible 'X86'
NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio 12.0
\VC\BIN\lib.EXE"' : return code '0x458'
Stop.

autoconf with MinGW does not work though.

[vo1stv]

In answer to your question, I've only tested the x64 version. Also, I'm not using the 2013 version, but in 2012 jargon, you need to open the "configuration manager" and add a new "platform". You must also make sure you use x86 tools when targeting a 32-bit Java VM; and likewise x64 tools when targetting the 64-bit Java VM.

Note well, however: your comment is a bit off topic. I do not recompile z3 under visual studio... in fact, I do not recompile z3.dll at all. That is unnecessary. Just follow the instructions as written in https://github.com/epfl-lara/ScalaZ3/blob/master/README.md regarding copying the binaries to your working copy of ScalaZ3.

I do use Visual Studio to recompile ScalaZ3.dll, but that consists of 4 c files (casts, extra, z3_thycallbacks, and z3_Z3Wrapper) and the import library libz3.lib. In earlier versions of z3, libz3.lib was distributed with z3 but not since 4.3.. This could be an oversight on the part of RISE. In any case it can be generated using dlltools and the .def file from Artemis.

[vo1stv]

The remaining problem is that the cygwin gcc links the dll against cygwin1.dll which is not present outside of the Cygwin shell. It may be possible to solve this by bundling cygwin1.dll inside the JAR, but that sounds too easy. I haven't been able to find any solution to this issue via Google except possibly compiling under another Linux shell (eg. MingW). It may be a week before I get to test that out. Any feedback in the meantime is appreciated.

[MikaelMayer]

We might a a fix for Windows 64 bits soon, using Visual Studio. We will keep you in touch.