# HG changeset patch # User wenzelm # Date 1633635806 -7200 # Node ID f8ad2ee7638d55fc3f619d0b962a3a256b88c685 # Parent fd5f62176987041396115c9a8554c8f5458089b2# Parent 74a36aae067a9569c52035b7ebc67e0599d9d2a6 merged diff -r fd5f62176987 -r f8ad2ee7638d Admin/components/components.sha1 --- 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 diff -r fd5f62176987 -r f8ad2ee7638d Admin/components/main --- 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 diff -r fd5f62176987 -r f8ad2ee7638d etc/build.props --- 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 \ diff -r fd5f62176987 -r f8ad2ee7638d src/Doc/Nitpick/document/root.tex --- 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 diff -r fd5f62176987 -r f8ad2ee7638d src/HOL/Tools/Nitpick/kodkod.scala --- 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 diff -r fd5f62176987 -r f8ad2ee7638d src/HOL/Tools/Nitpick/kodkod_sat.ML --- 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 [] diff -r fd5f62176987 -r f8ad2ee7638d src/Pure/Admin/build_minisat.scala --- /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) + }) +} diff -r fd5f62176987 -r f8ad2ee7638d src/Pure/Admin/build_vampire.scala --- 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 diff -r fd5f62176987 -r f8ad2ee7638d src/Pure/System/isabelle_tool.scala --- 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,