src/Pure/Admin/component_hugo.scala
author wenzelm
Fri, 16 Feb 2024 11:25:11 +0100
changeset 79629 4d81c0391da2
parent 78746 a748a244a028
child 79974 f0150bc6fea5
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
78746
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     1
/*  Title:      Pure/Admin/component_hugo.scala
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     2
    Author:     Fabian Huch, TU Muenchen
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     3
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     4
Build Isabelle component for hugo site generator. See also:
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     5
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     6
  - https://gohugo.io
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     7
  - https://github.com/gohugoio/hugo
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     8
*/
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
     9
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    10
package isabelle
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    11
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    12
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    13
object Component_Hugo {
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    14
  /* platform information */
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    15
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    16
  sealed case class Download_Platform(platform_name: String, url_template: String) {
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    17
    override def toString: String = platform_name
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    18
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    19
    def is_windows: Boolean = url_template.contains("windows")
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    20
    def url(base_url: String, version: String): String =
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    21
      base_url + "/v" + version + "/" + url_template.replace("{V}", version)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    22
  }
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    23
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    24
  val platforms: List[Download_Platform] =
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    25
    List(
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    26
      Download_Platform("arm64-darwin", "hugo_extended_{V}_darwin-universal.tar.gz"),
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    27
      Download_Platform("arm64-linux", "hugo_extended_{V}_linux-arm64.tar.gz"),
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    28
      Download_Platform("x86_64-darwin", "hugo_extended_{V}_darwin-universal.tar.gz"),
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    29
      Download_Platform("x86_64-linux", "hugo_extended_{V}_linux-amd64.tar.gz"),
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    30
      Download_Platform("x86_64-windows", "hugo_extended_{V}_windows-amd64.zip"))
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    31
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    32
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    33
  /* build hugo */
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    34
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    35
  val default_url = "https://github.com/gohugoio/hugo/releases/download"
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    36
  val default_version = "0.119.0"
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    37
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    38
  def build_hugo(
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    39
    base_url: String = default_url,
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    40
    version: String = default_version,
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    41
    target_dir: Path = Path.current,
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    42
    progress: Progress = new Progress
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    43
  ): Unit = {
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    44
    /* component */
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    45
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    46
    val component = "hugo-" + version
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    47
    val component_dir =
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    48
      Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    49
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    50
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    51
    /* download */
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    52
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    53
    for (platform <- platforms) {
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    54
      val platform_dir =
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    55
        Isabelle_System.make_directory(component_dir.path + Path.basic(platform.platform_name))
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    56
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    57
      val url = platform.url(base_url, version)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    58
      val name = Library.take_suffix(_ != '/', url.toList)._2.mkString
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    59
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    60
      val exe = Path.basic("hugo").exe_if(platform.is_windows)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    61
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    62
      Isabelle_System.with_tmp_dir("download", component_dir.path.file) { download_dir =>
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    63
        Isabelle_System.with_tmp_dir("tmp", component_dir.path.file) { tmp_dir =>
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    64
          val archive_file = download_dir + Path.basic(name)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    65
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    66
          Isabelle_System.download_file(url, archive_file, progress = progress)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    67
          Isabelle_System.extract(archive_file, tmp_dir)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    68
          Isabelle_System.move_file(tmp_dir + exe, platform_dir)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    69
          Isabelle_System.move_file(tmp_dir + Path.basic("LICENSE"), component_dir.LICENSE)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    70
          File.set_executable(platform_dir + exe)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    71
        }
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    72
      }
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    73
    }
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    74
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    75
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    76
    /* settings */
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    77
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    78
    component_dir.write_settings("""
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    79
ISABELLE_HUGO="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    80
""")
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    81
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    82
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    83
    /* README */
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    84
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    85
    File.write(component_dir.README,
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    86
      """This Isabelle components provides a hugo extended """ + version + """.
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    87
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    88
See also https://gohugo.io and executables from """ + base_url + """
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    89
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    90
        Fabian
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    91
        """ + Date.Format.date(Date.now()) + "\n")
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    92
  }
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    93
79629
4d81c0391da2 tuned comments;
wenzelm
parents: 78746
diff changeset
    94
4d81c0391da2 tuned comments;
wenzelm
parents: 78746
diff changeset
    95
  /* Isabelle tool wrapper */
4d81c0391da2 tuned comments;
wenzelm
parents: 78746
diff changeset
    96
78746
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    97
  val isabelle_tool =
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    98
    Isabelle_Tool("component_hugo", "build hugo component", Scala_Project.here,
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
    99
      { args =>
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   100
        var target_dir = Path.current
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   101
        var base_url = default_url
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   102
        var version = default_version
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   103
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   104
        val getopts = Getopts("""
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   105
Usage: isabelle component_hugo [OPTIONS]
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   106
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   107
  Options are:
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   108
    -D DIR       target directory (default ".")
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   109
    -U URL       download URL (default: """" + default_url + """")
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   110
    -V VERSION   version (default: """" + default_version + """")
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   111
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   112
  Build extended hugo component.
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   113
""",
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   114
          "D:" -> (arg => target_dir = Path.explode(arg)),
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   115
          "U:" -> (arg => base_url = arg),
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   116
          "V:" -> (arg => version = arg))
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   117
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   118
        val more_args = getopts(args)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   119
        if (more_args.nonEmpty) getopts.usage()
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   120
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   121
        val progress = new Console_Progress()
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   122
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   123
        build_hugo(base_url = base_url, version = version, target_dir = target_dir,
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   124
          progress = progress)
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   125
    })
a748a244a028 add component build tool for hugo from afp-devel;
Fabian Huch <huch@in.tum.de>
parents:
diff changeset
   126
}