--- a/src/Pure/Admin/build_release.scala Sun Oct 21 14:35:46 2018 +0200
+++ b/src/Pure/Admin/build_release.scala Sun Oct 21 18:32:33 2018 +0200
@@ -9,6 +9,101 @@
object Build_Release
{
+ /** generated content **/
+
+ /* patch release */
+
+ private def change_file(dir: Path, name: String, f: String => String)
+ {
+ val file = dir + Path.explode(name)
+ File.write(file, f(File.read(file)))
+ }
+
+ def patch_release(
+ dir: Path, ident: String, is_official: Boolean, dist_name: String, dist_version: String)
+ {
+ for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
+ {
+ change_file(dir, name,
+ s =>
+ s.replaceAll("val is_identified = false", "val is_identified = true")
+ .replaceAll("val is_official = false", "val is_official = " + is_official))
+ }
+
+ change_file(dir, "lib/scripts/getsettings",
+ s =>
+ s.replaceAll("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(ident))
+ .replaceAll("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(dist_name)))
+
+ change_file(dir, "lib/html/library_index_header.template",
+ s => s.replaceAll("""\{ISABELLE\}""", dist_name))
+
+ for {
+ name <-
+ List(
+ "src/Pure/System/distribution.ML",
+ "src/Pure/System/distribution.scala",
+ "lib/Tools/version") }
+ {
+ change_file(dir, name, s => s.replaceAll("repository version", dist_version))
+ }
+
+ change_file(dir, "README",
+ s => s.replaceAll("some repository version of Isabelle", dist_version))
+ }
+
+
+ /* ANNOUNCE */
+
+ def make_announce(dir: Path, ident: String)
+ {
+ File.write(dir + Path.explode("ANNOUNCE"),
+"""
+IMPORTANT NOTE
+==============
+
+This is a snapshot of Isabelle/""" + ident + """ from the repository.
+
+""")
+ }
+
+
+ /* NEWS */
+
+ def make_news(other_isabelle: Other_Isabelle, dist_version: String)
+ {
+ val target = other_isabelle.isabelle_home + Path.explode("doc")
+ val target_fonts = target + Path.explode("fonts")
+ Isabelle_System.mkdirs(target_fonts)
+
+ for (font <- other_isabelle.fonts(html = true))
+ File.copy(font, target_fonts)
+
+ HTML.write_document(target, "NEWS.html",
+ List(HTML.title("NEWS (" + dist_version + ")")),
+ List(
+ HTML.chapter("NEWS"),
+ HTML.source(
+ Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
+ }
+
+
+ /* contrib */
+
+ def make_contrib(dir: Path)
+ {
+ Isabelle_System.mkdirs(dir + Path.explode("contrib"))
+ File.write(dir + Path.explode("contrib/README"),
+"""This directory contains add-on components that contribute to the main
+Isabelle distribution. Separate licensing conditions apply, see each
+directory individually.
+""")
+ }
+
+
+
+ /** build_release **/
+
sealed case class Bundle_Info(
platform_family: String,
platform_description: String,
@@ -20,22 +115,35 @@
sealed case class Release(
date: Date,
- name: String,
+ dist_name: String,
dist_dir: Path,
- dist_archive: Path,
- dist_library_archive: Path,
- id: String)
+ ident: String)
{
+ val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
+ val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
+ val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
+
+ val other_isabelle_identifier: String = dist_name + "-build"
+
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")))
+ List(Bundle_Info("linux", "Linux", dist_name + "_app.tar.gz", None),
+ Bundle_Info("windows", "Windows", dist_name + ".exe", None),
+ Bundle_Info("macos", "Mac OS X", dist_name + ".dmg", Some(dist_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))
+
+ def execute_dist_name(dir: Path, script: String): Unit =
+ Isabelle_System.bash(script, cwd = dir.file,
+ env = Isabelle_System.settings() + ("DIST_NAME" -> dist_name)).check
}
+ private def execute(dir: Path, script: String): Unit =
+ Isabelle_System.bash(script, cwd = dir.file).check
+
+ private def execute_tar(dir: Path, args: String): Unit =
+ Isabelle_System.gnutar(args, cwd = dir.file).check
private val default_platform_families = List("linux", "windows", "macos")
@@ -44,60 +152,168 @@
rev: String = "",
afp_rev: String = "",
official_release: Boolean = false,
- release_name: String = "",
+ proper_release_name: Option[String] = None,
platform_families: List[String] = default_platform_families,
website: Option[Path] = None,
build_library: Boolean = false,
parallel_jobs: Int = 1,
remote_mac: String = ""): Release =
{
- /* release info */
-
- Isabelle_System.mkdirs(base_dir)
+ /* make distribution */
val release =
{
- 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(date, name, dist_dir, dist_archive, dist_library_archive, "")
- }
+ val release =
+ {
+ val date = Date.now()
+ val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
+ val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
+ Release(date, dist_name, dist_dir, "")
+ }
- val bundle_infos = platform_families.map(release.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.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.dist_archive)) {
- progress.echo("### Release archive already exists: " + release.dist_archive.implode)
- }
- else {
- progress.echo("Producing release archive " + release.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))
+ val release_ident =
+ if (release.isabelle_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.isabelle_archive)) {
+ progress.echo("### Release archive already exists: " + release.isabelle_archive.implode)
+ File.read(isabelle_ident_file)
+ }
+ else {
+ progress.echo("Producing release archive " + release.isabelle_archive.implode + " ...")
+
+ Isabelle_System.mkdirs(release.dist_dir)
+
+ val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
+ val version = proper_release_name orElse proper_string(rev) getOrElse "tip"
+ val ident =
+ try { hg.id(version) }
+ catch { case ERROR(_) => error("Bad repository version: " + quote(version)) }
+
+ val dist_version =
+ if (proper_release_name.isDefined) {
+ proper_release_name.get + ": " + Date.Format("LLLL uuuu")(release.date)
+ }
+ else "Isabelle repository snapshot " + ident + " " + Date.Format.date(release.date)
+
+ if (release.isabelle_dir.is_dir)
+ error("Directory " + release.isabelle_dir + " already exists")
+
+ isabelle_ident_file.file.delete
+ isabelle_dist_file.file.delete
+
+
+ progress.echo("### Retrieving Mercurial repository version " + quote(version))
+
+ try {
+ hg.archive(release.isabelle_dir.expand.implode, rev = ident, options = "--type files")
+ }
+ catch { case ERROR(_) => error("Failed to retrieve " + version + "(" + ident + ")") }
+
+ for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
+ (release.isabelle_dir + Path.explode(name)).file.delete
+ }
+
+
+ progress.echo("### Preparing distribution " + quote(release.dist_name))
+
+ patch_release(release.isabelle_dir, ident,
+ proper_release_name.isDefined && official_release, release.dist_name, dist_version)
+
+ if (proper_release_name.isEmpty) make_announce(release.isabelle_dir, ident)
+
+ make_contrib(release.isabelle_dir)
+
+ execute(release.isabelle_dir,
+ """find . "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f -x""")
+ execute(release.isabelle_dir,
+ """find . -print | xargs chmod -f u+rw""")
+
+
+ /* build tools and documentation */
+
+ val other_isabelle =
+ Other_Isabelle(release.isabelle_dir,
+ isabelle_identifier = release.other_isabelle_identifier,
+ progress = progress)
+
+ other_isabelle.init_settings(
+ (base_dir.absolute + Path.explode("contrib")).implode, nonfree = false, Nil)
+ other_isabelle.resolve_components(echo = true)
+
+ try {
+ val export_classpath =
+ "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
+ other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
+ other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
+ }
+ catch { case ERROR(_) => error("Failed to build tools") }
+
+ try {
+ other_isabelle.bash(
+ "./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check
+ }
+ catch { case ERROR(_) => error("Failed to build documentation") }
+
+ make_news(other_isabelle, dist_version)
+
+ for (name <- List("Admin", "browser_info", "heaps")) {
+ Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
+ }
+
+ other_isabelle.cleanup()
+
+
+ progress.echo("### Creating distribution archive " + release.isabelle_archive)
+
+ release.execute_dist_name(release.dist_dir, """
+set -e
+
+chmod -R a+r "$DIST_NAME"
+chmod -R u+w "$DIST_NAME"
+chmod -R g=o "$DIST_NAME"
+find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
+""")
+
+ execute_tar(release.dist_dir, "--owner=root --group=root -czf " +
+ File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
+
+ release.execute_dist_name(release.dist_dir, """
+set -e
+
+mv "$DIST_NAME" "${DIST_NAME}-old"
+mkdir "$DIST_NAME"
+
+mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
+ "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
+mkdir "$DIST_NAME/doc"
+mv "${DIST_NAME}-old/doc/"*.pdf \
+ "${DIST_NAME}-old/doc/"*.html \
+ "${DIST_NAME}-old/doc/"*.css \
+ "${DIST_NAME}-old/doc/fonts" \
+ "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
+
+rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
+
+rm -rf "${DIST_NAME}-old"
+""")
+
+ File.write(isabelle_dist_file, release.isabelle_archive.implode)
+ File.write(isabelle_ident_file, ident)
+ ident
+ }
+
+ release.copy(ident = release_ident)
}
/* make application bundles */
+ val bundle_infos = platform_families.map(release.bundle_info(_))
+
for (bundle_info <- bundle_infos) {
val bundle =
(if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main
@@ -108,7 +324,7 @@
progress.echo(
"\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive.implode)
progress.bash(
- "isabelle makedist_bundle " + File.bash_path(release.dist_archive) +
+ "isabelle makedist_bundle " + File.bash_path(release.isabelle_archive) +
" " + Bash.string(bundle_info.platform_family) +
(if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
echo = true).check
@@ -122,17 +338,16 @@
val website_platform_bundles =
for {
bundle_info <- bundle_infos
- bundle <-
- bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file)
+ bundle <- bundle_info.names.find(name => (release.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.name)),
+ List(HTML.title(release.dist_name)),
List(
- HTML.chapter(release.name + " (" + release_id + ")"),
+ HTML.chapter(release.dist_name + " (" + release.ident + ")"),
HTML.itemize(
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::
@@ -146,45 +361,40 @@
/* HTML library */
if (build_library) {
- if (release.dist_library_archive.is_file)
- progress.echo("### Library archive already exists: " +
- release.dist_library_archive.implode)
+ if (release.isabelle_library_archive.is_file) {
+ progress.echo(
+ "### Library archive already exists: " + release.isabelle_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.name
+ val name = release.dist_name
val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
val bundle = release.dist_dir + Path.explode(name + "_" + platform + ".tar.gz")
- execute_tar("xzf " + File.bash_path(bundle))
+ execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle =
Other_Isabelle(tmp_dir + Path.explode(name),
- isabelle_identifier = name + "-build", progress = progress)
+ isabelle_identifier = release.other_isabelle_identifier, progress = progress)
Isabelle_System.mkdirs(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
- other_isabelle.bash("bin/isabelle build" + jobs_option +
+ other_isabelle.bash("bin/isabelle build -j " + parallel_jobs +
" -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.dist_library_archive) +
+ execute(tmp_dir, "chmod -R a+r " + Bash.string(name))
+ execute(tmp_dir, "chmod -R g=o " + Bash.string(name))
+ execute_tar(tmp_dir, "--owner=root --group=root -czf " +
+ File.bash_path(release.isabelle_library_archive) +
" " + Bash.string(name + "/browser_info"))
})
}
}
-
- release.copy(id = release_id)
+ release
}
@@ -197,7 +407,7 @@
var afp_rev = ""
var remote_mac = ""
var official_release = false
- var release_name = ""
+ var proper_release_name: Option[String] = None
var website: Option[Path] = None
var parallel_jobs = 1
var build_library = false
@@ -223,7 +433,7 @@
"A:" -> (arg => afp_rev = arg),
"M:" -> (arg => remote_mac = arg),
"O" -> (_ => official_release = true),
- "R:" -> (arg => release_name = arg),
+ "R:" -> (arg => proper_release_name = Some(arg)),
"W:" -> (arg => website = Some(Path.explode(arg))),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library = true),
@@ -236,9 +446,11 @@
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,
+ official_release = official_release, proper_release_name = proper_release_name,
+ website = website,
platform_families =
- if (platform_families.isEmpty) default_platform_families else platform_families,
+ if (platform_families.isEmpty) default_platform_families
+ else platform_families,
build_library = build_library, parallel_jobs = parallel_jobs, remote_mac = remote_mac)
}
}