src/Pure/Admin/build_release.scala
changeset 73634 c88faa1e09e1
parent 73632 7c70f10e0b3b
child 73637 f3a356c64193
equal deleted inserted replaced
73633:7e465e166bb2 73634:c88faa1e09e1
   221   }
   221   }
   222 
   222 
   223 
   223 
   224   /** build release **/
   224   /** build release **/
   225 
   225 
   226   /* build heaps on remote server */
   226   /* build heaps */
   227 
   227 
   228   private def remote_build_heaps(
   228   private def build_heaps(
   229     options: Options,
   229     options: Options,
   230     platform: Platform.Family.Value,
   230     platform: Platform.Family.Value,
   231     build_sessions: List[String],
   231     build_sessions: List[String],
   232     local_dir: Path): Unit =
   232     local_dir: Path): Unit =
   233   {
   233   {
   234     val server_option = "build_host_" + platform.toString
   234     val server_option = "build_host_" + platform.toString
   235     options.string(server_option) match {
   235     val ssh =
   236       case SSH.Target(user, host) =>
   236       options.string(server_option) match {
   237         using(SSH.open_session(options, host = host, user = user))(ssh =>
   237         case "" =>
   238           Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
   238           if (Platform.family == platform) SSH.Local
   239           {
   239           else error("Undefined option " + server_option + ": cannot build heaps")
   240             execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
   240         case SSH.Target(user, host) =>
   241             ssh.with_tmp_dir(remote_dir =>
   241           SSH.open_session(options, host = host, user = user)
   242             {
   242         case s => error("Malformed option " + server_option + ": " + quote(s))
   243               val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
   243       }
   244               ssh.write_file(remote_tmp_tar, local_tmp_tar)
   244     try {
   245               val remote_commands =
   245       Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
   246                 List(
   246       {
   247                   "cd " + File.bash_path(remote_dir),
   247         execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
   248                   "tar -xf tmp.tar",
   248         ssh.with_tmp_dir(remote_dir =>
   249                   "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
   249         {
   250                   "tar -cf tmp.tar heaps")
   250           val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
   251               ssh.execute(remote_commands.mkString(" && ")).check
   251           ssh.write_file(remote_tmp_tar, local_tmp_tar)
   252               ssh.read_file(remote_tmp_tar, local_tmp_tar)
   252           val remote_commands =
   253             })
   253             List(
   254             execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
   254               "cd " + File.bash_path(remote_dir),
   255           })
   255               "tar -xf tmp.tar",
   256         )
   256               "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
   257       case s => error("Bad " + server_option + ": " + quote(s))
   257               "tar -cf tmp.tar heaps")
   258     }
   258           ssh.execute(remote_commands.mkString(" && "), settings = false).check
       
   259           ssh.read_file(remote_tmp_tar, local_tmp_tar)
       
   260         })
       
   261         execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
       
   262       })
       
   263     }
       
   264     finally { ssh.close() }
   259   }
   265   }
   260 
   266 
   261 
   267 
   262   /* Isabelle application */
   268   /* Isabelle application */
   263 
   269 
   592 
   598 
   593 
   599 
   594         // build heaps
   600         // build heaps
   595 
   601 
   596         if (build_sessions.nonEmpty) {
   602         if (build_sessions.nonEmpty) {
   597           progress.echo("Building heaps ...")
   603           progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
   598           remote_build_heaps(options, platform, build_sessions, isabelle_target)
   604           build_heaps(options, platform, build_sessions, isabelle_target)
   599         }
   605         }
   600 
   606 
   601 
   607 
   602         // application bundling
   608         // application bundling
   603 
   609 
   899       if (more_args.nonEmpty) getopts.usage()
   905       if (more_args.nonEmpty) getopts.usage()
   900 
   906 
   901       if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
   907       if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
   902         error("Building for windows requires 7z")
   908         error("Building for windows requires 7z")
   903 
   909 
       
   910       val progress = new Console_Progress()
   904       def make_context(name: String): Release_Context =
   911       def make_context(name: String): Release_Context =
   905         Release_Context(target_dir,
   912         Release_Context(target_dir,
   906           release_name = name,
   913           release_name = name,
   907           components_base = components_base,
   914           components_base = components_base,
   908           progress = new Console_Progress())
   915           progress = progress)
   909 
   916 
   910       val context =
   917       val context =
   911         if (source_archive.isEmpty) {
   918         if (source_archive.isEmpty) {
   912           val context = make_context(release_name)
   919           val context = make_context(release_name)
   913           val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
   920           val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
   914           build_release_archive(context, version, parallel_jobs = parallel_jobs)
   921           build_release_archive(context, version, parallel_jobs = parallel_jobs)
   915           context
   922           context
   916         }
   923         }
   917         else {
   924         else {
   918           val archive = Release_Archive.get(source_archive, rename = release_name)
   925           val archive =
       
   926             Release_Archive.get(source_archive, rename = release_name, progress = progress)
   919           val context = make_context(archive.identifier)
   927           val context = make_context(archive.identifier)
   920           Isabelle_System.new_directory(context.dist_dir)
   928           Isabelle_System.make_directory(context.dist_dir)
   921           use_release_archive(context, archive, id = rev)
   929           use_release_archive(context, archive, id = rev)
   922           context
   930           context
   923         }
   931         }
   924 
   932 
   925       build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
   933       build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,