# HG changeset patch # User desharna # Date 1697797616 -7200 # Node ID 09b5113e5c9d244e7ec1d13ae1927cf112ef9bd9 # Parent 4c5aadf1cb48191bce37a3f07a67937c4bad2442 tuned component_vampire script for Vampire 4.8 and added new flag to force version name diff -r 4c5aadf1cb48 -r 09b5113e5c9d src/Pure/Admin/component_vampire.scala --- a/src/Pure/Admin/component_vampire.scala Tue Oct 24 18:29:53 2023 +0200 +++ b/src/Pure/Admin/component_vampire.scala Fri Oct 20 12:26:56 2023 +0200 @@ -21,6 +21,7 @@ download_url: String = default_download_url, jobs: Int = default_jobs, component_name: String = "", + component_version: String = "", progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { @@ -39,9 +40,13 @@ } val version = - archive_name match { - case Version(version) => version - case _ => error("Failed to determine component version from " + quote(archive_name)) + component_version match { + case "" => + archive_name match { + case Version(version) => version + case _ => error("Failed to determine component version from " + quote(archive_name)) + } + case _ => component_version } val component = proper_string(component_name) getOrElse make_component_name(version) @@ -76,7 +81,9 @@ Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir.path) - val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else "" + val cmake_opts = + "-DCMAKE_BUILD_TYPE=Release -DCMAKE_BUILD_HOL=On -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON " + + (if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else "") val cmake_out = progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""", cwd = source_dir.file, echo = progress.verbose).check.out @@ -96,6 +103,7 @@ component_dir.write_settings(""" VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64" +VAMPIRE_VERSION=""" + quote(version) + """ ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire" """) @@ -126,6 +134,7 @@ var download_url = default_download_url var jobs = default_jobs var component_name = "" + var component_version = "" var verbose = false val getopts = Getopts(""" @@ -137,6 +146,7 @@ (default: """" + default_download_url + """") -j NUMBER parallel jobs for make (default: """ + default_jobs + """) -n NAME component name (default: """" + make_component_name("VERSION") + """") + -V VERSION component version (default: parsed from URL) -v verbose Build prover component from official download. @@ -145,6 +155,7 @@ "U:" -> (arg => download_url = arg), "j:" -> (arg => jobs = Value.Nat.parse(arg)), "n:" -> (arg => component_name = arg), + "V:" -> (arg => component_version = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) @@ -153,6 +164,7 @@ val progress = new Console_Progress(verbose = verbose) build_vampire(download_url = download_url, component_name = component_name, - jobs = jobs, progress = progress, target_dir = target_dir) + component_version = component_version, jobs = jobs, progress = progress, + target_dir = target_dir) }) }