Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Yices2 windows support #215

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

Yices2 windows support #215

wants to merge 15 commits into from

Conversation

baierd
Copy link
Collaborator

@baierd baierd commented Feb 3, 2021

This PR covers the Windows support for Yices2.

The JNI-wrapper was changed to conform to Windows pointer standards.
A bash script is provided that explains how to build Yices2 for Windows and then compiles and links the wrapper to it.
Note: Yices2 only provides explanations as to how to build it inside Windows with Cygwin + Mingw.
I don't know if it is possible to simply skip Cygwin and compile it with Mingw on a Unix system, do you know more about that @kfriedberger ?

The Yices2 Windows components are the following:
-libyices.dll
-libyices2j.dll
-libgmp-10.dll

TODO:
This needs to be tested on a Windows environment that does NOT have libgmp-10.dll installed in any way!

@baierd
Copy link
Collaborator Author

baierd commented Feb 3, 2021

I have just tested it on a new Windows environment and it works without any issues.

@kfriedberger
Copy link
Member

For MathSAT we use an existing DLL from the original development team and then MinGW on Linux to build the bindings for Windows.
As Yices also provides the DLL as part of their release, it should be doable, to build everything on Linux.
This would simplify further development, because we would only need to test on Windows and not develop there :-)

@baierd
Copy link
Collaborator Author

baierd commented Feb 3, 2021

We have to provide the GMP library additionally, but yes that should simplify it immensely.
I will check the script against the provided dll and report back.

@kfriedberger
Copy link
Member

GMP can be build with MinGW on Linux. I have already done that for MathSAT. That's easy.

@kfriedberger
Copy link
Member

Are you sure about GMP? The Windows-version is called MPIR.
The docu can be found in the script for compiling MathSAT for Windows.

@baierd
Copy link
Collaborator Author

baierd commented Feb 3, 2021

GMP is statically linked in the provided Yices2 Windows binary, so that solves that.
But we would still need it when compiling the wrapper, as it is a needed dependency in the macros.

It would most likely suffice to compile it on Linux, i can test it.

@baierd
Copy link
Collaborator Author

baierd commented Feb 4, 2021

I've tested the prebuilt dll and it does not load and i don't know why.
I will investigate further.

@baierd
Copy link
Collaborator Author

baierd commented Feb 14, 2021

Update:
The precompiled binary needs 3 additional dependencies: libwinpthread-1.dll, libstdc++-6.dll and libgcc_s_seh-1.dll.
I tried simply statically link these, but there are 2 problems and i could only solve one.

The linker can't know what is used by yices, only our wrapper, so it only statically adds the wrapper parts. Of course the needed yices components are missing then. This could be solved by using the --whole-archive flag.

Winpthread is needed but the linker won't link it when threads are not used. This is solved by the --whole-archive flag.

A problem arises when using the mentioned flag on all libraries, as mutex is defined in winpthread and stdc++, therefore it can't link all 3, just 2. (gcc is always fine, but just one of the others)

Ideas:
-Either simply provide i.e. libstdc++-6.dll as an additional dependency.
-Switch from the pre-compiled yices binary to compile it ourselfs and statically link the libs there.

@kfriedberger
Copy link
Member

We already use (and used) our own version of Yices for Linux, based on some Git revision of their repository.
So, we might stay with always compiling Yices directly.
It would be optimal, if we can build everything on Linux, using GCC and MinGW directly.

@baierd
Copy link
Collaborator Author

baierd commented Feb 14, 2021

I don't know if that is possible for Windows. The Yices2 devs only provide build documentation for Cygwin + Mingw (and Cygwin alone). I can test it and take a look at the build script.
On Windows its a little different from Linux as Yices2 needs the static + shared GMP libary, but Windows does not allow the shared and static GMP lib to be installed at the same time and location. Yices needs the shared headers for shared and static build to package the binary with it. That is not really a problem, but a little annoying. However, i have a documentation of how to do it on Windows.
I'm gona test compiling Yices2 threadsafe from source with the static dependencies on Windows first, if that is working, i'll try on Linux.
As far as i have seen and tested, the build documentation for Windows is at least 7-8 years old, maybe i can ask the devs for an updated version.

@kfriedberger kfriedberger mentioned this pull request Feb 15, 2021
3 tasks
@baierd
Copy link
Collaborator Author

baierd commented Apr 7, 2021

I tested building the Yices2 version on Linux, however the config does not seem to work for that purpose.
I might need to ask the Yices2 devs for help here as there are options in the config for exactly this purpose.

But i updated to build information for Cygwin + Mingw and the script that builds the wrapper in Cygwin.
This results in 2 dll's: libyices.dll and libyices2j.dll
They work fine on my Windows machine as well as an fresh VM i tested.

The only issue with them is that multithreading is not supported as i get an error when trying to compile with it.
This might however be a wrong error as i checked what it is doing (simply a mini config that is executed).
But as multithreading for Yices2 is not supported on Unix at the moment i didn't spend much time on it.

If we were to use the prebuild Yices2 this issue would be resolved. But the script would have to be extended a little. I put instructions and possible hints if it fails into the script as i tested this with the old prebuild binaries.

Would you like me to continue this until multithreading is supported?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

Successfully merging this pull request may close these issues.

2 participants