1/* Title: Pure/Admin/build_release.scala 2 Author: Makarius 3 4Build full Isabelle distribution from repository. 5*/ 6 7package isabelle 8 9 10object Build_Release 11{ 12 sealed case class Bundle_Info( 13 platform_family: String, 14 platform_description: String, 15 main: String, 16 fallback: Option[String]) 17 { 18 def names: List[String] = main :: fallback.toList 19 } 20 21 sealed case class Release_Info( 22 date: Date, 23 name: String, 24 dist_dir: Path, 25 dist_archive: Path, 26 dist_library_archive: Path, 27 id: String) 28 { 29 val bundle_infos: List[Bundle_Info] = 30 List(Bundle_Info("linux", "Linux", name + "_app.tar.gz", None), 31 Bundle_Info("windows", "Windows", name + ".exe", None), 32 Bundle_Info("macos", "Mac OS X", name + ".dmg", Some(name + "_dmg.tar.gz"))) 33 34 def bundle_info(platform_family: String): Bundle_Info = 35 bundle_infos.find(bundle_info => bundle_info.platform_family == platform_family) getOrElse 36 error("Unknown platform family " + quote(platform_family)) 37 } 38 39 40 private val default_platform_families = List("linux", "windows", "macos") 41 42 def build_release(base_dir: Path, 43 progress: Progress = No_Progress, 44 rev: String = "", 45 afp_rev: String = "", 46 official_release: Boolean = false, 47 release_name: String = "", 48 platform_families: List[String] = default_platform_families, 49 website: Option[Path] = None, 50 build_library: Boolean = false, 51 parallel_jobs: Int = 1, 52 remote_mac: String = ""): Release_Info = 53 { 54 /* release info */ 55 56 Isabelle_System.mkdirs(base_dir) 57 58 val release_info = 59 { 60 val date = Date.now() 61 val name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date)) 62 val dist_dir = base_dir + Path.explode("dist-" + name) 63 val dist_archive = dist_dir + Path.explode(name + ".tar.gz") 64 val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz") 65 Release_Info(date, name, dist_dir, dist_archive, dist_library_archive, "") 66 } 67 68 val bundle_infos = platform_families.map(release_info.bundle_info(_)) 69 70 71 /* make distribution */ 72 73 val jobs_option = " -j" + parallel_jobs.toString 74 75 val release_id = 76 { 77 val isabelle_ident_file = base_dir + Path.explode("ISABELLE_IDENT") 78 val isabelle_dist_file = base_dir + Path.explode("ISABELLE_DIST") 79 80 if (release_info.dist_archive.is_file && 81 isabelle_ident_file.is_file && isabelle_dist_file.is_file && 82 File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))), 83 release_info.dist_archive)) { 84 progress.echo("### Release archive already exists: " + release_info.dist_archive.implode) 85 } 86 else { 87 progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...") 88 progress.bash( 89 "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option + 90 (if (official_release) " -O" else "") + 91 (if (release_name != "") " -r " + Bash.string(release_name) else "") + 92 (if (rev != "") " " + Bash.string(rev) else ""), 93 echo = true).check 94 } 95 Library.trim_line(File.read(isabelle_ident_file)) 96 } 97 98 99 /* make application bundles */ 100 101 for (bundle_info <- bundle_infos) { 102 val bundle = 103 (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main 104 val bundle_archive = release_info.dist_dir + Path.explode(bundle) 105 if (bundle_archive.is_file) 106 progress.echo("### Application bundle already exists: " + bundle_archive.implode) 107 else { 108 progress.echo( 109 "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode) 110 progress.bash( 111 "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) + 112 " " + Bash.string(bundle_info.platform_family) + 113 (if (remote_mac == "") "" else " " + Bash.string(remote_mac)), 114 echo = true).check 115 } 116 } 117 118 119 /* minimal website */ 120 121 for (dir <- website) { 122 val website_platform_bundles = 123 for { 124 bundle_info <- bundle_infos 125 bundle <- 126 bundle_info.names.find(name => (release_info.dist_dir + Path.explode(name)).is_file) 127 } yield (bundle, bundle_info) 128 129 val afp_link = 130 HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) 131 132 HTML.write_document(dir, "index.html", 133 List(HTML.title(release_info.name)), 134 List( 135 HTML.chapter(release_info.name + " (" + release_id + ")"), 136 HTML.itemize( 137 website_platform_bundles.map({ case (bundle, bundle_info) => 138 List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: 139 (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) 140 141 for ((bundle, _) <- website_platform_bundles) 142 File.copy(release_info.dist_dir + Path.explode(bundle), dir) 143 } 144 145 146 /* HTML library */ 147 148 if (build_library) { 149 if (release_info.dist_library_archive.is_file) 150 progress.echo("### Library archive already exists: " + 151 release_info.dist_library_archive.implode) 152 else { 153 Isabelle_System.with_tmp_dir("build_release")(tmp_dir => 154 { 155 def execute(script: String): Unit = 156 Isabelle_System.bash(script, cwd = tmp_dir.file).check 157 def execute_tar(args: String): Unit = 158 Isabelle_System.gnutar(args, cwd = tmp_dir.file).check 159 160 val name = release_info.name 161 val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") 162 val bundle = release_info.dist_dir + Path.explode(name + "_" + platform + ".tar.gz") 163 execute_tar("xzf " + File.bash_path(bundle)) 164 165 val other_isabelle = 166 Other_Isabelle(tmp_dir + Path.explode(name), 167 isabelle_identifier = name + "-build", progress = progress) 168 169 other_isabelle.bash("bin/isabelle build" + jobs_option + 170 " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + 171 " -s -c -a -d '~~/src/Benchmarks'", echo = true).check 172 other_isabelle.isabelle_home_user.file.delete 173 174 execute("chmod -R a+r " + Bash.string(name)) 175 execute("chmod -R g=o " + Bash.string(name)) 176 execute_tar("--owner=root --group=root -czf " + 177 File.bash_path(release_info.dist_library_archive) + 178 " " + Bash.string(name + "/browser_info")) 179 }) 180 } 181 } 182 183 184 release_info.copy(id = release_id) 185 } 186 187 188 189 /** command line entry point **/ 190 191 def main(args: Array[String]) 192 { 193 Command_Line.tool0 { 194 var afp_rev = "" 195 var remote_mac = "" 196 var official_release = false 197 var release_name = "" 198 var website: Option[Path] = None 199 var parallel_jobs = 1 200 var build_library = false 201 var platform_families = default_platform_families 202 var rev = "" 203 204 val getopts = Getopts(""" 205Usage: Admin/build_release [OPTIONS] BASE_DIR 206 207 Options are: 208 -A REV corresponding AFP changeset id 209 -M USER@HOST remote Mac OS X for dmg build 210 -O official release (not release-candidate) 211 -R RELEASE proper release with name 212 -W WEBSITE produce minimal website in given directory 213 -j INT maximum number of parallel jobs (default 1) 214 -l build library 215 -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) 216 -r REV Mercurial changeset id (default: RELEASE or tip) 217 218 Build Isabelle release in base directory, using the local repository clone. 219""", 220 "A:" -> (arg => afp_rev = arg), 221 "M:" -> (arg => remote_mac = arg), 222 "O" -> (_ => official_release = true), 223 "R:" -> (arg => release_name = arg), 224 "W:" -> (arg => website = Some(Path.explode(arg))), 225 "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), 226 "l" -> (_ => build_library = true), 227 "p:" -> (arg => platform_families = space_explode(',', arg)), 228 "r:" -> (arg => rev = arg)) 229 230 val more_args = getopts(args) 231 val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } 232 233 val progress = new Console_Progress() 234 235 build_release(Path.explode(base_dir), progress = progress, rev = rev, afp_rev = afp_rev, 236 official_release = official_release, release_name = release_name, website = website, 237 platform_families = 238 if (platform_families.isEmpty) default_platform_families else platform_families, 239 build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) 240 } 241 } 242} 243