diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala +++ b/src/Pure/Admin/build_release.scala @@ -1,946 +1,942 @@ /* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { /** release context **/ private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check private def execute_tar(dir: Path, args: String, strip: Int = 0): Process_Result = Isabelle_System.gnutar(args, dir = dir, strip = strip).check private def bash_java_opens(args: String*): String = Bash.strings(args.toList.flatMap(arg => List("--add-opens", arg + "=ALL-UNNAMED"))) object Release_Context { def apply( target_dir: Path, release_name: String = "", components_base: Path = Components.default_components_base, progress: Progress = new Progress ): Release_Context = { val date = Date.now() val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute new Release_Context(release_name, dist_name, dist_dir, components_base, progress) } } class Release_Context private[Build_Release]( val release_name: String, val dist_name: String, val dist_dir: Path, val components_base: Path, val progress: Progress ) { override def toString: String = dist_name val isabelle: Path = Path.explode(dist_name) val isabelle_dir: Path = dist_dir + isabelle val isabelle_archive: Path = dist_dir + isabelle.tar.gz val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") def other_isabelle(dir: Path): Other_Isabelle = Other_Isabelle(dir + isabelle, isabelle_identifier = dist_name + "-build", progress = progress) def make_announce(id: String): Unit = { if (release_name.isEmpty) { File.write(isabelle_dir + Path.explode("ANNOUNCE"), """ IMPORTANT NOTE ============== This is a snapshot of Isabelle/""" + id + """ from the repository. """) } } def make_contrib(): Unit = { Isabelle_System.make_directory(Components.contrib(isabelle_dir)) File.write(Components.contrib(isabelle_dir, name = "README"), """This directory contains add-on components that contribute to the main Isabelle distribution. Separate licensing conditions apply, see each directory individually. """) } def bundle_info(platform: Platform.Family.Value): Bundle_Info = platform match { case Platform.Family.linux_arm => Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz") case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz") case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") } } sealed case class Bundle_Info( platform: Platform.Family.Value, platform_description: String, name: String ) { def path: Path = Path.explode(name) } /** release archive **/ val ISABELLE: Path = Path.basic("Isabelle") val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID") val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS") val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER") object Release_Archive { def make(bytes: Bytes, rename: String = ""): Release_Archive = { Isabelle_System.with_tmp_dir("build_release")(dir => Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path => val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE) Bytes.write(archive_path, bytes) execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1) val id = File.read(isabelle_dir + ISABELLE_ID) val tags = File.read(isabelle_dir + ISABELLE_TAGS) val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER) val (bytes1, identifier1) = if (rename.isEmpty || rename == identifier) (bytes, identifier) else { File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename) Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename)) execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename)) (Bytes.read(archive_path), rename) } new Release_Archive(bytes1, id, tags, identifier1) } ) } def read(path: Path, rename: String = ""): Release_Archive = make(Bytes.read(path), rename = rename) def get( url: String, rename: String = "", progress: Progress = new Progress ): Release_Archive = { val bytes = if (Path.is_wellformed(url)) Bytes.read(Path.explode(url)) else Isabelle_System.download(url, progress = progress).bytes make(bytes, rename = rename) } } case class Release_Archive private[Build_Release]( bytes: Bytes, id: String, tags: String, identifier: String) { override def toString: String = identifier } /** generated content **/ /* bundled components */ class Bundled(platform: Option[Platform.Family.Value] = None) { def detect(s: String): Boolean = s.startsWith("#bundled") && !s.startsWith("#bundled ") def apply(name: String): String = "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name private val Pattern1 = ("""^#bundled:(.*)$""").r private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r def unapply(s: String): Option[String] = s match { case Pattern1(name) => Some(name) case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name) case _ => None } } def record_bundled_components(dir: Path): Unit = { val catalogs = List("main", "bundled").map((_, new Bundled())) ::: Platform.Family.list.flatMap(platform => List(platform.toString, "bundled-" + platform.toString). map((_, new Bundled(platform = Some(platform))))) File.append(Components.components(dir), terminate_lines("#bundled components" :: (for { (catalog, bundled) <- catalogs.iterator path = Components.admin(dir) + Path.basic(catalog) if path.is_file line <- split_lines(File.read(path)) if line.nonEmpty && !line.startsWith("#") } yield bundled(line)).toList)) } def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = { val Bundled = new Bundled(platform = Some(platform)) val components = for { Bundled(name) <- Components.read_components(dir) } yield name val jdk_component = components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") (components, jdk_component) } def activate_components( dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit = { def contrib_name(name: String): String = Components.contrib(name = name).implode val Bundled = new Bundled(platform = Some(platform)) Components.write_components(dir, Components.read_components(dir).flatMap(line => line match { case Bundled(name) => if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) else None case _ => if (Bundled.detect(line)) None else Some(line) }) ::: more_names.map(contrib_name)) } /** build release **/ /* build heaps */ private def build_heaps( options: Options, platform: Platform.Family.Value, build_sessions: List[String], local_dir: Path, progress: Progress = new Progress, ): Unit = { val server_option = "build_host_" + platform.toString val server = options.string(server_option) progress.echo("Building heaps for " + commas_quote(build_sessions) + " (" + server_option + " = " + quote(server) + ") ...") val ssh = - server match { - case "" => - if (Platform.family == platform) SSH.Local - else error("Undefined option " + server_option + ": cannot build heaps") - case SSH.Target(user, host) => - SSH.open_session(options, host = host, user = user) - case _ => error("Malformed option " + server_option + ": " + quote(server)) - } + if (server.nonEmpty) SSH.open_session(options, server) + else if (Platform.family == platform) SSH.Local + else error("Undefined option " + server_option + ": cannot build heaps") + try { Isabelle_System.with_tmp_file("tmp", ext = "tar") { local_tmp_tar => execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") ssh.with_tmp_dir { remote_dir => val remote_tmp_tar = remote_dir + Path.basic("tmp.tar") ssh.write_file(remote_tmp_tar, local_tmp_tar) val build_command = "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions) val build_script = List( "cd " + File.bash_path(remote_dir), "tar -xf tmp.tar", build_command, """perl -pi -e "s/ISABELLE_APPLE_PLATFORM64/ISABELLE_WINDOWS_PLATFORM64/g;" "$(bin/isabelle getenv -b POLYML_HOME)/etc/settings" """, build_command, "tar -cf tmp.tar heaps") ssh.execute(build_script.mkString(" && "), settings = false).check ssh.read_file(remote_tmp_tar, local_tmp_tar) } execute_tar(local_dir, "-xvf " + File.bash_path(local_tmp_tar)) .out_lines.sorted.foreach(progress.echo) } } finally { ssh.close() } } /* Isabelle application */ def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit = { val title = "# Java runtime options" File.write(path, (title :: options).map(_ + line_ending).mkString) } def make_isabelle_app( platform: Platform.Family.Value, isabelle_target: Path, isabelle_name: String, jdk_component: String, classpath: List[Path], dock_icon: Boolean = false): Unit = { val script = """#!/usr/bin/env bash # # Author: Makarius # # Main Isabelle application script. # minimal Isabelle environment ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)" source "$ISABELLE_HOME/lib/scripts/isabelle-platform" #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """" source "$COMPONENT/etc/settings" # main declare -a JAVA_OPTIONS=($(grep -v '^#' "$ISABELLE_HOME/Isabelle.options")) "$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup" exec "$ISABELLE_JDK_HOME/bin/java" \ "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ -classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \ "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \ """ + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \ """ else "") + """isabelle.jedit.JEdit_Main "$@" """ val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app") File.write(script_path, script) File.set_executable(script_path, true) val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app") Isabelle_System.move_file( component_dir + Path.explode(Platform.Family.standard(platform)) + Path.explode("Isabelle"), isabelle_target + Path.explode(isabelle_name)) Isabelle_System.rm_tree(component_dir) } def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit = { File.write(path, """ CFBundleDevelopmentRegion English CFBundleIconFile isabelle.icns CFBundleIdentifier de.tum.in.isabelle CFBundleDisplayName """ + isabelle_name + """ CFBundleInfoDictionaryVersion 6.0 CFBundleName """ + isabelle_name + """ CFBundlePackageType APPL CFBundleShortVersionString """ + isabelle_name + """ CFBundleSignature ???? CFBundleVersion """ + isabelle_rev + """ NSHumanReadableCopyright LSMinimumSystemVersion 10.11 LSApplicationCategoryType public.app-category.developer-tools NSHighResolutionCapable true NSSupportsAutomaticGraphicsSwitching true CFBundleDocumentTypes CFBundleTypeExtensions thy CFBundleTypeIconFile theory.icns CFBundleTypeName Isabelle theory file CFBundleTypeRole Editor LSTypeIsPackage """) } /* main */ def use_release_archive( context: Release_Context, archive: Release_Archive, id: String = "" ): Unit = { if (id.nonEmpty && id != archive.id) { error("Mismatch of release identification " + id + " vs. archive " + archive.id) } if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) { Bytes.write(context.isabelle_archive, archive.bytes) } } def build_release_archive( context: Release_Context, version: String, parallel_jobs: Int = 1 ): Unit = { val progress = context.progress val hg = Mercurial.self_repository() val id = try { hg.id(version) } catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } if (context.isabelle_archive.is_file) { progress.echo_warning("Found existing release archive: " + context.isabelle_archive) use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id) } else { progress.echo_warning("Preparing release " + context.dist_name + " ...") Isabelle_System.new_directory(context.dist_dir) hg.archive(context.isabelle_dir.expand.implode, rev = id) for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { (context.isabelle_dir + Path.explode(name)).file.delete } File.write(context.isabelle_dir + ISABELLE_ID, id) File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id)) File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name) context.make_announce(id) context.make_contrib() execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""") record_bundled_components(context.isabelle_dir) /* build tools and documentation */ val other_isabelle = context.other_isabelle(context.dist_dir) other_isabelle.init_settings( other_isabelle.init_components( components_base = context.components_base, catalogs = List("main"))) other_isabelle.resolve_components(echo = true) try { other_isabelle.bash( "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" + "bin/isabelle jedit -b", echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) } try { other_isabelle.bash( "bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) } other_isabelle.make_news() for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) } other_isabelle.cleanup() progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...") execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""") execute(context.dist_dir, """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""") execute_tar(context.dist_dir, "-czf " + File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name)) } } def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0 def build_release( options: Options, context: Release_Context, afp_rev: String = "", platform_families: List[Platform.Family.Value] = default_platform_families, more_components: List[Path] = Nil, website: Option[Path] = None, build_sessions: List[String] = Nil, build_library: Boolean = false, parallel_jobs: Int = 1 ): Unit = { val progress = context.progress /* release directory */ val archive = Release_Archive.read(context.isabelle_archive) for (path <- List(context.isabelle, ISABELLE)) { Isabelle_System.rm_tree(context.dist_dir + path) } Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path => Bytes.write(archive_path, archive.bytes) val extract = List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc"). map(name => context.dist_name + "/" + name) execute_tar(context.dist_dir, "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract)) } Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE) /* make application bundles */ val bundle_infos = platform_families.map(context.bundle_info) for (bundle_info <- bundle_infos) { val isabelle_name = context.dist_name val platform = bundle_info.platform progress.echo("\nApplication bundle for " + platform) Isabelle_System.with_tmp_dir("build_release") { tmp_dir => // release archive execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive)) val other_isabelle = context.other_isabelle(tmp_dir) val isabelle_target = other_isabelle.isabelle_home // bundled components progress.echo("Bundled components:") val contrib_dir = Components.contrib(isabelle_target) val (bundled_components, jdk_component) = get_bundled_components(isabelle_target, platform) Components.resolve(context.components_base, bundled_components, target_dir = Some(contrib_dir), copy_dir = Some(context.dist_dir + Path.explode("contrib")), progress = progress) val more_components_names = more_components.map(Components.unpack(contrib_dir, _, progress = progress)) activate_components(isabelle_target, platform, more_components_names) // Java parameters val java_options: List[String] = (for { variable <- List( "ISABELLE_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_OPTIONS") opt <- Word.explode(other_isabelle.getenv(variable)) } yield { val s = "-Dapple.awt.application.name=" if (opt.startsWith(s)) s + isabelle_name else opt }) ::: List("-Disabelle.jedit_server=" + isabelle_name) val classpath: List[Path] = { val base = isabelle_target.absolute val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")) val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH")) (classpath1 ::: classpath2).map { path => val abs_path = path.absolute File.relative_path(base, abs_path) match { case Some(rel_path) => rel_path case None => error("Bad classpath element: " + abs_path) } } } val jedit_options = Path.explode("src/Tools/jEdit/etc/options") val jedit_props = Path.explode(other_isabelle.getenv("JEDIT_HOME") + "/properties/jEdit.props") // build heaps if (build_sessions.nonEmpty) { build_heaps(options, platform, build_sessions, isabelle_target, progress = progress) } // application bundling Components.purge(contrib_dir, platform) platform match { case Platform.Family.linux_arm | Platform.Family.linux => File.change(isabelle_target + jedit_options) { _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24") } File.change(isabelle_target + jedit_props) { _.replaceAll("console.fontsize=.*", "console.fontsize=18") .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") .replaceAll("view.fontsize=.*", "view.fontsize=24") .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16") } make_isabelle_options( isabelle_target + Path.explode("Isabelle.options"), java_options) make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath) progress.echo("Packaging " + bundle_info.name + " ...") execute_tar(tmp_dir, "-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " + Bash.string(isabelle_name)) case Platform.Family.macos => File.change(isabelle_target + jedit_props) { _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d") } // macOS application bundle val app_contents = isabelle_target + Path.explode("Contents") for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) { Isabelle_System.copy_file(isabelle_target + Path.explode(icon), Isabelle_System.make_directory(app_contents + Path.explode("Resources"))) } make_isabelle_plist( app_contents + Path.explode("Info.plist"), isabelle_name, archive.id) make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath, dock_icon = true) val isabelle_options = Path.explode("Isabelle.options") make_isabelle_options( isabelle_target + isabelle_options, java_options ::: List("-Disabelle.app=true")) // application archive progress.echo("Packaging " + bundle_info.name + " ...") val isabelle_app = Path.explode(isabelle_name + ".app") Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name), tmp_dir + isabelle_app) execute_tar(tmp_dir, "-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " + File.bash_path(isabelle_app)) case Platform.Family.windows => File.change(isabelle_target + jedit_props) { _.replaceAll("foldPainter=.*", "foldPainter=Square") } // application launcher Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) val app_template = Path.explode("~~/Admin/Windows/launch4j") make_isabelle_options( isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), java_options, line_ending = "\r\n") val isabelle_xml = Path.explode("isabelle.xml") val isabelle_exe = bundle_info.path File.write(tmp_dir + isabelle_xml, File.read(app_template + isabelle_xml) .replace("{ISABELLE_NAME}", isabelle_name) .replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe)) .replace("{ICON}", File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) .replace("{SPLASH}", File.platform_path(app_template + Path.explode("isabelle.bmp"))) .replace("{CLASSPATH}", cat_lines(classpath.map(cp => " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) .replace("\\jdk\\", "\\" + jdk_component + "\\")) val java_opts = bash_java_opens( "java.base/java.io", "java.base/java.lang", "java.base/java.lang.reflect", "java.base/java.text", "java.base/java.util", "java.desktop/java.awt.font") val launch4j_jar = Path.explode("windows_app/launch4j-" + Platform.family + "/launch4j.jar") execute(tmp_dir, cat_lines(List( "export LAUNCH4J=" + File.bash_platform_path(launch4j_jar), "isabelle java " + java_opts + " -jar \"$LAUNCH4J\" isabelle.xml"))) Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"), isabelle_target + isabelle_exe.ext("manifest")) // Cygwin setup val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) val cygwin_mirror = File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) val cygwin_bat = Path.explode("Cygwin-Setup.bat") File.write(isabelle_target + cygwin_bat, File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror)) File.set_executable(isabelle_target + cygwin_bat, true) for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { val path = Path.explode(name) Isabelle_System.copy_file(cygwin_template + path, isabelle_target + Path.explode("contrib/cygwin") + path) } execute(isabelle_target, """find . -type f -not -name "*.exe" -not -name "*.dll" """ + (if (Platform.is_macos) "-perm +100" else "-executable") + " -print0 > contrib/cygwin/isabelle/executables") execute(isabelle_target, """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + """> contrib/cygwin/isabelle/symlinks""") execute(isabelle_target, """find . -type l -exec rm "{}" ";" """) File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") // executable archive (self-extracting 7z) val archive_name = isabelle_name + ".7z" val exe_archive = tmp_dir + Path.explode(archive_name) exe_archive.file.delete progress.echo("Packaging " + archive_name + " ...") execute(tmp_dir, "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name)) if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive) val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx") val sfx_txt = File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")) .replace("{ISABELLE_NAME}", isabelle_name) Bytes.write(context.dist_dir + isabelle_exe, Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive)) File.set_executable(context.dist_dir + isabelle_exe, true) } } progress.echo("DONE") } /* minimal website */ for (dir <- website) { val website_platform_bundles = for { bundle_info <- bundle_infos if (context.dist_dir + bundle_info.path).is_file } yield (bundle_info.name, bundle_info) val isabelle_link = HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id), HTML.text("Isabelle/" + archive.id)) val afp_link = HTML.link(Isabelle_System.afp_repository.changeset(afp_rev), HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(context.dist_name)), List( HTML.section(context.dist_name), HTML.subsection("Downloads"), HTML.itemize( List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) :: website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })), HTML.subsection("Repositories"), HTML.itemize( List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link)))))) Isabelle_System.copy_file(context.isabelle_archive, dir) for ((bundle, _) <- website_platform_bundles) { Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir) } } /* HTML library */ if (build_library) { if (context.isabelle_library_archive.is_file) { progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive) } else { Isabelle_System.with_tmp_dir("build_release") { tmp_dir => val bundle = context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz") execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) val other_isabelle = context.other_isabelle(tmp_dir) Isabelle_System.make_directory(other_isabelle.etc) File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\n") other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name)) execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name)) execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) + " " + Bash.string(context.dist_name + "/browser_info")) } } } } /** command line entry point **/ def main(args: Array[String]): Unit = { Command_Line.tool { var afp_rev = "" var components_base: Path = Components.default_components_base var target_dir = Path.current var release_name = "" var source_archive = "" var website: Option[Path] = None var build_sessions: List[String] = Nil var more_components: List[Path] = Nil var parallel_jobs = 1 var build_library = false var options = Options.init() var platform_families = default_platform_families var rev = "" val getopts = Getopts(""" Usage: Admin/build_release [OPTIONS] Options are: -A REV corresponding AFP changeset id -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) -D DIR target directory (default ".") -R RELEASE explicit release name -S ARCHIVE use existing source archive (file or URL) -W WEBSITE produce minimal website in given directory -b SESSIONS build platform-specific session images (separated by commas) -c ARCHIVE clean bundling with additional component .tar.gz archive -j INT maximum number of parallel jobs (default 1) -l build library -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip) Build Isabelle release in base directory, using the local repository clone. """, "A:" -> (arg => afp_rev = arg), "C:" -> (arg => components_base = Path.explode(arg)), "D:" -> (arg => target_dir = Path.explode(arg)), "R:" -> (arg => release_name = arg), "S:" -> (arg => source_archive = arg), "W:" -> (arg => website = Some(Path.explode(arg))), "b:" -> (arg => build_sessions = space_explode(',', arg)), "c:" -> (arg => { val path = Path.explode(arg) Components.Archive.get_name(path.file_name) more_components = more_components ::: List(path) }), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), "r:" -> (arg => rev = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) error("Building for windows requires 7z") val progress = new Console_Progress() def make_context(name: String): Release_Context = Release_Context(target_dir, release_name = name, components_base = components_base, progress = progress) val context = if (source_archive.isEmpty) { val context = make_context(release_name) val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip" build_release_archive(context, version, parallel_jobs = parallel_jobs) context } else { val archive = Release_Archive.get(source_archive, rename = release_name, progress = progress) val context = make_context(archive.identifier) Isabelle_System.make_directory(context.dist_dir) use_release_archive(context, archive, id = rev) context } build_release(options, context, afp_rev = afp_rev, platform_families = platform_families, more_components = more_components, build_sessions = build_sessions, build_library = build_library, parallel_jobs = parallel_jobs, website = website) } } } diff --git a/src/Pure/General/mercurial.scala b/src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala +++ b/src/Pure/General/mercurial.scala @@ -1,621 +1,619 @@ /* Title: Pure/General/mercurial.scala Author: Makarius Support for Mercurial repositories, with local or remote repository clone and working directory (via ssh connection). */ package isabelle import scala.annotation.tailrec import scala.collection.mutable object Mercurial { type Graph = isabelle.Graph[String, Unit] /** HTTP server **/ object Server { def apply(root: String): Server = new Server(root) def start(root: Path): Server = { val hg = repository(root) val server_process = Future.promise[Bash.Process] val server_root = Future.promise[String] Isabelle_Thread.fork("hg") { val process = Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) } server_process.fulfill_result(process) Exn.release(process).result(progress_stdout = line => if (!server_root.is_finished) { server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line)) }) } server_process.join new Server(server_root.join) { override def close(): Unit = server_process.join.terminate() } } } class Server private(val root: String) extends AutoCloseable { override def toString: String = root def close(): Unit = () def changeset(rev: String = "tip", raw: Boolean = false): String = root + (if (raw) "/raw-rev/" else "/rev/") + rev def file(path: Path, rev: String = "tip", raw: Boolean = false): String = root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode def archive(rev: String = "tip"): String = root + "/archive/" + rev + ".tar.gz" def read_changeset(rev: String = "tip"): String = Url.read(changeset(rev = rev, raw = true)) def read_file(path: Path, rev: String = "tip"): String = Url.read(file(path, rev = rev, raw = true)) def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content = Isabelle_System.download(archive(rev = rev), progress = progress) def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit = { Isabelle_System.new_directory(dir) Isabelle_System.with_tmp_file("rev", ext = ".tar.gz") { archive_path => val content = download_archive(rev = rev, progress = progress) Bytes.write(archive_path, content.bytes) progress.echo("Unpacking " + rev + ".tar.gz") Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path), dir = dir, original_owner = true, strip = 1).check } } } /** repository commands **/ /* command-line syntax */ def optional(s: String, prefix: String = ""): String = if (s == "") "" else " " + prefix + " " + Bash.string(s) def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else "" def opt_rev(s: String): String = optional(s, "--rev") def opt_template(s: String): String = optional(s, "--template") /* repository archives */ private val Archive_Node = """^node: (\S{12}).*$""".r private val Archive_Tag = """^tag: (\S+).*$""".r sealed case class Archive_Info(lines: List[String]) { def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a }) def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag } def archive_info(root: Path): Option[Archive_Info] = { val path = root + Path.explode(".hg_archival.txt") if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None } def archive_id(root: Path): Option[String] = archive_info(root).flatMap(_.id) def archive_tags(root: Path): Option[String] = archive_info(root).map(info => info.tags.mkString(" ")) /* hg_sync meta data */ object Hg_Sync { val NAME = ".hg_sync" val _NAME: String = " " + NAME val PATH: Path = Path.explode(NAME) val PATH_ID: Path = PATH + Path.explode("id") val PATH_LOG: Path = PATH + Path.explode("log") val PATH_DIFF: Path = PATH + Path.explode("diff") val PATH_STAT: Path = PATH + Path.explode("stat") def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + PATH) def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = { if (is_directory(root, ssh = ssh)) new Directory(root, ssh) else error("No .hg_sync directory found in " + ssh.rsync_path(root)) } class Directory private [Hg_Sync](val root: Path, val ssh: SSH.System) { override def toString: String = ssh.rsync_path(root) def read(path: Path): String = ssh.read(root + path) lazy val id: String = read(PATH_ID) lazy val log: String = read(PATH_LOG) lazy val diff: String = read(PATH_DIFF) lazy val stat: String = read(PATH_STAT) def changed: Boolean = id.endsWith("+") } } /* repository access */ def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + Path.explode(".hg")) && new Repository(root, ssh).command("root").ok def id_repository(root: Path, ssh: SSH.System = SSH.Local, rev: String = "tip"): Option[String] = if (is_repository(root, ssh = ssh)) Some(repository(root, ssh = ssh).id(rev = rev)) else None def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = { val hg = new Repository(root, ssh) hg.command("root").check hg } def self_repository(): Repository = repository(Path.ISABELLE_HOME) def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = { @tailrec def find(root: Path): Option[Repository] = if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) else if (root.is_root) None else find(root + Path.parent) find(ssh.expand_path(start)) } def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository = find_repository(start, ssh = ssh) getOrElse error("No repository found in " + start.absolute) private def make_repository( root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local ) : Repository = { val hg = new Repository(root, ssh) ssh.make_directory(hg.root.dir) hg.command(cmd, args, repository = false).check hg } def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository = make_repository(root, "init", ssh.bash_path(root), ssh = ssh) def clone_repository(source: String, root: Path, rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository = make_repository(root, "clone", options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh) def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = { if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } else clone_repository(source, root, options = "--noupdate", ssh = ssh) } class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) { hg => val root: Path = ssh.expand_path(root_path) def root_url: String = ssh.hg_url + root.implode override def toString: String = ssh.hg_url + root.implode def command_line( name: String, args: String = "", options: String = "", repository: Boolean = true ): String = { "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + (if (repository) " --repository " + ssh.bash_path(root) else "") + " --noninteractive " + name + " " + options + " " + args } def command( name: String, args: String = "", options: String = "", repository: Boolean = true ): Process_Result = { ssh.execute(command_line(name, args = args, options = options, repository = repository)) } def add(files: List[Path]): Unit = hg.command("add", files.map(ssh.bash_path).mkString(" ")) def archive(target: String, rev: String = "", options: String = ""): Unit = hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check def heads(template: String = "{node|short}\n", options: String = ""): List[String] = hg.command("heads", opt_template(template), options).check.out_lines def identify(rev: String = "tip", options: String = ""): String = hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" def id(rev: String = "tip"): String = identify(rev, options = "-i") def tags(rev: String = "tip"): String = { val result = identify(rev, options = "-t") Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ") } def paths(args: String = "", options: String = ""): List[String] = hg.command("paths", args = args, options = options).check.out_lines def manifest(rev: String = "", options: String = ""): List[String] = hg.command("manifest", opt_rev(rev), options).check.out_lines def log(rev: String = "", template: String = "", options: String = ""): String = hg.command("log", opt_rev(rev) + opt_template(template), options).check.out def diff(rev: String = "", options: String = ""): String = hg.command("diff", opt_rev(rev), options).check.out def parent(): String = log(rev = "p1()", template = "{node|short}") def push( remote: String = "", rev: String = "", force: Boolean = false, options: String = "" ): Unit = { hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options). check_rc(rc => rc == 0 | rc == 1) } def pull(remote: String = "", rev: String = "", options: String = ""): Unit = hg.command("pull", opt_rev(rev) + optional(remote), options).check def update( rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "" ): Unit = { hg.command("update", opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check } def status(options: String = ""): List[String] = hg.command("status", options = options).check.out_lines def known_files(): List[String] = status(options = "--modified --added --clean --no-status") def sync(context: Rsync.Context, target: String, verbose: Boolean = false, thorough: Boolean = false, dry_run: Boolean = false, filter: List[String] = Nil, contents: List[File.Content] = Nil, rev: String = "" ): Unit = { require(ssh == SSH.Local, "local repository required") Isabelle_System.with_tmp_dir("sync") { tmp_dir => val context0 = context.copy(progress = new Progress) Rsync.init(context0, target) val list = Rsync.exec(context0, list = true, args = List("--", Rsync.terminate(target))) .check.out_lines.filterNot(_.endsWith(" .")) if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { error("No .hg_sync meta data in " + quote(target)) } val id_content = id(rev = rev) val is_changed = id_content.endsWith("+") val log_content = if (is_changed) "" else log(rev = rev, options = "-l1") val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" Rsync.init(context0, target, contents = File.content(Hg_Sync.PATH_ID, id_content) :: File.content(Hg_Sync.PATH_LOG, log_content) :: File.content(Hg_Sync.PATH_DIFF, diff_content) :: File.content(Hg_Sync.PATH_STAT, stat_content) :: contents) val (exclude, source) = if (rev.isEmpty) { val exclude = ".hg" :: status(options = "--unknown --ignored --no-status") val source = File.standard_path(root) (exclude, source) } else { val exclude = List(".hg_archival.txt") val source = File.standard_path(tmp_dir + Path.explode("archive")) archive(source, rev = rev) (exclude, source) } val exclude_path = tmp_dir + Path.explode("exclude") File.write(exclude_path, cat_lines(exclude.map("/" + _))) val protect = (Hg_Sync.PATH :: contents.map(_.path)) .map(path => "protect /" + File.standard_path(path)) Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run, clean = true, prune_empty_dirs = true, filter = protect ::: filter, args = List("--exclude-from=" + exclude_path.implode, "--", Rsync.terminate(source), target) ).check } } def graph(): Graph = { val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r val log_result = log(template = """node: {node|short} {p1node|short} {p2node|short}\n""") split_lines(log_result).foldLeft(Graph.string[Unit]) { case (graph, Node(x, y, z)) => val deps = List(y, z).filterNot(s => s.forall(_ == '0')) val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ())) deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) }) case (graph, _) => graph } } } /** check files **/ def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = { val outside = new mutable.ListBuffer[Path] val unknown = new mutable.ListBuffer[Path] @tailrec def check(paths: List[Path]): Unit = { paths match { case path :: rest => find_repository(path, ssh) match { case None => outside += path; check(rest) case Some(hg) => val known = hg.known_files().iterator.map(name => (hg.root + Path.explode(name)).canonical_file).toSet if (!known(path.canonical_file)) unknown += path check(rest.filterNot(p => known(p.canonical_file))) } case Nil => } } check(files) (outside.toList, unknown.toList) } /** hg_setup **/ private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = { val hgrc = local_hg.root + Path.explode(".hg/hgrc") def header(line: String): Boolean = line.startsWith("[paths]") val Entry = """^(\S+)\s*=\s*(.*)$""".r val new_entry = path_name + " = " + source def commit(lines: List[String]): Boolean = { File.write(hgrc, cat_lines(lines)) true } val edited = hgrc.is_file && { val lines = split_lines(File.read(hgrc)) lines.count(header) == 1 && { if (local_hg.paths(options = "-q").contains(path_name)) { val old_source = local_hg.paths(args = path_name).head val old_entry = path_name + ".old = " + old_source val lines1 = lines.map { case Entry(a, b) if a == path_name && b == old_source => new_entry + "\n" + old_entry case line => line } lines != lines1 && commit(lines1) } else { val prefix = lines.takeWhile(line => !header(line)) val n = prefix.length commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1)) } } } if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n") } val default_path_name = "default" def hg_setup( remote: String, local_path: Path, remote_name: String = "", path_name: String = default_path_name, remote_exists: Boolean = false, progress: Progress = new Progress ): Unit = { /* local repository */ Isabelle_System.make_directory(local_path) val repos_name = proper_string(remote_name) getOrElse local_path.absolute.base.implode val local_hg = if (is_repository(local_path)) repository(local_path) else init_repository(local_path) progress.echo("Local repository " + local_hg.root.absolute) /* remote repository */ - val remote_url = - remote match { - case _ if remote.startsWith("ssh://") => - val ssh_url = remote + "/" + repos_name + val remote_url = { + if (remote.startsWith("ssh://")) { + val ssh_url = remote + "/" + repos_name - if (!remote_exists) { - try { local_hg.command("init", ssh_url, repository = false).check } - catch { case ERROR(msg) => progress.echo_warning(msg) } + if (!remote_exists) { + try { local_hg.command("init", ssh_url, repository = false).check } + catch { case ERROR(msg) => progress.echo_warning(msg) } + } + + ssh_url + } + else { + val phabricator = Phabricator.API(remote) + + var repos = + phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { + if (remote_exists) { + error("Remote repository " + + quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") + } + else phabricator.create_repository(repos_name, short_name = repos_name) } - ssh_url - - case SSH.Target(user, host) => - val phabricator = Phabricator.API(user, host) + while (repos.importing) { + progress.echo("Awaiting remote repository ...") + Time.seconds(0.5).sleep() + repos = phabricator.the_repository(repos.phid) + } - var repos = - phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { - if (remote_exists) { - error("Remote repository " + - quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") - } - else phabricator.create_repository(repos_name, short_name = repos_name) - } - - while (repos.importing) { - progress.echo("Awaiting remote repository ...") - Time.seconds(0.5).sleep() - repos = phabricator.the_repository(repos.phid) - } - - repos.ssh_url - - case _ => error("Malformed remote specification " + quote(remote)) + repos.ssh_url } + } progress.echo("Remote repository " + quote(remote_url)) /* synchronize local and remote state */ progress.echo("Synchronizing ...") edit_hgrc(local_hg, path_name, remote_url) local_hg.pull(options = "-u") local_hg.push(remote = remote_url) } val isabelle_tool1 = Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", Scala_Project.here, { args => var remote_name = "" var path_name = default_path_name var remote_exists = false val getopts = Getopts(""" Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR Options are: -n NAME remote repository name (default: base name of LOCAL_DIR) -p PATH Mercurial path name (default: """ + quote(default_path_name) + """) -r assume that remote repository already exists Setup a remote vs. local Mercurial repository: REMOTE either refers to a Phabricator server "user@host" or SSH file server "ssh://user@host/path". """, "n:" -> (arg => remote_name = arg), "p:" -> (arg => path_name = arg), "r" -> (_ => remote_exists = true)) val more_args = getopts(args) val (remote, local_path) = more_args match { case List(arg1, arg2) => (arg1, Path.explode(arg2)) case _ => getopts.usage() } val progress = new Console_Progress hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name, remote_exists = remote_exists, progress = progress) }) /** hg_sync **/ val isabelle_tool2 = Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory", Scala_Project.here, { args => var filter: List[String] = Nil var protect_args = false var root: Option[Path] = None var ssh_control_path = "" var thorough = false var dry_run = false var ssh_port = 0 var rev = "" var verbose = false val getopts = Getopts(""" Usage: isabelle hg_sync [OPTIONS] TARGET Options are: -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion) -P protect spaces in target file names: more robust, less portable -R ROOT explicit repository root directory (default: implicit from current directory) -S PATH SSH control path for connection multiplexing -T thorough treatment of file content and directory times -n no changes: dry-run -p PORT SSH port -r REV explicit revision (default: state of working directory) -v verbose Synchronize Mercurial repository with TARGET directory, which can be local or remote (using notation of rsync). """, "F:" -> (arg => filter = filter ::: List(arg)), "P" -> (_ => protect_args = true), "R:" -> (arg => root = Some(Path.explode(arg))), "S:" -> (arg => ssh_control_path = arg), "T" -> (_ => thorough = true), "n" -> (_ => dry_run = true), "p:" -> (arg => ssh_port = Value.Int.parse(arg)), "r:" -> (arg => rev = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) val target = more_args match { case List(target) => target case _ => getopts.usage() } val progress = new Console_Progress val hg = root match { case Some(dir) => repository(dir) case None => the_repository(Path.current) } val context = Rsync.Context(progress, ssh_port = ssh_port, ssh_control_path = ssh_control_path, protect_args = protect_args) hg.sync(context, target, verbose = verbose, thorough = thorough, dry_run = dry_run, filter = filter, rev = rev) } ) } diff --git a/src/Pure/General/ssh.scala b/src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala +++ b/src/Pure/General/ssh.scala @@ -1,367 +1,351 @@ /* Title: Pure/General/ssh.scala Author: Makarius SSH client on OpenSSH command-line tools, preferably with connection multiplexing, but this does not work on Windows. */ package isabelle import java.util.{Map => JMap} import java.io.{File => JFile} object SSH { - /* target machine: user@host syntax */ - - object Target { - def parse(s: String): (String, String) = { - val i = s.indexOf('@') - if (i <= 0) ("", s) - else (s.substring(0, i), s.substring(i + 1)) - } - - def unapplySeq(s: String): Option[List[String]] = { - val (user, host) = parse(s) - if (host.isEmpty) None else Some(List(user, host)) - } - } - - /* OpenSSH configuration and command-line */ // see https://linux.die.net/man/5/ssh_config object Config { def entry(x: String, y: String): String = x + "=" + y def entry(x: String, y: Int): String = entry(x, y.toString) def entry(x: String, y: Long): String = entry(x, y.toString) def entry(x: String, y: Boolean): String = entry(x, if (y) "yes" else "no") def make(options: Options, port: Int = 0, user: String = "", control_master: Boolean = false, control_path: String = "" ): List[String] = { val ssh_batch_mode = options.bool("ssh_batch_mode") val ssh_compression = options.bool("ssh_compression") val ssh_alive_interval = options.real("ssh_alive_interval").round val ssh_alive_count_max = options.int("ssh_alive_count_max") List( entry("BatchMode", ssh_batch_mode), entry("Compression", ssh_compression)) ::: (if (ssh_alive_interval >= 0) List(entry("ServerAliveInterval", ssh_alive_interval)) else Nil) ::: (if (ssh_alive_count_max >= 0) List(entry("ServerAliveCountMax", ssh_alive_count_max)) else Nil) ::: (if (port > 0) List(entry("Port", port)) else Nil) ::: (if (user.nonEmpty) List(entry("User", user)) else Nil) ::: (if (control_master) List("ControlMaster=yes", "ControlPersist=yes") else Nil) ::: (if (control_path.nonEmpty) List("ControlPath=" + control_path) else Nil) } def option(entry: String): String = "-o " + Bash.string(entry) def option(x: String, y: String): String = option(entry(x, y)) def option(x: String, y: Int): String = option(entry(x, y)) def option(x: String, y: Long): String = option(entry(x, y)) def option(x: String, y: Boolean): String = option(entry(x, y)) def command(command: String, config: List[String]): String = Bash.string(command) + config.map(entry => " " + option(entry)).mkString } def sftp_string(str: String): String = { val special = "[]?*\\{} \"'" if (str.isEmpty) "\"\"" else if (str.exists(special.contains)) { val res = new StringBuilder for (c <- str) { if (special.contains(c)) res += '\\' res += c } res.toString() } else str } /* open session */ def open_session( options: Options, host: String, port: Int = 0, user: String = "" ): Session = { val multiplex = options.bool("ssh_multiplexing") && !Platform.is_windows val (control_master, control_path) = if (multiplex) (true, Isabelle_System.tmp_file("ssh", initialized = false).getPath) else (false, "") new Session(options, host, port, user, control_master, control_path) } class Session private[SSH]( val options: Options, val host: String, val port: Int, val user: String, control_master: Boolean, val control_path: String ) extends System { ssh => def port_suffix: String = if (port > 0) ":" + port else "" def user_prefix: String = if (user.nonEmpty) user + "@" else "" override def toString: String = user_prefix + host + port_suffix override def hg_url: String = "ssh://" + toString + "/" override def rsync_prefix: String = user_prefix + host + ":" /* local ssh commands */ def run_command(command: String, master: Boolean = false, opts: String = "", args: String = "", cwd: JFile = null, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true ): Process_Result = { val config = Config.make(options, port = port, user = user, control_master = master, control_path = control_path) val cmd = Config.command(command, config) + (if (opts.nonEmpty) " " + opts else "") + (if (args.nonEmpty) " -- " + args else "") Isabelle_System.bash(cmd, cwd = cwd, progress_stdout = progress_stdout, progress_stderr = progress_stderr, strict = strict) } def run_sftp( script: String, init: Path => Unit = _ => (), exit: Path => Unit = _ => () ): Process_Result = { Isabelle_System.with_tmp_dir("ssh") { dir => init(dir) File.write(dir + Path.explode("script"), script) val result = run_command("sftp", opts = "-b script", args = Bash.string(host), cwd = dir.file).check exit(dir) result } } def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = { val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "") run_command("ssh", master = master, opts = opts, args = args1) } /* init and exit */ val user_home: String = { run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines match { case List(user_home, shell) => if (shell.endsWith("/bash")) user_home else { error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell) } case _ => error("Malformed remote environment for " + quote(toString)) } } val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home) override def close(): Unit = { if (control_path.nonEmpty) run_ssh(opts = "-O exit").check } /* remote commands */ override def execute(cmd_line: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), settings: Boolean = true, strict: Boolean = true ): Process_Result = { val args1 = Bash.string(host) + " " + Bash.string("export USER_HOME=\"$HOME\"\n" + cmd_line) run_command("ssh", args = args1, progress_stdout = progress_stdout, progress_stderr = progress_stderr, strict = strict) } override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh)) /* remote file-system */ override def expand_path(path: Path): Path = path.expand_env(settings) def remote_path(path: Path): String = expand_path(path).implode override def bash_path(path: Path): String = Bash.string(remote_path(path)) def sftp_path(path: Path): String = sftp_string(remote_path(path)) def rm(path: Path): Unit = run_sftp("rm " + sftp_path(path)) override def is_dir(path: Path): Boolean = run_ssh(args = "test -d " + bash_path(path)).ok override def is_file(path: Path): Boolean = run_ssh(args = "test -f " + bash_path(path)).ok override def make_directory(path: Path): Path = { if (!execute("mkdir -p " + bash_path(path)).ok) { error("Failed to create directory: " + quote(remote_path(path))) } path } def read_dir(path: Path): List[String] = run_sftp("ls -1 -a " + sftp_path(path)).out_lines.flatMap(s => if (s == "." || s == ".." || s.endsWith("/.") || s.endsWith("/..")) None else Some(Library.perhaps_unprefix("./", s))) private def get_file[A](path: Path, f: Path => A): A = { var result: Option[A] = None run_sftp("get -p " + sftp_path(path) + " local", exit = dir => result = Some(f(dir + Path.explode("local")))) result.get } private def put_file(path: Path, f: Path => Unit): Unit = run_sftp("put -p local " + sftp_path(path), init = dir => f(dir + Path.explode("local"))) override def read_file(path: Path, local_path: Path): Unit = get_file(path, Isabelle_System.copy_file(_, local_path)) override def read_bytes(path: Path): Bytes = get_file(path, Bytes.read) override def read(path: Path): String = get_file(path, File.read) override def write_file(path: Path, local_path: Path): Unit = put_file(path, Isabelle_System.copy_file(local_path, _)) def write_bytes(path: Path, bytes: Bytes): Unit = put_file(path, Bytes.write(_, bytes)) def write(path: Path, text: String): Unit = put_file(path, File.write(_, text)) /* tmp dirs */ def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) def rm_tree(remote_dir: String): Unit = execute("rm -r -f " + Bash.string(remote_dir)).check def tmp_dir(): String = execute("mktemp -d /tmp/ssh-XXXXXXXXXXXX").check.out override def with_tmp_dir[A](body: Path => A): A = { val remote_dir = tmp_dir() try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } } /* port forwarding */ def port_forwarding( remote_port: Int, remote_host: String = "localhost", local_port: Int = 0, local_host: String = "localhost", ssh_close: Boolean = false ): Port_Forwarding = { val port = if (local_port > 0) local_port else Isabelle_System.local_port() val forward = List(local_host, port, remote_host, remote_port).mkString(":") val forward_option = "-L " + Bash.string(forward) val cancel: () => Unit = if (control_path.nonEmpty) { run_ssh(opts = forward_option + " -O forward").check () => run_ssh(opts = forward_option + " -O cancel") // permissive } else { val result = Synchronized[Exn.Result[Boolean]](Exn.Res(false)) val thread = Isabelle_Thread.fork("port_forwarding") { val opts = forward_option + " " + Config.option("SessionType", "none") + " " + Config.option("PermitLocalCommand", true) + " " + Config.option("LocalCommand", "pwd") try { run_command("ssh", opts = opts, args = Bash.string(host), progress_stdout = _ => result.change(_ => Exn.Res(true))).check } catch { case exn: Throwable => result.change(_ => Exn.Exn(exn)) } } result.guarded_access { case res@Exn.Res(ok) => if (ok) Some((), res) else None case Exn.Exn(exn) => throw exn } () => thread.interrupt() } val shutdown_hook = Isabelle_System.create_shutdown_hook { cancel() } new Port_Forwarding(host, port, remote_host, remote_port) { override def toString: String = forward override def close(): Unit = { cancel() Isabelle_System.remove_shutdown_hook(shutdown_hook) if (ssh_close) ssh.close() } } } } abstract class Port_Forwarding private[SSH]( val host: String, val port: Int, val remote_host: String, val remote_port: Int ) extends AutoCloseable /* system operations */ trait System extends AutoCloseable { def close(): Unit = () def hg_url: String = "" def rsync_prefix: String = "" def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode def expand_path(path: Path): Path = path.expand def bash_path(path: Path): String = File.bash_path(path) def is_dir(path: Path): Boolean = path.is_dir def is_file(path: Path): Boolean = path.is_file def make_directory(path: Path): Path = Isabelle_System.make_directory(path) def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body) def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) def read_bytes(path: Path): Bytes = Bytes.read(path) def read(path: Path): String = File.read(path) def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), settings: Boolean = true, strict: Boolean = true): Process_Result = Isabelle_System.bash(command, progress_stdout = progress_stdout, progress_stderr = progress_stderr, env = if (settings) Isabelle_System.settings() else null, strict = strict) def isabelle_platform: Isabelle_Platform = Isabelle_Platform() } object Local extends System } diff --git a/src/Pure/System/components.scala b/src/Pure/System/components.scala --- a/src/Pure/System/components.scala +++ b/src/Pure/System/components.scala @@ -1,350 +1,349 @@ /* Title: Pure/System/components.scala Author: Makarius Isabelle system components. */ package isabelle import java.io.{File => JFile} object Components { /* archive name */ object Archive { val suffix: String = ".tar.gz" def apply(name: String): String = if (name == "") error("Bad component name: " + quote(name)) else name + suffix def unapply(archive: String): Option[String] = { for { name0 <- Library.try_unsuffix(suffix, archive) name <- proper_string(name0) } yield name } def get_name(archive: String): String = unapply(archive) getOrElse error("Bad component archive name (expecting .tar.gz): " + quote(archive)) } /* component collections */ def default_component_repository: String = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") def admin(dir: Path): Path = dir + Path.explode("Admin/components") def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = { val name = Archive.get_name(archive.file_name) progress.echo("Unpacking " + name) Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check name } def resolve(base_dir: Path, names: List[String], target_dir: Option[Path] = None, copy_dir: Option[Path] = None, progress: Progress = new Progress ): Unit = { Isabelle_System.make_directory(base_dir) for (name <- names) { val archive_name = Archive(name) val archive = base_dir + Path.explode(archive_name) if (!archive.is_file) { val remote = Components.default_component_repository + "/" + archive_name Isabelle_System.download_file(remote, archive, progress = progress) } for (dir <- copy_dir) { Isabelle_System.make_directory(dir) Isabelle_System.copy_file(archive, dir) } unpack(target_dir getOrElse base_dir, archive, progress = progress) } } private val platforms_family: Map[Platform.Family.Value, Set[String]] = Map( Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"), Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"), Platform.Family.macos -> Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), Platform.Family.windows -> Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) private val platforms_all: Set[String] = Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2) def purge(dir: Path, platform: Platform.Family.Value): Unit = { val purge_set = platforms_all -- platforms_family(platform) File.find_files(dir.file, (file: JFile) => file.isDirectory && purge_set(file.getName), include_dirs = true).foreach(Isabelle_System.rm_tree) } /* component directories */ def directories(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) /* component directory content */ def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") def check_dir(dir: Path): Boolean = settings(dir).is_file || components(dir).is_file def read_components(dir: Path): List[String] = split_lines(File.read(components(dir))).filter(_.nonEmpty) def write_components(dir: Path, lines: List[String]): Unit = File.write(components(dir), terminate_lines(lines)) /* component repository content */ val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) { override def toString: String = digest.shasum(name) } def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => Word.explode(line) match { case Nil => None case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name)) case _ => error("Bad components.sha1 entry: " + quote(line)) }) def write_components_sha1(entries: List[SHA1_Digest]): Unit = File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n")) /** manage user components **/ val components_path: Path = Path.explode("$ISABELLE_HOME_USER/etc/components") def read_components(): List[String] = if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) else Nil def write_components(lines: List[String]): Unit = { Isabelle_System.make_directory(components_path.dir) File.write(components_path, Library.terminate_lines(lines)) } def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = { val path = path0.expand.absolute if (!check_dir(path) && !Sessions.is_session_dir(path)) error("Bad component directory: " + path) val lines1 = read_components() val lines2 = lines1.filter(line => line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) val lines3 = if (add) lines2 ::: List(path.implode) else lines2 if (lines1 != lines3) write_components(lines3) val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" progress.echo(prefix + " component " + path) } /* main entry point */ def main(args: Array[String]): Unit = { Command_Line.tool { for (arg <- args) { val add = if (arg.startsWith("+")) true else if (arg.startsWith("-")) false else error("Bad argument: " + quote(arg)) val path = Path.explode(arg.substring(1)) update_components(add, path, progress = new Console_Progress) } } } /** build and publish components **/ def build_components( options: Options, components: List[Path], progress: Progress = new Progress, publish: Boolean = false, force: Boolean = false, update_components_sha1: Boolean = false ): Unit = { val archives: List[Path] = for (path <- components) yield { path.file_name match { case Archive(_) => path case name => if (!path.is_dir) error("Bad component directory: " + path) else if (!check_dir(path)) { error("Malformed component directory: " + path + "\n (requires " + settings() + " or " + Components.components() + ")") } else { val component_path = path.expand val archive_dir = component_path.dir val archive_name = Archive(name) val archive = archive_dir + Path.explode(archive_name) if (archive.is_file && !force) { error("Component archive already exists: " + archive) } progress.echo("Packaging " + archive_name) Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), dir = archive_dir).check archive } } } if ((publish && archives.nonEmpty) || update_components_sha1) { - options.string("isabelle_components_server") match { - case SSH.Target(user, host) => - using(SSH.open_session(options, host = host, user = user)) { ssh => - val components_dir = Path.explode(options.string("isabelle_components_dir")) - val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) - - for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { - error("Bad remote directory: " + dir) - } - - if (publish) { - for (archive <- archives) { - val archive_name = archive.file_name - val name = Archive.get_name(archive_name) - val remote_component = components_dir + archive.base - val remote_contrib = contrib_dir + Path.explode(name) - - // component archive - if (ssh.is_file(remote_component) && !force) { - error("Remote component archive already exists: " + remote_component) - } - progress.echo("Uploading " + archive_name) - ssh.write_file(remote_component, archive) + val server = options.string("isabelle_components_server") + if (server.isEmpty) error("Undefined option isabelle_components_server") - // contrib directory - val is_standard_component = - Isabelle_System.with_tmp_dir("component") { tmp_dir => - Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check - check_dir(tmp_dir + Path.explode(name)) - } - if (is_standard_component) { - if (ssh.is_dir(remote_contrib)) { - if (force) ssh.rm_tree(remote_contrib) - else error("Remote component directory already exists: " + remote_contrib) - } - progress.echo("Unpacking remote " + archive_name) - ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + - ssh.bash_path(remote_component)).check - } - else { - progress.echo_warning("No unpacking of non-standard component: " + archive_name) - } + using(SSH.open_session(options, server)) { ssh => + val components_dir = Path.explode(options.string("isabelle_components_dir")) + val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) + + for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { + error("Bad remote directory: " + dir) + } + + if (publish) { + for (archive <- archives) { + val archive_name = archive.file_name + val name = Archive.get_name(archive_name) + val remote_component = components_dir + archive.base + val remote_contrib = contrib_dir + Path.explode(name) + + // component archive + if (ssh.is_file(remote_component) && !force) { + error("Remote component archive already exists: " + remote_component) + } + progress.echo("Uploading " + archive_name) + ssh.write_file(remote_component, archive) + + // contrib directory + val is_standard_component = + Isabelle_System.with_tmp_dir("component") { tmp_dir => + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check + check_dir(tmp_dir + Path.explode(name)) } + if (is_standard_component) { + if (ssh.is_dir(remote_contrib)) { + if (force) ssh.rm_tree(remote_contrib) + else error("Remote component directory already exists: " + remote_contrib) + } + progress.echo("Unpacking remote " + archive_name) + ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + + ssh.bash_path(remote_component)).check } - - // remote SHA1 digests - if (update_components_sha1) { - val lines = - for { - entry <- ssh.read_dir(components_dir) - if ssh.is_file(components_dir + Path.basic(entry)) && - entry.endsWith(Archive.suffix) - } - yield { - progress.echo("Digesting remote " + entry) - ssh.execute("cd " + ssh.bash_path(components_dir) + - "; sha1sum " + Bash.string(entry)).check.out - } - write_components_sha1(read_components_sha1(lines)) + else { + progress.echo_warning("No unpacking of non-standard component: " + archive_name) } } - case s => error("Bad isabelle_components_server: " + quote(s)) + } + + // remote SHA1 digests + if (update_components_sha1) { + val lines = + for { + entry <- ssh.read_dir(components_dir) + if ssh.is_file(components_dir + Path.basic(entry)) && + entry.endsWith(Archive.suffix) + } + yield { + progress.echo("Digesting remote " + entry) + ssh.execute("cd " + ssh.bash_path(components_dir) + + "; sha1sum " + Bash.string(entry)).check.out + } + write_components_sha1(read_components_sha1(lines)) + } } } // local SHA1 digests { val new_entries = for (archive <- archives) yield { val name = archive.file_name progress.echo("Digesting local " + name) SHA1_Digest(SHA1.digest(archive), name) } val new_names = new_entries.map(_.name).toSet write_components_sha1( new_entries ::: read_components_sha1().filterNot(entry => new_names.contains(entry.name))) } } /* Isabelle tool wrapper */ private val relevant_options = List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") val isabelle_tool = Isabelle_Tool("build_components", "build and publish Isabelle components", Scala_Project.here, { args => var publish = false var update_components_sha1 = false var force = false var options = Options.init() def show_options: String = cat_lines(relevant_options.flatMap(options.get).map(_.print)) val getopts = Getopts(""" Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... Options are: -P publish on SSH server (see options below) -f force: overwrite existing component archives and directories -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u update all SHA1 keys in Isabelle repository Admin/components Build and publish Isabelle components as .tar.gz archives on SSH server, depending on system options: """ + Library.indent_lines(2, show_options) + "\n", "P" -> (_ => publish = true), "f" -> (_ => force = true), "o:" -> (arg => options = options + arg), "u" -> (_ => update_components_sha1 = true)) val more_args = getopts(args) if (more_args.isEmpty && !update_components_sha1) getopts.usage() val progress = new Console_Progress build_components(options, more_args.map(Path.explode), progress = progress, publish = publish, force = force, update_components_sha1 = update_components_sha1) }) } diff --git a/src/Pure/Tools/phabricator.scala b/src/Pure/Tools/phabricator.scala --- a/src/Pure/Tools/phabricator.scala +++ b/src/Pure/Tools/phabricator.scala @@ -1,1058 +1,1055 @@ /* Title: Pure/Tools/phabricator.scala Author: Makarius Support for Phabricator server, notably for Ubuntu 20.04 LTS. See also: - https://www.phacility.com/phabricator - https://secure.phabricator.com/book/phabricator */ package isabelle import scala.collection.mutable import scala.util.matching.Regex object Phabricator { /** defaults **/ /* required packages */ val packages_ubuntu_20_04: List[String] = Build_Docker.packages ::: List( // https://secure.phabricator.com/source/phabricator/browse/master/scripts/install/install_ubuntu.sh 15e6e2adea61 "git", "mysql-server", "apache2", "libapache2-mod-php", "php", "php-mysql", "php-gd", "php-curl", "php-apcu", "php-cli", "php-json", "php-mbstring", // more packages "php-xml", "php-zip", "python3-pygments", "ssh", "subversion", "python-pygments", // mercurial build packages "make", "gcc", "python", "python2-dev", "python-docutils", "python-openssl") def packages: List[String] = { val release = Linux.Release() if (release.is_ubuntu_20_04) packages_ubuntu_20_04 else error("Bad Linux version: expected Ubuntu 20.04 LTS") } /* global system resources */ val www_user = "www-data" val daemon_user = "phabricator" val sshd_config: Path = Path.explode("/etc/ssh/sshd_config") /* installation parameters */ val default_name = "vcs" def phabricator_name(name: String = "", ext: String = ""): String = "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext) def isabelle_phabricator_name(name: String = "", ext: String = ""): String = "isabelle-" + phabricator_name(name = name, ext = ext) def default_root(name: String): Path = Path.explode("/var/www") + Path.basic(phabricator_name(name = name)) def default_repo(name: String): Path = default_root(name) + Path.basic("repo") val default_mailers: Path = Path.explode("mailers.json") val default_system_port: Int = 22 val alternative_system_port = 222 val default_server_port = 2222 val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz" /** global configuration **/ val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf")) def global_config_script( init: String = "", body: String = "", exit: String = ""): String = { """#!/bin/bash """ + (if (init.nonEmpty) "\n" + init else "") + """ { while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } do NAME="$(echo "$REPLY" | cut -d: -f1)" ROOT="$(echo "$REPLY" | cut -d: -f2)" { """ + Library.indent_lines(6, body) + """ } < /dev/null done } < """ + File.bash_path(global_config) + "\n" + (if (exit.nonEmpty) "\n" + exit + "\n" else "") } sealed case class Config(name: String, root: Path) { def home: Path = root + Path.explode(phabricator_name()) def execute(command: String): Process_Result = Isabelle_System.bash("bin/" + command, cwd = home.file, redirect = true).check } def read_config(): List[Config] = { if (global_config.is_file) { for (entry <- Library.trim_split_lines(File.read(global_config)) if entry.nonEmpty) yield { space_explode(':', entry) match { case List(name, root) => Config(name, Path.explode(root)) case _ => error("Malformed config file " + global_config + "\nentry " + quote(entry)) } } } else Nil } def write_config(configs: List[Config]): Unit = { File.write(global_config, configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n")) } def get_config(name: String): Config = read_config().find(config => config.name == name) getOrElse error("Bad Isabelle/Phabricator installation " + quote(name)) /** administrative tools **/ /* Isabelle tool wrapper */ val isabelle_tool1 = Isabelle_Tool("phabricator", "invoke command-line tool within Phabricator home directory", Scala_Project.here, { args => var list = false var name = default_name val getopts = Getopts(""" Usage: isabelle phabricator [OPTIONS] COMMAND [ARGS...] Options are: -l list available Phabricator installations -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Invoke a command-line tool within the home directory of the named Phabricator installation. """, "l" -> (_ => list = true), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.isEmpty && !list) getopts.usage() val progress = new Console_Progress if (list) { for (config <- read_config()) { progress.echo("phabricator " + quote(config.name) + " root " + config.root) } } else { val config = get_config(name) val result = progress.bash(Bash.strings(more_args), cwd = config.home.file, echo = true) if (!result.ok) error(result.print_return_code) } }) /** setup **/ def user_setup(name: String, description: String, ssh_setup: Boolean = false): Unit = { if (!Linux.user_exists(name)) { Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup) } else if (Linux.user_description(name) != description) { error("User " + quote(name) + " already exists --" + " for Phabricator it should have the description:\n " + quote(description)) } } def command_setup(name: String, init: String = "", body: String = "", exit: String = "" ): Path = { val command = Path.explode("/usr/local/bin") + Path.basic(name) File.write(command, global_config_script(init = init, body = body, exit = exit)) Isabelle_System.chmod("755", command) Isabelle_System.chown("root:root", command) command } def mercurial_setup(mercurial_source: String, progress: Progress = new Progress): Unit = { progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...") Isabelle_System.with_tmp_dir("mercurial") { tmp_dir => val archive = if (Url.is_wellformed(mercurial_source)) { val archive = tmp_dir + Path.basic("mercurial.tar.gz") Isabelle_System.download_file(mercurial_source, archive) archive } else Path.explode(mercurial_source) Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir)) progress.bash("make all && make install", cwd = build_dir.file, echo = true).check } } def phabricator_setup( options: Options, name: String = default_name, root: String = "", repo: String = "", package_update: Boolean = false, mercurial_source: String = "", progress: Progress = new Progress ): Unit = { /* system environment */ Linux.check_system_root() progress.echo("System packages ...") if (package_update) { Linux.package_update(progress = progress) Linux.check_reboot_required() } Linux.package_install(packages, progress = progress) Linux.check_reboot_required() if (mercurial_source.nonEmpty) { for { name <- List("mercurial", "mercurial-common") if Linux.package_installed(name) } { error("Cannot install Mercurial from source:\n" + "package package " + quote(name) + " already installed") } mercurial_setup(mercurial_source, progress = progress) } /* users */ if (name.exists((c: Char) => !(Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c))) || Set("", "ssh", "phd", "dump", daemon_user).contains(name)) { error("Bad installation name: " + quote(name)) } user_setup(daemon_user, "Phabricator Daemon User", ssh_setup = true) user_setup(name, "Phabricator SSH User") /* basic installation */ progress.echo("\nPhabricator installation ...") val root_path = if (root.nonEmpty) Path.explode(root) else default_root(name) val repo_path = if (repo.nonEmpty) Path.explode(repo) else default_repo(name) val configs = read_config() for (config <- configs if config.name == name) { error("Duplicate Phabricator installation " + quote(name) + " in " + config.root) } if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { error("Failed to create root directory " + root_path) } Isabelle_System.chown(Bash.string(www_user) + ":" + Bash.string(www_user), root_path) Isabelle_System.chmod("755", root_path) progress.bash(cwd = root_path.file, echo = true, script = """ set -e echo "Cloning distribution repositories:" git clone --branch stable https://github.com/phacility/arcanist.git git -C arcanist reset --hard """ + Bash.string(options.string("phabricator_version_arcanist")) + """ git clone --branch stable https://github.com/phacility/phabricator.git git -C phabricator reset --hard """ + Bash.string(options.string("phabricator_version_phabricator")) + """ """).check val config = Config(name, root_path) write_config(configs ::: List(config)) config.execute("config set pygments.enabled true") /* local repository directory */ progress.echo("\nRepository hosting setup ...") if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { error("Failed to create local repository directory " + repo_path) } Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), repo_path) Isabelle_System.chmod("755", repo_path) config.execute("config set repository.default-local-path " + File.bash_path(repo_path)) val sudoers_file = Path.explode("/etc/sudoers.d") + Path.basic(isabelle_phabricator_name(name = name)) File.write(sudoers_file, www_user + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/ssh, /usr/bin/id\n" + name + " ALL=(" + daemon_user + ") SETENV: NOPASSWD: /usr/bin/git, /usr/bin/git-upload-pack, /usr/bin/git-receive-pack, /usr/local/bin/hg, /usr/bin/hg, /usr/bin/svnserve, /usr/bin/ssh, /usr/bin/id\n") Isabelle_System.chmod("440", sudoers_file) config.execute("config set diffusion.ssh-user " + Bash.string(config.name)) /* MySQL setup */ progress.echo("\nMySQL setup ...") File.write(Path.explode("/etc/mysql/mysql.conf.d/" + phabricator_name(ext = "cnf")), """[mysqld] max_allowed_packet = 32M innodb_buffer_pool_size = 1600M local_infile = 0 """) Linux.service_restart("mysql") def mysql_conf(R: Regex, which: String): String = { val conf = Path.explode("/etc/mysql/debian.cnf") split_lines(File.read(conf)).collectFirst({ case R(a) => a }) match { case Some(res) => res case None => error("Cannot determine " + which + " from " + conf) } } val mysql_root_user = mysql_conf("""^user\s*=\s*(\S*)\s*$""".r, "superuser name") val mysql_root_password = mysql_conf("""^password\s*=\s*(\S*)\s*$""".r, "superuser password") val mysql_name = phabricator_name(name = name).replace("-", "_") val mysql_user_string = SQL.string(mysql_name) + "@'localhost'" val mysql_password = Linux.generate_password() Isabelle_System.bash("mysql --user=" + Bash.string(mysql_root_user) + " --password=" + Bash.string(mysql_root_password) + " --execute=" + Bash.string( """DROP USER IF EXISTS """ + mysql_user_string + "; " + """CREATE USER """ + mysql_user_string + """ IDENTIFIED BY """ + SQL.string(mysql_password) + """ PASSWORD EXPIRE NEVER; """ + """GRANT ALL ON `""" + (mysql_name + "_%").replace("_", "\\_") + """`.* TO """ + mysql_user_string + ";" + """GRANT PROCESS ON *.* TO """ + mysql_user_string + ";")).check config.execute("config set mysql.user " + Bash.string(mysql_name)) config.execute("config set mysql.pass " + Bash.string(mysql_password)) config.execute("config set phabricator.cache-namespace " + Bash.string(mysql_name)) config.execute("config set storage.default-namespace " + Bash.string(mysql_name)) config.execute("config set storage.mysql-engine.max-size 8388608") progress.bash("bin/storage upgrade --force", cwd = config.home.file, echo = true).check /* database dump */ val dump_name = isabelle_phabricator_name(name = "dump") command_setup(dump_name, body = """mkdir -p "$ROOT/database" && chown root:root "$ROOT/database" && chmod 700 "$ROOT/database" [ -e "$ROOT/database/dump.sql.gz" ] && mv -f "$ROOT/database/dump.sql.gz" "$ROOT/database/dump-old.sql.gz" echo -n "Creating $ROOT/database/dump.sql.gz ..." "$ROOT/phabricator/bin/storage" dump --compress --output "$ROOT/database/dump.sql.gz" 2>&1 | fgrep -v '[Warning] Using a password on the command line interface can be insecure' echo " $(ls -hs "$ROOT/database/dump.sql.gz" | cut -d" " -f1)" """) /* Phabricator upgrade */ command_setup(isabelle_phabricator_name(name = "upgrade"), init = """BRANCH="${1:-stable}" if [ "$BRANCH" != "master" -a "$BRANCH" != "stable" ] then echo "Bad branch: \"$BRANCH\"" exit 1 fi systemctl stop isabelle-phabricator-phd systemctl stop apache2 """, body = """echo -e "\nUpgrading phabricator \"$NAME\" root \"$ROOT\" ..." for REPO in arcanist phabricator do cd "$ROOT/$REPO" echo -e "\nUpdating \"$REPO\" ..." git checkout "$BRANCH" git pull done echo -e "\nUpgrading storage ..." "$ROOT/phabricator/bin/storage" upgrade --force """, exit = """systemctl start apache2 systemctl start isabelle-phabricator-phd""") /* PHP setup */ val php_version = Isabelle_System.bash("""php --run 'echo PHP_MAJOR_VERSION . "." . PHP_MINOR_VERSION;'""") .check.out val php_conf = Path.explode("/etc/php") + Path.basic(php_version) + // educated guess Path.explode("apache2/conf.d") + Path.basic(isabelle_phabricator_name(ext = "ini")) File.write(php_conf, "post_max_size = 32M\n" + "opcache.validate_timestamps = 0\n" + "memory_limit = 512M\n" + "max_execution_time = 120\n") /* Apache setup */ progress.echo("Apache setup ...") val apache_root = Path.explode("/etc/apache2") val apache_sites = apache_root + Path.explode("sites-available") if (!apache_sites.is_dir) error("Bad Apache sites directory " + apache_sites) val server_name = phabricator_name(name = name, ext = "lvh.me") // alias for "localhost" for testing val server_url = "http://" + server_name File.write(apache_sites + Path.basic(isabelle_phabricator_name(name = name, ext = "conf")), """ ServerName """ + server_name + """ ServerAdmin webmaster@localhost DocumentRoot """ + config.home.implode + """/webroot ErrorLog ${APACHE_LOG_DIR}/error.log CustomLog ${APACHE_LOG_DIR}/access.log combined RewriteEngine on RewriteRule ^(.*)$ /index.php?__path__=$1 [B,L,QSA] # vim: syntax=apache ts=4 sw=4 sts=4 sr noet """) Isabelle_System.bash( """ set -e a2enmod rewrite a2ensite """ + Bash.string(isabelle_phabricator_name(name = name))).check config.execute("config set phabricator.base-uri " + Bash.string(server_url)) Linux.service_restart("apache2") progress.echo("\nFurther manual configuration via " + server_url) /* PHP daemon */ progress.echo("\nPHP daemon setup ...") val phd_log_path = Isabelle_System.make_directory(Path.explode("/var/tmp/phd")) Isabelle_System.chown( "-R " + Bash.string(daemon_user) + ":" + Bash.string(daemon_user), phd_log_path) Isabelle_System.chmod("755", phd_log_path) config.execute("config set phd.user " + Bash.string(daemon_user)) config.execute("config set phd.log-directory /var/tmp/phd/" + isabelle_phabricator_name(name = name) + "/log") val phd_name = isabelle_phabricator_name(name = "phd") Linux.service_shutdown(phd_name) val phd_command = command_setup(phd_name, body = """"$ROOT/phabricator/bin/phd" "$@" """) try { Linux.service_install(phd_name, """[Unit] Description=PHP daemon manager for Isabelle/Phabricator After=syslog.target network.target apache2.service mysql.service [Service] Type=oneshot User=""" + daemon_user + """ Group=""" + daemon_user + """ Environment=PATH=/sbin:/usr/sbin:/usr/local/sbin:/usr/local/bin:/usr/bin:/bin ExecStart=""" + phd_command.implode + """ start --force ExecStop=""" + phd_command.implode + """ stop RemainAfterExit=yes [Install] WantedBy=multi-user.target """) } catch { case ERROR(msg) => progress.bash("bin/phd status", cwd = config.home.file, echo = true).check error(msg) } } /* Isabelle tool wrapper */ val isabelle_tool2 = Isabelle_Tool("phabricator_setup", "setup Phabricator server on Ubuntu Linux", Scala_Project.here, { args => var mercurial_source = "" var repo = "" var package_update = false var name = default_name var options = Options.init() var root = "" val getopts = Getopts(""" Usage: isabelle phabricator_setup [OPTIONS] Options are: -M SOURCE install Mercurial from source: local PATH, or URL, or ":" for """ + standard_mercurial_source + """ -R DIR repository directory (default: """ + default_repo("NAME") + """) -U full update of system packages before installation -n NAME Phabricator installation name (default: """ + quote(default_name) + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r DIR installation root directory (default: """ + default_root("NAME") + """) Install Phabricator as LAMP application (Linux, Apache, MySQL, PHP). The installation name (default: """ + quote(default_name) + """) is mapped to a regular Unix user; this is relevant for public SSH access. """, "M:" -> (arg => mercurial_source = (if (arg == ":") standard_mercurial_source else arg)), "R:" -> (arg => repo = arg), "U" -> (_ => package_update = true), "n:" -> (arg => name = arg), "o:" -> (arg => options = options + arg), "r:" -> (arg => root = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup(options, name = name, root = root, repo = repo, package_update = package_update, mercurial_source = mercurial_source, progress = progress) }) /** setup mail **/ val mailers_template: String = """[ { "key": "example.org", "type": "smtp", "options": { "host": "mail.example.org", "port": 465, "user": "phabricator@example.org", "password": "********", "protocol": "ssl", "message-id": true } } ]""" def phabricator_setup_mail( name: String = default_name, config_file: Option[Path] = None, test_user: String = "", progress: Progress = new Progress ): Unit = { Linux.check_system_root() val config = get_config(name) val default_config_file = config.root + default_mailers val mail_config = config_file getOrElse default_config_file def setup_mail: Unit = { progress.echo("Using mail configuration from " + mail_config) config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config)) if (test_user.nonEmpty) { progress.echo("Sending test mail to " + quote(test_user)) progress.bash(cwd = config.home.file, echo = true, script = """echo "Test from Phabricator ($(date))" | bin/mail send-test --subject "Test" --to """ + Bash.string(test_user)).check } } if (config_file.isEmpty) { if (!default_config_file.is_file) { File.write(default_config_file, mailers_template) Isabelle_System.chmod("600", default_config_file) } if (File.read(default_config_file) == mailers_template) { progress.echo("Please invoke the tool again, after providing details in\n " + default_config_file.implode + "\n") } else setup_mail } else setup_mail } /* Isabelle tool wrapper */ val isabelle_tool3 = Isabelle_Tool("phabricator_setup_mail", "setup mail for one Phabricator installation", Scala_Project.here, { args => var test_user = "" var name = default_name var config_file: Option[Path] = None val getopts = Getopts(""" Usage: isabelle phabricator_setup_mail [OPTIONS] Options are: -T USER send test mail to Phabricator user -f FILE config file (default: """ + default_mailers + """ within Phabricator root) -n NAME Phabricator installation name (default: """ + quote(default_name) + """) Provide mail configuration for existing Phabricator installation. """, "T:" -> (arg => test_user = arg), "f:" -> (arg => config_file = Some(Path.explode(arg))), "n:" -> (arg => name = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_mail(name = name, config_file = config_file, test_user = test_user, progress = progress) }) /** setup ssh **/ /* sshd config */ private val Port = """^\s*Port\s+(\d+)\s*$""".r private val No_Port = """^#\s*Port\b.*$""".r private val Any_Port = """^#?\s*Port\b.*$""".r def conf_ssh_port(port: Int): String = if (port == default_system_port) "#Port " + default_system_port else "Port " + port def read_ssh_port(conf: Path): Int = { val lines = split_lines(File.read(conf)) val ports = lines.flatMap({ case Port(Value.Int(p)) => Some(p) case No_Port() => Some(default_system_port) case _ => None }) ports match { case List(port) => port case Nil => error("Missing Port specification in " + conf) case _ => error("Multiple Port specifications in " + conf) } } def write_ssh_port(conf: Path, port: Int): Boolean = { val old_port = read_ssh_port(conf) if (old_port == port) false else { val lines = split_lines(File.read(conf)) val lines1 = lines.map({ case Any_Port() => conf_ssh_port(port) case line => line }) File.write(conf, cat_lines(lines1)) true } } /* phabricator_setup_ssh */ def phabricator_setup_ssh( server_port: Int = default_server_port, system_port: Int = default_system_port, progress: Progress = new Progress ): Unit = { Linux.check_system_root() val configs = read_config() if (server_port == system_port) { error("Port for Phabricator sshd coincides with system port: " + system_port) } val sshd_conf_system = Path.explode("/etc/ssh/sshd_config") val sshd_conf_server = sshd_conf_system.ext(isabelle_phabricator_name()) val ssh_name = isabelle_phabricator_name(name = "ssh") Linux.service_shutdown(ssh_name) val old_system_port = read_ssh_port(sshd_conf_system) if (old_system_port != system_port) { progress.echo("Reconfigurig system ssh service") Linux.service_shutdown("ssh") write_ssh_port(sshd_conf_system, system_port) Linux.service_start("ssh") } progress.echo("Configuring " + ssh_name + " service") val ssh_command = command_setup(ssh_name, body = """if [ "$1" = "$NAME" ] then exec "$ROOT/phabricator/bin/ssh-auth" "$@" fi""", exit = "exit 1") File.write(sshd_conf_server, """# OpenBSD Secure Shell server for Isabelle/Phabricator AuthorizedKeysCommand """ + ssh_command.implode + """ AuthorizedKeysCommandUser """ + daemon_user + """ AuthorizedKeysFile none AllowUsers """ + configs.map(_.name).mkString(" ") + """ Port """ + server_port + """ Protocol 2 PermitRootLogin no AllowAgentForwarding no AllowTcpForwarding no PrintMotd no PrintLastLog no PasswordAuthentication no ChallengeResponseAuthentication no PidFile /var/run/""" + ssh_name + """.pid """) Linux.service_install(ssh_name, """[Unit] Description=OpenBSD Secure Shell server for Isabelle/Phabricator After=network.target auditd.service ConditionPathExists=!/etc/ssh/sshd_not_to_be_run [Service] EnvironmentFile=-/etc/default/ssh ExecStartPre=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecStart=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -D $SSHD_OPTS ExecReload=/usr/sbin/sshd -f """ + sshd_conf_server.implode + """ -t ExecReload=/bin/kill -HUP $MAINPID KillMode=process Restart=on-failure RestartPreventExitStatus=255 Type=notify RuntimeDirectory=sshd-phabricator RuntimeDirectoryMode=0755 [Install] WantedBy=multi-user.target Alias=""" + ssh_name + """.service """) for (config <- configs) { progress.echo("phabricator " + quote(config.name) + " port " + server_port) config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString)) if (server_port == default_system_port) config.execute("config delete diffusion.ssh-port") } } /* Isabelle tool wrapper */ val isabelle_tool4 = Isabelle_Tool("phabricator_setup_ssh", "setup ssh service for all Phabricator installations", Scala_Project.here, { args => var server_port = default_server_port var system_port = default_system_port val getopts = Getopts(""" Usage: isabelle phabricator_setup_ssh [OPTIONS] Options are: -p PORT sshd port for Phabricator servers (default: """ + default_server_port + """) -q PORT sshd port for the operating system (default: """ + default_system_port + """) Configure ssh service for all Phabricator installations: a separate sshd is run in addition to the one of the operating system, and ports need to be distinct. A particular Phabricator installation is addressed by using its name as the ssh user; the actual Phabricator user is determined via stored ssh keys. """, "p:" -> (arg => server_port = Value.Int.parse(arg)), "q:" -> (arg => system_port = Value.Int.parse(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress phabricator_setup_ssh( server_port = server_port, system_port = system_port, progress = progress) }) /** conduit API **/ object API { /* user information */ sealed case class User( id: Long, phid: String, name: String, real_name: String, roles: List[String] ) { def is_valid: Boolean = roles.contains("verified") && roles.contains("approved") && roles.contains("activated") def is_admin: Boolean = roles.contains("admin") def is_regular: Boolean = !(roles.contains("bot") || roles.contains("list")) } /* repository information */ sealed case class Repository( vcs: VCS.Value, id: Long, phid: String, name: String, callsign: String, short_name: String, importing: Boolean, ssh_url: String ) { def is_hg: Boolean = vcs == VCS.hg } object VCS extends Enumeration { val hg, git, svn = Value def read(s: String): Value = try { withName(s) } catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) } } def edits(typ: String, value: JSON.T): List[JSON.Object.T] = List(JSON.Object("type" -> typ, "value" -> value)) def opt_edits(typ: String, value: Option[JSON.T]): List[JSON.Object.T] = value.toList.flatMap(edits(typ, _)) /* result with optional error */ sealed case class Result(result: JSON.T, error: Option[String]) { def ok: Boolean = error.isEmpty def get: JSON.T = if (ok) result else Exn.error(error.get) def get_value[A](unapply: JSON.T => Option[A]): A = unapply(get) getOrElse Exn.error("Bad JSON result: " + JSON.Format(result)) def get_string: String = get_value(JSON.Value.String.unapply) } def make_result(json: JSON.T): Result = { val result = JSON.value(json, "result").getOrElse(JSON.Object.empty) val error_info = JSON.string(json, "error_info") val error_code = JSON.string(json, "error_code") Result(result, error_info orElse error_code) } /* context for operations */ - def apply(user: String, host: String, port: Int = default_system_port): API = - new API(user, host, port) + def apply(ssh_target: String, ssh_port: Int = default_system_port): API = + new API(ssh_target, ssh_port) } - final class API private(ssh_user: String, ssh_host: String, ssh_port: Int) { + final class API private(ssh_target: String, ssh_port: Int) { /* connection */ - require(ssh_host.nonEmpty && ssh_port >= 0, "bad ssh host or port") - - private def ssh_user_prefix: String = - if (ssh_user.nonEmpty) ssh_user + "@" else "" + require(ssh_target.nonEmpty && ssh_port >= 0, "bad ssh host or port") private def ssh_port_suffix: String = if (ssh_port != default_system_port) ":" + ssh_port else "" - override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix - def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix + override def toString: String = ssh_target + ssh_port_suffix + def hg_url: String = "ssh://" + ssh_target + ssh_port_suffix /* execute methods */ def execute_raw(method: String, params: JSON.T = JSON.Object.empty): JSON.T = { Isabelle_System.with_tmp_file("params", "json") { params_file => File.write(params_file, JSON.Format(JSON.Object("params" -> JSON.Format(params)))) val result = Isabelle_System.bash( - "ssh -p " + ssh_port + " " + Bash.string(ssh_user_prefix + ssh_host) + + "ssh -p " + ssh_port + " " + Bash.string(ssh_target) + " conduit " + Bash.string(method) + " < " + File.bash_path(params_file)).check JSON.parse(result.out, strict = false) } } def execute(method: String, params: JSON.T = JSON.Object.empty): API.Result = API.make_result(execute_raw(method, params = params)) def execute_search[A]( method: String, params: JSON.Object.T, unapply: JSON.T => Option[A] ): List[A] = { val results = new mutable.ListBuffer[A] var after = "" var cont = true while (cont) { val result = execute(method, params = params ++ JSON.optional("after" -> proper_string(after))) results ++= result.get_value(JSON.list(_, "data", unapply)) after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after"))) cont = after.nonEmpty } results.toList } def ping(): String = execute("conduit.ping").get_string /* users */ lazy val user_phid: String = execute("user.whoami").get_value(JSON.string(_, "phid")) lazy val user_name: String = execute("user.whoami").get_value(JSON.string(_, "userName")) def get_users( all: Boolean = false, phid: String = "", name: String = "" ): List[API.User] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "usernames" -> name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("user.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "username") real_name <- JSON.string0(fields, "realName") roles <- JSON.strings(fields, "roles") } yield API.User(id, phid, name, real_name, roles))) } def the_user(phid: String): API.User = get_users(phid = phid) match { case List(user) => user case _ => error("Bad user PHID " + quote(phid)) } /* repositories */ def get_repositories( all: Boolean = false, phid: String = "", callsign: String = "", short_name: String = "" ): List[API.Repository] = { val constraints: JSON.Object.T = (for { (key, value) <- List("phids" -> phid, "callsigns" -> callsign, "shortNames" -> short_name) if value.nonEmpty } yield (key, List(value))).toMap execute_search("diffusion.repository.search", JSON.Object("queryKey" -> (if (all) "all" else "active"), "constraints" -> constraints), data => JSON.value(data, "fields", fields => for { vcs_name <- JSON.string(fields, "vcs") id <- JSON.long(data, "id") phid <- JSON.string(data, "phid") name <- JSON.string(fields, "name") callsign <- JSON.string0(fields, "callsign") short_name <- JSON.string0(fields, "shortName") importing <- JSON.bool(fields, "isImporting") } yield { val vcs = API.VCS.read(vcs_name) val url_path = if (short_name.isEmpty) "/diffusion/" + id else "/source/" + short_name val ssh_url = vcs match { case API.VCS.hg => hg_url + url_path case API.VCS.git => hg_url + url_path + ".git" case API.VCS.svn => "" } API.Repository(vcs, id, phid, name, callsign, short_name, importing, ssh_url) })) } def the_repository(phid: String): API.Repository = get_repositories(phid = phid) match { case List(repo) => repo case _ => error("Bad repository PHID " + quote(phid)) } def create_repository( name: String, callsign: String = "", // unique name, UPPERCASE short_name: String = "", // unique name description: String = "", public: Boolean = false, vcs: API.VCS.Value = API.VCS.hg ): API.Repository = { require(name.nonEmpty, "bad repository name") val transactions = API.edits("vcs", vcs.toString) ::: API.edits("name", name) ::: API.opt_edits("callsign", proper_string(callsign)) ::: API.opt_edits("shortName", proper_string(short_name)) ::: API.opt_edits("description", proper_string(description)) ::: (if (public) Nil else API.edits("view", user_phid) ::: API.edits("policy.push", user_phid)) ::: API.edits("status", "active") val phid = execute("diffusion.repository.edit", params = JSON.Object("transactions" -> transactions)) .get_value(JSON.value(_, "object", JSON.string(_, "phid"))) execute("diffusion.looksoon", params = JSON.Object("repositories" -> List(phid))).get the_repository(phid) } } }