--- a/src/Pure/Admin/build_vampire.scala Wed Oct 06 10:58:05 2021 +0200
+++ b/src/Pure/Admin/build_vampire.scala Wed Oct 06 13:28:11 2021 +0200
@@ -10,19 +10,18 @@
object Build_Vampire
{
val default_repository = "https://github.com/vprover/vampire.git"
- val default_version1 = "4.5.1"
- val default_version2 = "df87588848db"
+ val default_version = "4.5.1"
val default_jobs = 1
- def make_component_name(version: String): String = "vampire-" + version
+ def make_component_name(version: String): String =
+ "vampire-" + Library.try_unprefix("v", version).getOrElse(version)
/* build Vampire */
def build_vampire(
repository: String = default_repository,
- version1: String = default_version1,
- version2: String = default_version2,
+ version: String = default_version,
jobs: Int = default_jobs,
component_name: String = "",
verbose: Boolean = false,
@@ -36,7 +35,7 @@
{
/* component and platform */
- val component = proper_string(component_name) getOrElse make_component_name(version1)
+ 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)
@@ -57,32 +56,30 @@
Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir)
- /* build versions */
+ /* build */
- for { (rev, exe) <- List(version1 -> "vampire", version2 -> "vampire_polymorphic") } {
- progress.echo("Building " + exe + " (rev " + rev + ")")
- progress.bash("git checkout --quiet --detach " + Bash.string(rev),
- cwd = source_dir.file, echo = verbose).check
+ progress.echo("Building vampire")
+ progress.bash("git checkout --quiet --detach " + Bash.string(version),
+ cwd = source_dir.file, echo = verbose).check
- val build_dir = source_dir + Path.explode("build")
- Isabelle_System.rm_tree(build_dir)
- Isabelle_System.make_directory(build_dir)
+ val build_dir = source_dir + Path.explode("build")
+ Isabelle_System.rm_tree(build_dir)
+ Isabelle_System.make_directory(build_dir)
- val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
- val cmake_out =
- progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" ..""",
- cwd = build_dir.file, echo = verbose).check.out
+ val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
+ val cmake_out =
+ progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" ..""",
+ cwd = build_dir.file, echo = verbose).check.out
- val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
- val binary =
- split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
- .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
+ val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
+ val binary =
+ split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
+ .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
- progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
+ progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
- Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
- platform_dir + Path.basic(exe).platform_exe)
- }
+ Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
+ platform_dir + Path.basic("vampire").platform_exe)
/* settings */
@@ -94,22 +91,18 @@
VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
-ISABELLE_VAMPIRE_POLYMORPHIC="$VAMPIRE_HOME/vampire_polymorphic"
""")
/* README */
File.write(component_dir + Path.basic("README"),
- "This Isabelle component provides two versions of Vampire from\n" + repository + """
+ "This Isabelle component provides Vampire " + version + """
+using original sources from https://github.com/vprover/vampire
- * vampire: standard version (regular stable release)
- * vampire_polymorphic: special version for polymorphic FOL and HOL
- (intermediate repository version)
+The executable has been built like this:
-The executables have been built like this:
-
- git checkout COMMIT
+ git checkout REV
cmake .
make
@@ -130,8 +123,7 @@
{
var target_dir = Path.current
var repository = default_repository
- var version1 = default_version1
- var version2 = default_version2
+ var version = default_version
var jobs = default_jobs
var component_name = ""
var verbose = false
@@ -142,18 +134,16 @@
Options are:
-D DIR target directory (default ".")
-U URL repository (default: """" + default_repository + """")
- -V REV1 standard version (default: """" + default_version1 + """")
- -W REV2 polymorphic version (default: """" + default_version2 + """")
+ -V REV version tag (default: """" + default_version + """")
-j NUMBER parallel jobs for make (default: """ + default_jobs + """)
- -n NAME component name (default: """" + make_component_name("REV1") + """")
+ -n NAME component name (default: """" + make_component_name("REV") + """")
-v verbose
Build prover component from official download.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"U:" -> (arg => repository = arg),
- "V:" -> (arg => version1 = arg),
- "W:" -> (arg => version2 = arg),
+ "V:" -> (arg => version = arg),
"j:" -> (arg => jobs = Value.Nat.parse(arg)),
"n:" -> (arg => component_name = arg),
"v" -> (_ => verbose = true))
@@ -163,8 +153,7 @@
val progress = new Console_Progress()
- build_vampire(repository = repository, version1 = version1, version2 = version2,
- component_name = component_name, jobs = jobs, verbose = verbose, progress = progress,
- target_dir = target_dir)
+ build_vampire(repository = repository, version = version, component_name = component_name,
+ jobs = jobs, verbose = verbose, progress = progress, target_dir = target_dir)
})
}