| author | wenzelm | 
| Fri, 24 Nov 2023 21:32:32 +0100 | |
| changeset 79055 | c83cdd300848 | 
| parent 78746 | a748a244a028 | 
| child 79629 | 4d81c0391da2 | 
| 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")
 | 
| 
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 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 94 | val isabelle_tool = | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 95 |     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 | 96 |       { args =>
 | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 97 | var target_dir = Path.current | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 98 | var base_url = default_url | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 99 | var version = default_version | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 100 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 101 |         val getopts = Getopts("""
 | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 102 | Usage: isabelle component_hugo [OPTIONS] | 
| 
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 | Options are: | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 105 | -D DIR target directory (default ".") | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 106 | -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 | 107 | -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 | 108 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 109 | Build extended hugo component. | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 110 | """, | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 111 | "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 | 112 | "U:" -> (arg => base_url = arg), | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 113 | "V:" -> (arg => version = arg)) | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 114 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 115 | val more_args = getopts(args) | 
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 116 | 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 | 117 | |
| 
a748a244a028
add component build tool for hugo from afp-devel;
 Fabian Huch <huch@in.tum.de> parents: diff
changeset | 118 | val progress = new Console_Progress() | 
| 
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 | 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 | 121 | progress = 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 | } |