--- a/Admin/components/components.sha1 Thu Oct 07 16:28:17 2021 +0200
+++ b/Admin/components/components.sha1 Thu Oct 07 21:43:26 2021 +0200
@@ -253,6 +253,7 @@
3ecdade953bb455ed2907952be287d7e5cf6533b kodkodi-1.5.5.tar.gz
8aa939f5127290eb9a99952d375be9ffbf90c43b kodkodi-1.5.6-1.tar.gz
6b12bf3f40b16fae8ff22aa39171fa018d107cb3 kodkodi-1.5.6.tar.gz
+c8b2e632f3ab959a4e037833a45e6360c8b72a99 kodkodi-1.5.7.tar.gz
377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz
1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.tar.gz
@@ -260,6 +261,7 @@
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz
3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz
+ae76bfaade3bf72ff6b2d3aafcd52fa45609fcd1 minisat-2.2.1.tar.gz
eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz
--- a/Admin/components/main Thu Oct 07 16:28:17 2021 +0200
+++ b/Admin/components/main Thu Oct 07 21:43:26 2021 +0200
@@ -13,7 +13,8 @@
jedit-20210802
jfreechart-1.5.3
jortho-1.0-2
-kodkodi-1.5.6-1
+kodkodi-1.5.7
+minisat-2.2.1
nunchaku-0.5
opam-2.0.7
polyml-5.8.2
--- a/etc/build.props Thu Oct 07 16:28:17 2021 +0200
+++ b/etc/build.props Thu Oct 07 21:43:26 2021 +0200
@@ -21,6 +21,7 @@
src/Pure/Admin/build_jdk.scala \
src/Pure/Admin/build_jedit.scala \
src/Pure/Admin/build_log.scala \
+ src/Pure/Admin/build_minisat.scala \
src/Pure/Admin/build_polyml.scala \
src/Pure/Admin/build_release.scala \
src/Pure/Admin/build_spass.scala \
--- a/src/Doc/Nitpick/document/root.tex Thu Oct 07 16:28:17 2021 +0200
+++ b/src/Doc/Nitpick/document/root.tex Thu Oct 07 21:43:26 2021 +0200
@@ -2196,9 +2196,6 @@
the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
\texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
executable.%
-\footnote{Important note for Cygwin users: The path must be specified using
-native Windows syntax. Make sure to escape backslashes properly.%
-\label{cygwin-paths}}
The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
\url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
Nitpick has been tested with version 2.51.
@@ -2212,7 +2209,6 @@
written in \cpp{}. To use MiniSat, set the environment variable
\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
executable.%
-\footref{cygwin-paths}
The \cpp{} sources and executables for MiniSat are available at
\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
and 2.2.
@@ -2226,7 +2222,6 @@
\item[\labelitemi] \textbf{\textit{Riss3g}:} Riss3g is an efficient solver written in
\cpp{}. To use Riss3g, set the environment variable \texttt{RISS3G\_HOME} to the
directory that contains the \texttt{riss3g} executable.%
-\footref{cygwin-paths}
The \cpp{} sources for Riss3g are available at
\url{http://tools.computational-logic.org/content/riss3g.php}.
Nitpick has been tested with the SAT Competition 2013 version.
@@ -2234,7 +2229,6 @@
\item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written
in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
the directory that contains the \texttt{zchaff} executable.%
-\footref{cygwin-paths}
The \cpp{} sources and executables for zChaff are available at
\url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
versions 2004-05-13, 2004-11-15, and 2007-03-12.
@@ -2242,7 +2236,6 @@
\item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver written in
\cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
directory that contains the \texttt{rsat} executable.%
-\footref{cygwin-paths}
The \cpp{} sources for RSat are available at
\url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
2.01.
@@ -2250,7 +2243,7 @@
\item[\labelitemi] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
written in C. To use BerkMin, set the environment variable
\texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
-executable.\footref{cygwin-paths}
+executable.
The BerkMin executables are available at
\url{http://eigold.tripod.com/BerkMin.html}.
@@ -2259,7 +2252,6 @@
version of BerkMin, set the environment variable
\texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
executable.%
-\footref{cygwin-paths}
\item[\labelitemi] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
written in Java that can be used incrementally. It is bundled with Kodkodi and
--- a/src/HOL/Tools/Nitpick/kodkod.scala Thu Oct 07 16:28:17 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Thu Oct 07 21:43:26 2021 +0200
@@ -11,7 +11,7 @@
import java.util.concurrent.{TimeUnit, LinkedBlockingQueue, ThreadPoolExecutor}
import org.antlr.runtime.{ANTLRInputStream, RecognitionException}
-import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}
+import isabelle.kodkodi.{Context, KodkodiLexer, KodkodiParser}
object Kodkod
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Oct 07 16:28:17 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Oct 07 21:43:26 2021 +0200
@@ -18,9 +18,7 @@
open Kodkod
datatype sink = ToStdout | ToFile
-datatype availability =
- Java |
- JNI of int list
+datatype availability = Java | JNI of int list
datatype mode = Batch | Incremental
datatype sat_solver_info =
@@ -35,8 +33,7 @@
[("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
- ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
- "UNSAT")),
+ ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", "UNSAT")),
("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
"Instance Satisfiable", "",
@@ -53,45 +50,29 @@
("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
fun dynamic_entry_for_external name dev home exec args markers =
- case getenv home of
- "" => NONE
- | dir =>
- SOME (name, fn () =>
- let
- val serial_str = serial_string ()
- val base = name ^ serial_str
- val out_file = base ^ ".out"
- val dir_sep =
- if String.isSubstring "\\" dir andalso
- not (String.isSubstring "/" dir) then
- "\\"
- else
- "/"
- in
- [if null markers then "External" else "ExternalV2",
- dir ^ dir_sep ^ exec, base ^ ".cnf"] @
- (if null markers then []
- else [if dev = ToFile then out_file else ""]) @ markers @
- (if dev = ToFile then [out_file] else []) @ args
- end)
+ let
+ fun make_args () =
+ let val inpath = name ^ serial_string () ^ ".cnf" in
+ [if null markers then "External" else "ExternalV2"] @
+ [File.platform_path (Path.variable home + Path.platform_exe (Path.basic exec))] @
+ [inpath] @ (if null markers then [] else [if dev = ToFile then "out" else ""]) @
+ markers @ args
+ end
+ in if getenv home = "" then NONE else SOME (name, make_args) end
fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
- | dynamic_entry_for_info incremental
- (name, Internal (JNI from_version, mode, ss)) =
+ | dynamic_entry_for_info incremental (name, Internal (JNI from_version, mode, ss)) =
if (incremental andalso mode = Batch) orelse
- is_less (dict_ord int_ord (kodkodi_version (), from_version)) then
- NONE
+ is_less (dict_ord int_ord (kodkodi_version (), from_version))
+ then NONE
else
let
- val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH"
- |> space_explode ":"
+ val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH" |> space_explode ":"
in
- if exists (fn path => File.exists (Path.explode (path ^ "/")))
- lib_paths then
- SOME (name, K ss)
- else
- NONE
+ if exists (fn path => File.exists (Path.explode (path ^ "/"))) lib_paths
+ then SOME (name, K ss)
+ else NONE
end
| dynamic_entry_for_info false (name, External (home, exec, args)) =
dynamic_entry_for_external name ToStdout home exec args []
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_minisat.scala Thu Oct 07 21:43:26 2021 +0200
@@ -0,0 +1,153 @@
+/* Title: Pure/Admin/build_minisat.scala
+ Author: Makarius
+
+Build Isabelle Minisat from sources.
+*/
+
+package isabelle
+
+
+object Build_Minisat
+{
+ val default_download_url = "https://github.com/stp/minisat/archive/releases/2.2.1.tar.gz"
+
+ def make_component_name(version: String): String = "minisat-" + version
+
+
+ /* build Minisat */
+
+ def build_minisat(
+ download_url: String = default_download_url,
+ component_name: String = "",
+ verbose: Boolean = false,
+ progress: Progress = new Progress,
+ target_dir: Path = Path.current): Unit =
+ {
+ Isabelle_System.with_tmp_dir("build")(tmp_dir =>
+ {
+ /* component */
+
+ val Archive_Name = """^.*?([^/]+)$""".r
+ val Version = """^v?([0-9.]+)\.tar.gz$""".r
+
+ val archive_name =
+ download_url match {
+ case Archive_Name(name) => name
+ case _ => error("Failed to determine source archive name from " + quote(download_url))
+ }
+
+ val version =
+ archive_name match {
+ case Version(version) => version
+ case _ => error("Failed to determine component version from " + quote(archive_name))
+ }
+
+ val component = proper_string(component_name) getOrElse make_component_name(version)
+ val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
+ progress.echo("Component " + component_dir)
+
+
+ /* platform */
+
+ val platform_name =
+ proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
+ error("No 64bit platform")
+
+ val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
+
+
+ /* download source */
+
+ val archive_path = tmp_dir + Path.basic(archive_name)
+ Isabelle_System.download_file(download_url, archive_path, progress = progress)
+
+ Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+ val source_name = File.get_dir(tmp_dir)
+
+ Isabelle_System.bash(
+ "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+ cwd = component_dir.file).check
+
+
+ /* build */
+
+ progress.echo("Building Minisat for " + platform_name + " ...")
+
+ val build_dir = tmp_dir + Path.basic(source_name)
+ Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
+
+ if (Platform.is_macos) {
+ File.change(build_dir + Path.explode("Makefile"),
+ _.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", ""))
+ }
+ progress.bash("make r", build_dir.file, echo = verbose).check
+
+ Isabelle_System.copy_file(
+ build_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
+
+
+ /* settings */
+
+ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+ File.write(etc_dir + Path.basic("settings"),
+ """# -*- shell-script -*- :mode=shellscript:
+
+MINISAT_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
+
+ISABELLE_MINISAT="$MINISAT_HOME/minisat"
+""")
+
+
+ /* README */
+
+ File.write(component_dir + Path.basic("README"),
+ "This Isabelle component provides Minisat " + version + """ using the
+sources from """.stripMargin + download_url + """
+
+The executables have been built via "make r"; macOS requires to
+remove options "--static" and "-Wl,-soname,..." from the Makefile.
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+ })
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("build_minisat", "build prover component from sources", Scala_Project.here,
+ args =>
+ {
+ var target_dir = Path.current
+ var download_url = default_download_url
+ var component_name = ""
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle build_minisat [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -U URL download URL
+ (default: """" + default_download_url + """")
+ -n NAME component name (default: """" + make_component_name("VERSION") + """")
+ -v verbose
+
+ Build prover component from official download.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => download_url = arg),
+ "n:" -> (arg => component_name = arg),
+ "v" -> (_ => verbose = true))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress()
+
+ build_minisat(download_url = download_url, component_name = component_name,
+ verbose = verbose, progress = progress, target_dir = target_dir)
+ })
+}
--- a/src/Pure/Admin/build_vampire.scala Thu Oct 07 16:28:17 2021 +0200
+++ b/src/Pure/Admin/build_vampire.scala Thu Oct 07 21:43:26 2021 +0200
@@ -127,8 +127,8 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_vampire", "build prover component from repository", Scala_Project.here,
- args =>
+ Isabelle_Tool("build_vampire", "build prover component from official download",
+ Scala_Project.here, args =>
{
var target_dir = Path.current
var download_url = default_download_url
--- a/src/Pure/System/isabelle_tool.scala Thu Oct 07 16:28:17 2021 +0200
+++ b/src/Pure/System/isabelle_tool.scala Thu Oct 07 21:43:26 2021 +0200
@@ -222,6 +222,7 @@
Build_JCEF.isabelle_tool,
Build_JDK.isabelle_tool,
Build_JEdit.isabelle_tool,
+ Build_Minisat.isabelle_tool,
Build_PolyML.isabelle_tool1,
Build_PolyML.isabelle_tool2,
Build_SPASS.isabelle_tool,