src/Pure/Admin/build_vampire.scala
author wenzelm
Fri, 07 May 2021 23:56:18 +0200
changeset 73906 9ce115baaa4f
parent 73590 0ffcad1f6130
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/build_vampire.scala
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     3
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     4
Build Isabelle Vampire component from repository.
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     5
*/
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     6
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     7
package isabelle
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     8
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
     9
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    10
object Build_Vampire
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    11
{
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    12
  val default_repository = "https://github.com/vprover/vampire.git"
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    13
  val default_version1 = "4.5.1"
73126
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
    14
  val default_version2 = "df87588848db"
73127
42d75bf8725c parallel jobs for make;
wenzelm
parents: 73126
diff changeset
    15
  val default_jobs = 1
73124
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
    16
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
    17
  def make_component_name(version: String) = "vampire-" + version
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    18
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    19
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    20
  /* build Vampire */
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    21
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    22
  def build_vampire(
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    23
    repository: String = default_repository,
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    24
    version1: String = default_version1,
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    25
    version2: String = default_version2,
73127
42d75bf8725c parallel jobs for make;
wenzelm
parents: 73126
diff changeset
    26
    jobs: Int = default_jobs,
73124
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
    27
    component_name: String = "",
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    28
    verbose: Boolean = false,
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    29
    progress: Progress = new Progress,
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73564
diff changeset
    30
    target_dir: Path = Path.current): Unit =
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    31
  {
73906
9ce115baaa4f clarified signature;
wenzelm
parents: 73590
diff changeset
    32
    Isabelle_System.require_command("git")
9ce115baaa4f clarified signature;
wenzelm
parents: 73590
diff changeset
    33
    Isabelle_System.require_command("cmake")
73178
bc88423eb0ad more checks;
wenzelm
parents: 73128
diff changeset
    34
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    35
    Isabelle_System.with_tmp_dir("build")(tmp_dir =>
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    36
    {
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    37
      /* component and platform */
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    38
73124
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
    39
      val component = proper_string(component_name) getOrElse make_component_name(version1)
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
    40
      val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    41
      progress.echo("Component " + component_dir)
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    42
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    43
      val platform_name =
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    44
        proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    45
          error("No 64bit platform")
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    46
      val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    47
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    48
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    49
      /* clone repository */
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    50
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    51
      progress.echo("Cloning repository " + repository)
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    52
      progress.bash("git clone " + Bash.string(repository) + " vampire",
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    53
        cwd = tmp_dir.file, echo = verbose).check
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    54
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    55
      val source_dir = tmp_dir + Path.explode("vampire")
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    56
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73178
diff changeset
    57
      Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir)
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    58
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    59
73126
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
    60
      /* build versions */
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    61
73126
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
    62
      for { (rev, exe) <- List(version1 -> "vampire", version2 -> "vampire_polymorphic") } {
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    63
        progress.echo("Building " + exe + " (rev " + rev + ")")
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    64
        progress.bash("git checkout --quiet --detach " + Bash.string(rev),
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    65
          cwd = source_dir.file, echo = verbose).check
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    66
73128
6751057a64b1 purge build dir;
wenzelm
parents: 73127
diff changeset
    67
        val build_dir = source_dir + Path.explode("build")
6751057a64b1 purge build dir;
wenzelm
parents: 73127
diff changeset
    68
        Isabelle_System.rm_tree(build_dir)
6751057a64b1 purge build dir;
wenzelm
parents: 73127
diff changeset
    69
        Isabelle_System.make_directory(build_dir)
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    70
73126
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
    71
        val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    72
        val cmake_out =
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    73
          progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" ..""",
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    74
            cwd = build_dir.file, echo = verbose).check.out
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    75
73126
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
    76
        val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    77
        val binary =
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    78
          split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    79
            .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    80
73127
42d75bf8725c parallel jobs for make;
wenzelm
parents: 73126
diff changeset
    81
        progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    82
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73178
diff changeset
    83
        Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
73125
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    84
          platform_dir + Path.basic(exe).platform_exe)
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    85
      }
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    86
74d785882737 prefer cmake build for standard version: more portable;
wenzelm
parents: 73124
diff changeset
    87
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    88
      /* settings */
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    89
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    90
      val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    91
      File.write(etc_dir + Path.basic("settings"),
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    92
        """# -*- shell-script -*- :mode=shellscript:
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    93
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    94
VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    95
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    96
ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    97
ISABELLE_VAMPIRE_POLYMORPHIC="$VAMPIRE_HOME/vampire_polymorphic"
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    98
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
    99
VAMPIRE_EXTRA_OPTIONS=""
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   100
""")
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   101
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   102
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   103
      /* README */
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   104
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   105
      File.write(component_dir + Path.basic("README"),
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   106
        "This Isabelle component provides two versions of Vampire from\n" + repository + """
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   107
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   108
  * vampire: standard version (regular stable release)
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   109
  * vampire_polymorphic: special version for polymorphic FOL and HOL
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   110
    (intermediate repository version)
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   111
73126
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
   112
The executables have been built like this:
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
   113
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
   114
    git checkout COMMIT
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
   115
    cmake .
5db643841f5d back to uniform build, using latest repository version for vampire_polymorphic;
wenzelm
parents: 73125
diff changeset
   116
    make
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   117
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   118
The precise commit id is revealed by executing "vampire --version".
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   119
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   120
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   121
        Makarius
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   122
        """ + Date.Format.date(Date.now()) + "\n")
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   123
    })
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   124
  }
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   125
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   126
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   127
  /* Isabelle tool wrapper */
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   128
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   129
  val isabelle_tool =
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   130
    Isabelle_Tool("build_vampire", "build prover component from repository", Scala_Project.here,
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   131
    args =>
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   132
    {
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   133
      var target_dir = Path.current
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   134
      var repository = default_repository
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   135
      var version1 = default_version1
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   136
      var version2 = default_version2
73127
42d75bf8725c parallel jobs for make;
wenzelm
parents: 73126
diff changeset
   137
      var jobs = default_jobs
73124
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
   138
      var component_name = ""
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   139
      var verbose = false
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   140
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   141
      val getopts = Getopts("""
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   142
Usage: isabelle build_vampire [OPTIONS]
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   143
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   144
  Options are:
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   145
    -D DIR       target directory (default ".")
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   146
    -U URL       repository (default: """" + default_repository + """")
73124
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
   147
    -V REV1      standard version (default: """" + default_version1 + """")
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
   148
    -W REV2      polymorphic version (default: """" + default_version2 + """")
73127
42d75bf8725c parallel jobs for make;
wenzelm
parents: 73126
diff changeset
   149
    -j NUMBER    parallel jobs for make (default: """ + default_jobs + """)
73124
970bad477c13 clarified default name;
wenzelm
parents: 73123
diff changeset
   150
    -n NAME      component name (default: """" + make_component_name("REV1") + """")
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   151
    -v           verbose
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   152
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   153
  Build prover component from official download.
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   154
""",
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   155
        "D:" -> (arg => target_dir = Path.explode(arg)),
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   156
        "U:" -> (arg => repository = arg),
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   157
        "V:" -> (arg => version1 = arg),
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   158
        "W:" -> (arg => version2 = arg),
73127
42d75bf8725c parallel jobs for make;
wenzelm
parents: 73126
diff changeset
   159
        "j:" -> (arg => jobs = Value.Nat.parse(arg)),
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   160
        "n:" -> (arg => component_name = arg),
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   161
        "v" -> (_ => verbose = true))
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   162
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   163
      val more_args = getopts(args)
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   164
      if (more_args.nonEmpty) getopts.usage()
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   165
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   166
      val progress = new Console_Progress()
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   167
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   168
      build_vampire(repository = repository, version1 = version1, version2 = version2,
73127
42d75bf8725c parallel jobs for make;
wenzelm
parents: 73126
diff changeset
   169
        component_name = component_name, jobs = jobs, verbose = verbose, progress = progress,
73123
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   170
        target_dir = target_dir)
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   171
    })
ac64b753a65f build Isabelle Vampire component from repository;
wenzelm
parents:
diff changeset
   172
}