src/Pure/Admin/component_vampire.scala

--- a/src/Pure/Admin/component_vampire.scala	Wed Oct 25 11:52:40 2023 +0200
+++ b/src/Pure/Admin/component_vampire.scala	Wed Oct 25 13:01:47 2023 +0200
@@ -8,7 +8,8 @@
 
 
 object Component_Vampire {
-  val default_download_url = "https://github.com/vprover/vampire/archive/refs/tags/v4.6.tar.gz"
+  val default_download_url = "https://github.com/vprover/vampire/archive/refs/tags/v4.8HO4Sledgahammer.tar.gz"
+  val default_version = "4.8"
   val default_jobs = 1
 
   def make_component_name(version: String): String =
@@ -21,7 +22,7 @@
     download_url: String = default_download_url,
     jobs: Int = default_jobs,
     component_name: String = "",
-    component_version: String = "",
+    component_version: String = default_version,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
@@ -31,7 +32,6 @@
       /* component */
 
       val Archive_Name = """^.*?([^/]+)$""".r
-      val Version = """^v?([0-9.]+)\.tar.gz$""".r
 
       val archive_name =
         download_url match {
@@ -39,17 +39,9 @@
           case _ => error("Failed to determine source archive name from " + quote(download_url))
         }
 
-      val version =
-        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
-        }
+      if (component_version.isEmpty) error("Missing component version")
 
-      val component = proper_string(component_name) getOrElse make_component_name(version)
+      val component = proper_string(component_name) getOrElse make_component_name(component_version)
       val component_dir =
         Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
@@ -103,7 +95,7 @@
 
       component_dir.write_settings("""
 VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
-VAMPIRE_VERSION=""" + quote(version) + """
+VAMPIRE_VERSION=""" + quote(component_version) + """
 
 ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
 """)
@@ -112,7 +104,7 @@
       /* README */
 
       File.write(component_dir.README,
-        "This Isabelle component provides Vampire " + version + """using the
+        "This Isabelle component provides Vampire " + component_version + """using the
 original sources from """ + download_url + """
 
 The executables have been built via "cmake . && make"
@@ -134,7 +126,7 @@
       var download_url = default_download_url
       var jobs = default_jobs
       var component_name = ""
-      var component_version = ""
+      var component_version = default_version
       var verbose = false
 
       val getopts = Getopts("""
@@ -146,7 +138,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 VERSION   component version (default: """ + default_version + """)
     -v           verbose
 
   Build prover component from official download.