src/Pure/Admin/build_zipperposition.scala
author wenzelm
Mon, 27 Sep 2021 20:45:26 +0200
changeset 74368 ac90d6c6c149
parent 73340 0ffcad1f6130
child 74457 4e317412db48
permissions -rw-r--r--
provide zipperposition-2.1 (still unused);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/build_zipperposition.scala
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     3
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     4
Build Isabelle Zipperposition component from OPAM repository.
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     5
*/
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     6
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     7
package isabelle
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     8
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
     9
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    10
object Build_Zipperposition
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    11
{
74368
ac90d6c6c149 provide zipperposition-2.1 (still unused);
wenzelm
parents: 73340
diff changeset
    12
  val default_version = "2.1"
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    13
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    14
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    15
  /* build Zipperposition */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    16
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    17
  def build_zipperposition(
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    18
    version: String = default_version,
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    19
    verbose: Boolean = false,
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    20
    progress: Progress = new Progress,
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73317
diff changeset
    21
    target_dir: Path = Path.current): Unit =
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    22
  {
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    23
    Isabelle_System.with_tmp_dir("build")(build_dir =>
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    24
    {
72940
4a652d3f4522 proper support for Windows/Cygwin;
wenzelm
parents: 72939
diff changeset
    25
      if (!Platform.is_windows) Isabelle_System.require_command("patchelf")
72471
aca85e8d873d more robust;
wenzelm
parents: 72467
diff changeset
    26
aca85e8d873d more robust;
wenzelm
parents: 72467
diff changeset
    27
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    28
      /* component */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    29
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    30
      val component_name = "zipperposition-" + version
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    31
      val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    32
      progress.echo("Component " + component_dir)
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    33
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    34
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    35
      /* platform */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    36
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    37
      val platform_name =
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    38
        proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64")) getOrElse
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    39
        error("No 64bit platform")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    40
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    41
      val platform_dir = Isabelle_System.make_directory(component_dir + Path.basic(platform_name))
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    42
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    43
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    44
      /* build */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    45
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    46
      progress.echo("OCaml/OPAM setup ...")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    47
      progress.bash("isabelle ocaml_setup", echo = verbose).check
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    48
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    49
      progress.echo("Building Zipperposition for " + platform_name + " ...")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    50
      progress.bash(cwd = build_dir.file, echo = verbose,
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    51
        script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) +
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    52
          " zipperposition=" + Bash.string(version)).check
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    53
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    54
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    55
      /* install */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    56
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72971
diff changeset
    57
      Isabelle_System.copy_file(build_dir + Path.explode("doc/zipperposition/LICENSE"),
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72971
diff changeset
    58
        component_dir)
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    59
72467
0822ff79eed8 proper support for Windows/Cygwin: "zipperposition" vs. "zipperposition.exe";
wenzelm
parents: 72466
diff changeset
    60
      val prg_path = Path.basic("zipperposition")
0822ff79eed8 proper support for Windows/Cygwin: "zipperposition" vs. "zipperposition.exe";
wenzelm
parents: 72466
diff changeset
    61
      val exe_path = prg_path.platform_exe
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72971
diff changeset
    62
      Isabelle_System.copy_file(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path)
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    63
72940
4a652d3f4522 proper support for Windows/Cygwin;
wenzelm
parents: 72939
diff changeset
    64
      if (!Platform.is_windows) {
4a652d3f4522 proper support for Windows/Cygwin;
wenzelm
parents: 72939
diff changeset
    65
        Executable.libraries_closure(
4a652d3f4522 proper support for Windows/Cygwin;
wenzelm
parents: 72939
diff changeset
    66
          platform_dir + exe_path, filter = Set("libgmp"), patchelf = true)
4a652d3f4522 proper support for Windows/Cygwin;
wenzelm
parents: 72939
diff changeset
    67
      }
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    68
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    69
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    70
      /* settings */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    71
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    72
      val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    73
      File.write(etc_dir + Path.basic("settings"),
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    74
        """# -*- shell-script -*- :mode=shellscript:
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    75
72971
162b71f7e554 rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents: 72940
diff changeset
    76
ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    77
""")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    78
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    79
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    80
      /* README */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    81
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    82
      File.write(component_dir + Path.basic("README"),
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    83
"""This is Zipperposition """ + version + """ from the OCaml/OPAM repository.
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    84
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    85
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    86
        Makarius
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    87
        """ + Date.Format.date(Date.now()) + "\n")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    88
    })
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    89
}
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    90
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    91
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    92
  /* Isabelle tool wrapper */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    93
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    94
  val isabelle_tool =
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    95
    Isabelle_Tool("build_zipperposition", "build prover component from OPAM repository",
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72471
diff changeset
    96
      Scala_Project.here, args =>
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    97
    {
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    98
      var target_dir = Path.current
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    99
      var version = default_version
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   100
      var verbose = false
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   101
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   102
      val getopts = Getopts("""
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   103
Usage: isabelle build_zipperposition [OPTIONS]
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   104
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   105
  Options are:
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   106
    -D DIR       target directory (default ".")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   107
    -V VERSION   version (default: """" + default_version + """")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   108
    -v           verbose
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   109
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   110
  Build prover component from OPAM repository.
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   111
""",
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   112
        "D:" -> (arg => target_dir = Path.explode(arg)),
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   113
        "V:" -> (arg => version = arg),
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   114
        "v" -> (_ => verbose = true))
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   115
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   116
      val more_args = getopts(args)
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   117
      if (more_args.nonEmpty) getopts.usage()
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   118
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   119
      val progress = new Console_Progress()
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   120
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   121
      build_zipperposition(version = version, verbose = verbose, progress = progress,
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   122
        target_dir = target_dir)
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   123
    })
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   124
}