Page MenuHomeIsabelle/Phabricator

Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon)
Closed, ResolvedPublic


In the past there used to be a 32bit Windows DLL for nitpick/kodkod, but it was dysfunctional on current 64bit Windows and merely fooled nitpick in accepting it as installed solver. After this causes an explicit error, e.g. in Isabelle/8162ca81ea8a:

The SAT solver "MiniSat_JNI" is not configured. The following solvers are configured:
"SAT4J", "SAT4J_Light"
At command "nitpick" (line 1264 of "~~/src/HOL/Nitpick_Examples/Refute_Nits.thy")

There are the following possibilities to resolve this:

  1. fool nitpick again by including a dummy minisat.dll (empty file)
  2. find minisat.dll for x86_64-windows and include it in the kodkodi component
  3. change the check by nitpick to be more tolerant, e.g. warning instead of error

Event Timeline

makarius reopened this task as Open.
makarius claimed this task.
makarius triaged this task as Normal priority.
makarius created this task.

I have scavenged the Net twice for a 64bit minsat.dll, but failed so far.

It would be great to know more for the forthcoming Isabelle2021 release, although this is not mission critial for it.

makarius moved this task from TODO to Backlog on the isabelle-release board.

Also missing: arm64-linux, arm64-darwin (relavant for native JDK on macOS).

makarius renamed this task from Missing minisat.dll for nitpick/kodkod on Windows to Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon).Jan 7 2021, 1:37 PM
makarius removed a subscriber: makarius.

See also Isabelle/74a36aae067a and Isabelle/2d089ff0e03b --- minisat is provided as external executable on all platforms.