| author | wenzelm | 
| Sun, 24 Mar 2024 19:14:56 +0100 | |
| changeset 79980 | ee04ce2ac13f | 
| parent 79975 | 90f4319c8b4f | 
| child 82030 | bae948b1132b | 
| permissions | -rw-r--r-- | 
| 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")
 | 
| 79975 | 20 | |
| 21 | def download(base_url: String, version: String): String = | |
| 78746 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 22 |       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 | 23 | } | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 24 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 25 | val platforms: List[Download_Platform] = | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 26 | List( | 
| 
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 | |
| 79975 | 57 | val download = platform.download(base_url, version) | 
| 58 | val name = | |
| 59 | Url.get_base_name(download) getOrElse | |
| 60 |           error("Malformed download name " + quote(download))
 | |
| 78746 
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 |       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 | 63 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 64 |       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 | 65 |         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 | 66 | 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 | 67 | |
| 79975 | 68 | Isabelle_System.download_file(download, archive_file, progress = progress) | 
| 78746 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 69 | 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 | 70 | 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 | 71 |           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 | 72 | 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 | 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 | |
| 
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 | /* settings */ | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 79 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 80 |     component_dir.write_settings("""
 | 
| 79974 | 81 | ISABELLE_HUGO="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
 | 
| 78746 
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 | |
| 
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 | /* README */ | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 86 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 87 | File.write(component_dir.README, | 
| 79975 | 88 | """This Isabelle components provides hugo extended """ + version + """. | 
| 78746 
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 | 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 | 91 | |
| 79975 | 92 | Fabian Huch | 
| 78746 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 93 | """ + 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 | 94 | } | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 95 | |
| 79629 | 96 | |
| 97 | /* Isabelle tool wrapper */ | |
| 98 | ||
| 78746 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 99 | val isabelle_tool = | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 100 |     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 | 101 |       { args =>
 | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 102 | var target_dir = Path.current | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 103 | var base_url = default_url | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 104 | var version = default_version | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 105 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 106 |         val getopts = Getopts("""
 | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 107 | Usage: isabelle component_hugo [OPTIONS] | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 108 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 109 | Options are: | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 110 | -D DIR target directory (default ".") | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 111 | -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 | 112 | -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 | 113 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 114 | Build extended hugo component. | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 115 | """, | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 116 | "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 | 117 | "U:" -> (arg => base_url = arg), | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 118 | "V:" -> (arg => version = arg)) | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 119 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 120 | val more_args = getopts(args) | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 121 | 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 | 122 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 123 | val progress = new Console_Progress() | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 124 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 125 | 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 | 126 | progress = progress) | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 127 | }) | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 128 | } |