/* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { sealed case class Bundle_Info( platform_family: String, platform_description: String, main: String, fallback: Option[String]) { def names: List[String] = main :: fallback.toList } sealed case class Release_Info( date: Date, name: String, dist_dir: Path, dist_archive: Path, dist_library_archive: Path, id: String) { val bundle_infos: List[Bundle_Info] = List(Bundle_Info("linux", "Linux", name + "_app.tar.gz", None), Bundle_Info("windows", "Windows", name + ".exe", None), Bundle_Info("macos", "Mac OS X", name + ".dmg", Some(name + "_dmg.tar.gz"))) def bundle_info(platform_family: String): Bundle_Info = bundle_infos.find(bundle_info => bundle_info.platform_family == platform_family) getOrElse error("Unknown platform family " + quote(platform_family)) } private val default_platform_families = List("linux", "windows", "macos") def build_release(base_dir: Path, progress: Progress = No_Progress, rev: String = "", afp_rev: String = "", official_release: Boolean = false, release_name: String = "", platform_families: List[String] = default_platform_families, website: Option[Path] = None, build_library: Boolean = false, parallel_jobs: Int = 1, remote_mac: String = ""): Release_Info = { /* release info */ Isabelle_System.mkdirs(base_dir) val release_info = { val date = Date.now() val name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = base_dir + Path.explode("dist-" + name) val dist_archive = dist_dir + Path.explode(name + ".tar.gz") val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz") Release_Info(date, name, dist_dir, dist_archive, dist_library_archive, "") } val bundle_infos = platform_families.map(release_info.bundle_info(_)) /* make distribution */ val jobs_option = " -j" + parallel_jobs.toString val release_id = { val isabelle_ident_file = base_dir + Path.explode("ISABELLE_IDENT") val isabelle_dist_file = base_dir + Path.explode("ISABELLE_DIST") if (release_info.dist_archive.is_file && isabelle_ident_file.is_file && isabelle_dist_file.is_file && File.eq(Path.explode(Library.trim_line(File.read(isabelle_dist_file))), release_info.dist_archive)) { progress.echo("### Release archive already exists: " + release_info.dist_archive.implode) } else { progress.echo("Producing release archive " + release_info.dist_archive.implode + " ...") progress.bash( "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option + (if (official_release) " -O" else "") + (if (release_name != "") " -r " + Bash.string(release_name) else "") + (if (rev != "") " " + Bash.string(rev) else ""), echo = true).check } Library.trim_line(File.read(isabelle_ident_file)) } /* make application bundles */ for (bundle_info <- bundle_infos) { val bundle = (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main val bundle_archive = release_info.dist_dir + Path.explode(bundle) if (bundle_archive.is_file) progress.echo("### Application bundle already exists: " + bundle_archive.implode) else { progress.echo( "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode) progress.bash( "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) + " " + Bash.string(bundle_info.platform_family) + (if (remote_mac == "") "" else " " + Bash.string(remote_mac)), echo = true).check } } /* minimal website */ for (dir <- website) { val website_platform_bundles = for { bundle_info <- bundle_infos bundle <- bundle_info.names.find(name => (release_info.dist_dir + Path.explode(name)).is_file) } yield (bundle, bundle_info) val afp_link = HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(release_info.name)), List( HTML.chapter(release_info.name + " (" + release_id + ")"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) for ((bundle, _) <- website_platform_bundles) File.copy(release_info.dist_dir + Path.explode(bundle), dir) } /* HTML library */ if (build_library) { if (release_info.dist_library_archive.is_file) progress.echo("### Library archive already exists: " + release_info.dist_library_archive.implode) else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { def execute(script: String): Unit = Isabelle_System.bash(script, cwd = tmp_dir.file).check def execute_tar(args: String): Unit = Isabelle_System.gnutar(args, cwd = tmp_dir.file).check val name = release_info.name val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") val bundle = release_info.dist_dir + Path.explode(name + "_" + platform + ".tar.gz") execute_tar("xzf " + File.bash_path(bundle)) val other_isabelle = Other_Isabelle(tmp_dir + Path.explode(name), isabelle_identifier = name + "-build", progress = progress) other_isabelle.bash("bin/isabelle build" + jobs_option + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -s -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete execute("chmod -R a+r " + Bash.string(name)) execute("chmod -R g=o " + Bash.string(name)) execute_tar("--owner=root --group=root -czf " + File.bash_path(release_info.dist_library_archive) + " " + Bash.string(name + "/browser_info")) }) } } release_info.copy(id = release_id) } /** command line entry point **/ def main(args: Array[String]) { Command_Line.tool0 { var afp_rev = "" var remote_mac = "" var official_release = false var release_name = "" var website: Option[Path] = None var parallel_jobs = 1 var build_library = false var platform_families = default_platform_families var rev = "" val getopts = Getopts(""" Usage: Admin/build_release [OPTIONS] BASE_DIR Options are: -A REV corresponding AFP changeset id -M USER@HOST remote Mac OS X for dmg build -O official release (not release-candidate) -R RELEASE proper release with name -W WEBSITE produce minimal website in given directory -j INT maximum number of parallel jobs (default 1) -l build library -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: RELEASE or tip) Build Isabelle release in base directory, using the local repository clone. """, "A:" -> (arg => afp_rev = arg), "M:" -> (arg => remote_mac = arg), "O" -> (_ => official_release = true), "R:" -> (arg => release_name = arg), "W:" -> (arg => website = Some(Path.explode(arg))), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "p:" -> (arg => platform_families = space_explode(',', arg)), "r:" -> (arg => rev = arg)) val more_args = getopts(args) val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } val progress = new Console_Progress() build_release(Path.explode(base_dir), progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, release_name = release_name, website = website, platform_families = if (platform_families.isEmpty) default_platform_families else platform_families, build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac) } } }