Email Gateway (Aug 22 2022 at 13:27): Email Gateway (Aug 22 2022 at 13:27):From: Omar Jasim <oajasim1@sheffield.ac.uk>
Dear list,
I have problem with using nitpick even for trivial lemma such as: lemma "P
⟷ Q ".
in the output panel, I've got this kodkod warning:
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
I'm using Isabelle 2016 64-bit windows version. Any suggestion?
Cheers
Omar
Email Gateway (Aug 22 2022 at 13:30):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Omar,
This seems to be a low-level issue. There are hard to debug; let's see if there's a workaround first.
In the Nitpick documentation (isabelle doc nitpick), there's a list of SAT solvers that can be tried. You can choose one by setting
nitpick_params [sat_solver = <name_of_solver>]
Could you try e.g. MiniSat as the solver and see if the issue goes away?
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 13:30):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Omar,
This seems to be a low-level issue. There are hard to debug; let's see if there's a workaround first.
In the Nitpick documentation (isabelle doc nitpick), there's a list of SAT solvers that can be tried. You can choose one by setting
nitpick_params [sat_solver = <name_of_solver>]
Could you try e.g. MiniSat as the solver and see if the issue goes away?
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 13:30):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Omar,
First, sorry for the duplicate email. My email client seems to be confused due to all the wifi connections/disconnections.
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). Please let me know privately and we can set a time.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 13:31):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 13:31):From: Makarius <makarius@sketis.net>
Making kodkod work on x86_64-windows is important in its own right.
But just for immediate use, you can downgrade to the 32-bit Windows
version of Isabelle2016 instead.
The main difference is the JDK, and its maximum heap resources. 32-bit
should be fine for medium-sized applications.
Makarius
Last updated: Apr 23 2024 at 12:29 UTC