Page MenuHomeIsabelle/Phabricator
Create Task
Maniphest T24

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

Description

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 https://isabelle.sketis.net/repos/kodkodi/rev/bc0a1d7d254b 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

Related Objects

Event Timeline

makarius closed this task as Resolved.Sep 28 2020, 12:21 PM
makarius reopened this task as Open.
makarius claimed this task.
makarius triaged this task as Normal priority.
makarius created this task.
makarius added a comment.Sep 28 2020, 12:28 PM

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

makarius added a project: isabelle-release.Oct 29 2020, 2:14 PM

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

makarius added a project: provers.Oct 29 2020, 5:19 PM
makarius moved this task from Backlog to TODO on the isabelle-release board.Dec 18 2020, 11:51 AM
makarius moved this task from TODO to Backlog on the isabelle-release board.
makarius added a comment.Jan 7 2021, 1:18 PM

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.
makarius added a comment.Oct 19 2021, 10:06 PM

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

makarius closed this task as Resolved.Oct 19 2021, 10:06 PM