Re: [isabelle] SAT solver problem



On 02/06/16 20:06, Jasmin Blanchette wrote:
>> So it seems that just for SAT4J and SAT4J_Light it working correctly but for the rest it not working properly!. 
> 
> SAT4J and SAT4J_Light do not rely on JNI, which is a technology for running binaries, which is always a risky undertaking. I suspect the issue is simply that you are using 64-bit Windows, and for all I know you might be the first user of Nitpick to do so. If you want to debug this further, I suggest we try a debugging session together (e.g. via Skype).

The Windows 64 version of Isabelle2016 uses a JDK for x86_64, but this
is also used for OS X and on most Linux installations. It is rare to see
x86 JDKs these days, but it can still happen.


In contrib/kodkod-1.5.2 (which is used for Isabelle2016), I see the
following JNI directories:

ppc-darwin/
x86-cygwin/
x86-darwin/
x86-linux/

Oddly, x86-darwin and x86-linux contain both x86 and x86_64 binaries,
but not x86-cygwin. The presence of ppc-darwin is a hint that the
general setup is somewhat outdated.

In recent years various Isabelle platform settings have emerged that
help to sort out this confusion. In particular, ISABELLE_JAVA_PLATFORM
says which Java platform is used for "isabelle java".


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.