src/Pure/Admin/component_zipperposition.scala
author wenzelm
Sun, 19 May 2024 18:43:45 +0200
changeset 80181 aa92c0f96036
parent 80049 b525f783b784
child 80224 db92e0b6a11a
permissions -rw-r--r--
provide scala-3.4.2, but do not activate it: scala-3.3.x is LTS version;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 77510
diff changeset
     1
/*  Title:      Pure/Admin/component_zipperposition.scala
72466
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
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 77510
diff changeset
    10
object Component_Zipperposition {
74368
ac90d6c6c149 provide zipperposition-2.1 (still unused);
wenzelm
parents: 73340
diff changeset
    11
  val default_version = "2.1"
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    12
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
  /* build Zipperposition */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    15
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    16
  def build_zipperposition(
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    17
    version: String = default_version,
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    18
    progress: Progress = new Progress,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74457
diff changeset
    19
    target_dir: Path = Path.current
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74457
diff changeset
    20
  ): Unit = {
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    21
    Isabelle_System.with_tmp_dir("build") { build_dir =>
74457
4e317412db48 no patchelf on macOS (undetected due to cached executables?);
wenzelm
parents: 74368
diff changeset
    22
      if (Platform.is_linux) Isabelle_System.require_command("patchelf")
72471
aca85e8d873d more robust;
wenzelm
parents: 72467
diff changeset
    23
aca85e8d873d more robust;
wenzelm
parents: 72467
diff changeset
    24
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    25
      /* component */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    26
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    27
      val component_name = "zipperposition-" + version
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    28
      val component_dir =
76547
9fe5d8c70352 tuned signature;
wenzelm
parents: 76518
diff changeset
    29
        Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    30
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    31
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    32
      /* platform */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    33
80049
wenzelm
parents: 80004
diff changeset
    34
      val platform_name = Isabelle_Platform.self.ISABELLE_PLATFORM()
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    35
      val platform_dir =
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    36
        Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    37
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    38
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    39
      /* build */
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
      progress.echo("OCaml/OPAM setup ...")
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 76548
diff changeset
    42
      progress.bash("isabelle ocaml_setup", echo = progress.verbose).check
72466
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
      progress.echo("Building Zipperposition for " + platform_name + " ...")
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 76548
diff changeset
    45
      progress.bash(cwd = build_dir.file, echo = progress.verbose,
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    46
        script = "isabelle_opam install -y --destdir=" + File.bash_path(build_dir) +
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    47
          " zipperposition=" + Bash.string(version)).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
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    50
      /* install */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    51
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72971
diff changeset
    52
      Isabelle_System.copy_file(build_dir + Path.explode("doc/zipperposition/LICENSE"),
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    53
        component_dir.path)
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    54
72467
0822ff79eed8 proper support for Windows/Cygwin: "zipperposition" vs. "zipperposition.exe";
wenzelm
parents: 72466
diff changeset
    55
      val prg_path = Path.basic("zipperposition")
0822ff79eed8 proper support for Windows/Cygwin: "zipperposition" vs. "zipperposition.exe";
wenzelm
parents: 72466
diff changeset
    56
      val exe_path = prg_path.platform_exe
73317
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 72971
diff changeset
    57
      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
    58
72940
4a652d3f4522 proper support for Windows/Cygwin;
wenzelm
parents: 72939
diff changeset
    59
      if (!Platform.is_windows) {
79499
d117821a5e82 always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c);
wenzelm
parents: 77566
diff changeset
    60
        Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"))
72940
4a652d3f4522 proper support for Windows/Cygwin;
wenzelm
parents: 72939
diff changeset
    61
      }
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    62
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    63
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    64
      /* settings */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    65
76548
0af64cc2eee9 tuned signature;
wenzelm
parents: 76547
diff changeset
    66
      component_dir.write_settings("""
72971
162b71f7e554 rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
wenzelm
parents: 72940
diff changeset
    67
ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
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
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    71
      /* README */
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    72
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 75394
diff changeset
    73
      File.write(component_dir.README,
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    74
"""This is Zipperposition """ + version + """ from the OCaml/OPAM repository.
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    75
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    76
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    77
        Makarius
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    78
        """ + Date.Format.date(Date.now()) + "\n")
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    79
    }
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    80
}
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
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    83
  /* Isabelle tool wrapper */
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
  val isabelle_tool =
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 77510
diff changeset
    86
    Isabelle_Tool("component_zipperposition", "build prover component from OPAM repository",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    87
      Scala_Project.here,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    88
      { args =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    89
        var target_dir = Path.current
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    90
        var version = default_version
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    91
        var verbose = false
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    92
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    93
        val getopts = Getopts("""
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 77510
diff changeset
    94
Usage: isabelle component_zipperposition [OPTIONS]
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    95
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    96
  Options are:
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    97
    -D DIR       target directory (default ".")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    98
    -V VERSION   version (default: """" + default_version + """")
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
    99
    -v           verbose
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   100
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   101
  Build prover component from OPAM repository.
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   102
""",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   103
          "D:" -> (arg => target_dir = Path.explode(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   104
          "V:" -> (arg => version = arg),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   105
          "v" -> (_ => verbose = true))
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   106
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   107
        val more_args = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   108
        if (more_args.nonEmpty) getopts.usage()
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   109
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 76548
diff changeset
   110
        val progress = new Console_Progress(verbose = verbose)
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   111
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 76548
diff changeset
   112
        build_zipperposition(version = version, progress = progress, target_dir = target_dir)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   113
      })
72466
04403e1ef176 build Isabelle Zipperposition component from OPAM repository;
wenzelm
parents:
diff changeset
   114
}