src/Pure/Admin/component_zstd.scala
author wenzelm
Sun, 19 Nov 2023 12:51:47 +0100
changeset 78992 bd250213c262
parent 78298 3b0f8f1010f2
permissions -rw-r--r--
unused (see also 004b39bf06a5);
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: 76548
diff changeset
     1
/*  Title:      Pure/Admin/component_zstd.scala
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     3
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     4
Build Isabelle zstd-jni component from official download.
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     5
*/
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     6
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     7
package isabelle
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     8
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     9
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 76548
diff changeset
    10
object Component_Zstd {
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    11
  /* platforms */
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    12
76457
badbae70c51a tuned signature;
wenzelm
parents: 76348
diff changeset
    13
  sealed case class Platform_Info(name: String, template: String, exe: Boolean = false) {
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    14
    def install(jar_dir: Path, component_dir: Path, version: String): Unit = {
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    15
      val source = jar_dir + Path.explode(template.replace("{V}", version))
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    16
      val target = Isabelle_System.make_directory(component_dir + Path.basic(name))
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    17
      Isabelle_System.copy_file(source, target)
78298
3b0f8f1010f2 clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
wenzelm
parents: 78147
diff changeset
    18
      if (exe) File.set_executable(target + source.base)
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    19
    }
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    20
  }
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    21
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    22
  private val platforms =
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    23
    List(
76457
badbae70c51a tuned signature;
wenzelm
parents: 76348
diff changeset
    24
      Platform_Info("arm64-darwin", "darwin/aarch64/libzstd-jni-{V}.dylib"),
badbae70c51a tuned signature;
wenzelm
parents: 76348
diff changeset
    25
      Platform_Info("x86_64-darwin", "darwin/x86_64/libzstd-jni-{V}.dylib"),
badbae70c51a tuned signature;
wenzelm
parents: 76348
diff changeset
    26
      Platform_Info("arm64-linux", "linux/aarch64/libzstd-jni-{V}.so"),
badbae70c51a tuned signature;
wenzelm
parents: 76348
diff changeset
    27
      Platform_Info("x86_64-linux", "linux/amd64/libzstd-jni-{V}.so"),
badbae70c51a tuned signature;
wenzelm
parents: 76348
diff changeset
    28
      Platform_Info("x86_64-windows", "win/amd64/libzstd-jni-{V}.dll", exe = true))
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    29
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    30
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    31
  /* build zstd */
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    32
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    33
  val license_url = "https://raw.githubusercontent.com/luben/zstd-jni/master/LICENSE"
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    34
  val default_download_url = "https://repo1.maven.org/maven2/com/github/luben/zstd-jni"
78147
f4221ae7544c updated to zstd-jni-1.5.5-4;
wenzelm
parents: 77566
diff changeset
    35
  val default_version = "1.5.5-4"
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    36
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    37
  def build_zstd(
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    38
    target_dir: Path = Path.current,
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    39
    download_url: String = default_download_url,
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    40
    version: String = default_version,
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    41
    progress: Progress = new Progress,
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    42
  ): Unit = {
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    43
    /* component */
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    44
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    45
    val component_name = "zstd-jni-" + version
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76457
diff changeset
    46
    val component_dir =
76547
9fe5d8c70352 tuned signature;
wenzelm
parents: 76543
diff changeset
    47
      Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    48
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76457
diff changeset
    49
    File.write(component_dir.README,
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    50
      "This is " + component_name + " from\n" + download_url +
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    51
        "\n\n        Makarius\n        " + Date.Format.date(Date.now()) + "\n")
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    52
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76457
diff changeset
    53
    Isabelle_System.download_file(license_url, component_dir.LICENSE, progress = progress)
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    54
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    55
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    56
    /* jar */
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    57
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    58
    val jar_name = component_name + ".jar"
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76457
diff changeset
    59
    val jar = component_dir.path + Path.basic(jar_name)
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    60
    Isabelle_System.download_file(
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    61
      download_url + "/" + version + "/" + jar_name, jar, progress = progress)
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    62
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    63
    Isabelle_System.with_tmp_dir("build") { jar_dir =>
76543
fef0195f8d8e clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents: 76518
diff changeset
    64
      Isabelle_System.extract(jar, jar_dir)
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76457
diff changeset
    65
      for (platform <- platforms) platform.install(jar_dir, component_dir.path, version)
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    66
    }
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    67
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    68
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    69
    /* settings */
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    70
76548
0af64cc2eee9 tuned signature;
wenzelm
parents: 76547
diff changeset
    71
    component_dir.write_settings("""
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    72
ISABELLE_ZSTD_HOME="$COMPONENT"
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    73
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    74
classpath "$ISABELLE_ZSTD_HOME/""" + jar_name + """"
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    75
""")
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    76
  }
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    77
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    78
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    79
  /* Isabelle tool wrapper */
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    80
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    81
  val isabelle_tool =
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 76548
diff changeset
    82
    Isabelle_Tool("component_zstd", "build Isabelle zstd-jni component from official download",
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    83
      Scala_Project.here,
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    84
      { args =>
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    85
        var target_dir = Path.current
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    86
        var download_url = default_download_url
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    87
        var version = default_version
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    88
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    89
        val getopts = Getopts("""
77566
2a99fcb283ee renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents: 76548
diff changeset
    90
Usage: isabelle component_zstd [OPTIONS]
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    91
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    92
  Options are:
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    93
    -D DIR       target directory (default ".")
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    94
    -U URL       download URL (default: """ + quote(default_download_url) + """)
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    95
    -V VERSION   version (default: """ + quote(default_version) + """)
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    96
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    97
  Build zstd-jni component from the specified download base URL and VERSION,
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    98
  see also https://github.com/luben/zstd-jni
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    99
""",
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   100
          "D:" -> (arg => target_dir = Path.explode(arg)),
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   101
          "U:" -> (arg => download_url = arg),
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   102
          "V:" -> (arg => version = arg))
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   103
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   104
        val more_args = getopts(args)
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   105
        if (more_args.nonEmpty) getopts.usage()
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   106
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   107
        val progress = new Console_Progress()
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   108
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   109
        build_zstd(target_dir = target_dir, download_url = download_url,
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   110
          version = version, progress = progress)
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   111
      })
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
   112
}