src/Pure/Admin/build_history.scala
author wenzelm
Fri Mar 17 21:55:13 2017 +0100 (2017-03-17)
changeset 65296 a71db30f3b2d
parent 65293 a53a5ae88205
child 65318 342efc382558
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Admin/build_history.scala
     2     Author:     Makarius
     3 
     4 Build other history versions.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 import java.time.format.DateTimeFormatter
    12 import java.util.Locale
    13 
    14 
    15 object Build_History
    16 {
    17   /* log files */
    18 
    19   val BUILD_HISTORY = "build_history"
    20   val META_INFO_MARKER = "\fmeta_info = "
    21 
    22 
    23   /* augment settings */
    24 
    25   def augment_settings(
    26     other_isabelle: Other_Isabelle,
    27     threads: Int,
    28     arch_64: Boolean = false,
    29     heap: Int = default_heap,
    30     max_heap: Option[Int] = None,
    31     more_settings: List[String]): String =
    32   {
    33     val (ml_platform, ml_settings) =
    34     {
    35       val windows_32 = "x86-windows"
    36       val windows_64 = "x86_64-windows"
    37       val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
    38       val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
    39       val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
    40 
    41       val polyml_home =
    42         try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
    43         catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
    44 
    45       def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
    46 
    47       def err(platform: String): Nothing =
    48         error("Platform " + platform + " unavailable on this machine")
    49 
    50       def check_dir(platform: String): Boolean =
    51         platform != "" && ml_home(platform).is_dir
    52 
    53       val ml_platform =
    54         if (Platform.is_windows && arch_64) {
    55           if (check_dir(windows_64)) windows_64 else err(windows_64)
    56         }
    57         else if (Platform.is_windows && !arch_64) {
    58           if (check_dir(windows_32)) windows_32
    59           else platform_32  // x86-cygwin
    60         }
    61         else {
    62           val (platform, platform_name) =
    63             if (arch_64) (platform_64, "x86_64-" + platform_family)
    64             else (platform_32, "x86-" + platform_family)
    65           if (check_dir(platform)) platform else err(platform_name)
    66         }
    67 
    68       val ml_options =
    69         "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
    70         " --gcthreads " + threads +
    71         (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
    72 
    73       (ml_platform,
    74         List(
    75           "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
    76           "ML_PLATFORM=" + quote(ml_platform),
    77           "ML_OPTIONS=" + quote(ml_options)))
    78     }
    79 
    80     val thread_settings =
    81       List(
    82         "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
    83         "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
    84 
    85     val settings =
    86       List(ml_settings, thread_settings) :::
    87         (if (more_settings.isEmpty) Nil else List(more_settings))
    88 
    89     File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
    90 
    91     ml_platform
    92   }
    93 
    94 
    95 
    96   /** build_history **/
    97 
    98   private val default_rev = "tip"
    99   private val default_multicore = (1, 1)
   100   private val default_heap = 1500
   101   private val default_isabelle_identifier = "build_history"
   102 
   103   def build_history(
   104     hg: Mercurial.Repository,
   105     progress: Progress = No_Progress,
   106     rev: String = default_rev,
   107     isabelle_identifier: String = default_isabelle_identifier,
   108     components_base: String = "",
   109     fresh: Boolean = false,
   110     nonfree: Boolean = false,
   111     multicore_base: Boolean = false,
   112     multicore_list: List[(Int, Int)] = List(default_multicore),
   113     arch_64: Boolean = false,
   114     heap: Int = default_heap,
   115     max_heap: Option[Int] = None,
   116     more_settings: List[String] = Nil,
   117     verbose: Boolean = false,
   118     build_tags: List[String] = Nil,
   119     build_args: List[String] = Nil): List[(Process_Result, Path)] =
   120   {
   121     /* sanity checks */
   122 
   123     if (File.eq(Path.explode("~~"), hg.root))
   124       error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
   125 
   126     for ((threads, _) <- multicore_list if threads < 1)
   127       error("Bad threads value < 1: " + threads)
   128     for ((_, processes) <- multicore_list if processes < 1)
   129       error("Bad processes value < 1: " + processes)
   130 
   131     if (heap < 100) error("Bad heap value < 100: " + heap)
   132 
   133     if (max_heap.isDefined && max_heap.get < heap)
   134       error("Bad max_heap value < heap: " + max_heap.get)
   135 
   136     System.getenv("ISABELLE_SETTINGS_PRESENT") match {
   137       case null | "" =>
   138       case _ => error("Cannot run build_history within existing Isabelle settings environment")
   139     }
   140 
   141 
   142     /* init repository */
   143 
   144     hg.update(rev = rev, clean = true)
   145     progress.echo_if(verbose, hg.log(rev, options = "-l1"))
   146 
   147     val isabelle_version = hg.id(rev)
   148     val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
   149 
   150 
   151     /* main */
   152 
   153     val build_host = Isabelle_System.hostname()
   154     val build_history_date = Date.now()
   155     val build_group_id = build_host + ":" + build_history_date.time.ms
   156 
   157     var first_build = true
   158     for ((threads, processes) <- multicore_list) yield
   159     {
   160       /* init settings */
   161 
   162       other_isabelle.init_settings(components_base, nonfree)
   163       other_isabelle.resolve_components(verbose)
   164       val ml_platform =
   165         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
   166 
   167       val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
   168       val isabelle_output_log = isabelle_output + Path.explode("log")
   169       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
   170 
   171       if (first_build) {
   172         other_isabelle.resolve_components(verbose)
   173 
   174         if (fresh)
   175           Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
   176         other_isabelle.bash(
   177           "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
   178             "bin/isabelle jedit -b", redirect = true, echo = verbose).check
   179 
   180         Isabelle_System.rm_tree(isabelle_base_log)
   181       }
   182 
   183       Isabelle_System.rm_tree(isabelle_output)
   184       Isabelle_System.mkdirs(isabelle_output)
   185 
   186 
   187       /* build */
   188 
   189       if (multicore_base && !first_build && isabelle_base_log.is_dir)
   190         Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
   191 
   192       val build_start = Date.now()
   193       val build_args1 = List("-v", "-j" + processes) ::: build_args
   194       val build_result =
   195         other_isabelle("build " + Bash.strings(build_args1), redirect = true, echo = verbose)
   196       val build_end = Date.now()
   197 
   198       val log_path =
   199         other_isabelle.isabelle_home_user +
   200           Build_Log.log_subdir(build_history_date) +
   201           Build_Log.log_filename(BUILD_HISTORY, build_history_date,
   202             List(build_host, ml_platform, "M" + threads) ::: build_tags)
   203 
   204       val build_info =
   205         Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info()
   206 
   207 
   208       /* output log */
   209 
   210       val store = Sessions.store()
   211 
   212       val meta_info =
   213         Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
   214         Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args1) :::
   215         List(
   216           Build_Log.Prop.build_group_id -> build_group_id,
   217           Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms),
   218           Build_Log.Prop.build_engine -> BUILD_HISTORY,
   219           Build_Log.Prop.build_host -> build_host,
   220           Build_Log.Prop.build_start -> Build_Log.print_date(build_start),
   221           Build_Log.Prop.build_end -> Build_Log.print_date(build_end),
   222           Build_Log.Prop.isabelle_version -> isabelle_version)
   223 
   224       val ml_statistics =
   225         build_info.finished_sessions.flatMap(session_name =>
   226           {
   227             val database = isabelle_output + store.database(session_name)
   228             val log_gz = isabelle_output + store.log_gz(session_name)
   229 
   230             val properties =
   231               if (database.is_file) {
   232                 using(SQLite.open_database(database))(db =>
   233                   store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
   234               }
   235               else if (log_gz.is_file) {
   236                 Build_Log.Log_File(log_gz).
   237                   parse_session_info(session_name, ml_statistics = true).ml_statistics
   238               }
   239               else Nil
   240             properties.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
   241           })
   242 
   243       val heap_sizes =
   244         build_info.finished_sessions.flatMap(session_name =>
   245           {
   246             val heap = isabelle_output + Path.explode(session_name)
   247             if (heap.is_file)
   248               Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
   249             else None
   250           })
   251 
   252       Isabelle_System.mkdirs(log_path.dir)
   253       File.write_xz(log_path.ext("xz"),
   254         terminate_lines(
   255           Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
   256           ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
   257           heap_sizes), XZ.options(6))
   258 
   259 
   260       /* next build */
   261 
   262       if (multicore_base && first_build && isabelle_output_log.is_dir)
   263         Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
   264 
   265       Isabelle_System.rm_tree(isabelle_output)
   266 
   267       first_build = false
   268 
   269       (build_result, log_path.ext("xz"))
   270     }
   271   }
   272 
   273 
   274   /* command line entry point */
   275 
   276   private object Multicore
   277   {
   278     private val Pat1 = """^(\d+)$""".r
   279     private val Pat2 = """^(\d+)x(\d+)$""".r
   280 
   281     def parse(s: String): (Int, Int) =
   282       s match {
   283         case Pat1(Value.Int(x)) => (x, 1)
   284         case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
   285         case _ => error("Bad multicore configuration: " + quote(s))
   286       }
   287   }
   288 
   289   def main(args: Array[String])
   290   {
   291     Command_Line.tool0 {
   292       var multicore_base = false
   293       var components_base = ""
   294       var heap: Option[Int] = None
   295       var max_heap: Option[Int] = None
   296       var multicore_list = List(default_multicore)
   297       var isabelle_identifier = default_isabelle_identifier
   298       var more_settings: List[String] = Nil
   299       var fresh = false
   300       var arch_64 = false
   301       var nonfree = false
   302       var rev = default_rev
   303       var build_tags = List.empty[String]
   304       var verbose = false
   305 
   306       val getopts = Getopts("""
   307 Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
   308 
   309   Options are:
   310     -B           first multicore build serves as base for scheduling information
   311     -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
   312     -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
   313     -M MULTICORE multicore configurations (see below)
   314     -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
   315     -U SIZE      maximal ML heap in MB (default: unbounded)
   316     -e TEXT      additional text for generated etc/settings
   317     -f           fresh build of Isabelle/Scala components (recommended)
   318     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
   319     -n           include nonfree components
   320     -r REV       update to revision (default: """ + default_rev + """)
   321     -t TAG       free-form build tag (multiple occurrences possible)
   322     -v           verbose
   323 
   324   Build Isabelle sessions from the history of another REPOSITORY clone,
   325   passing ARGS directly to its isabelle build tool.
   326 
   327   Each MULTICORE configuration consists of one or two numbers (default 1):
   328   THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
   329 """,
   330         "B" -> (_ => multicore_base = true),
   331         "C:" -> (arg => components_base = arg),
   332         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
   333         "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
   334         "N:" -> (arg => isabelle_identifier = arg),
   335         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
   336         "e:" -> (arg => more_settings = more_settings ::: List(arg)),
   337         "f" -> (_ => fresh = true),
   338         "m:" ->
   339           {
   340             case "32" | "x86" => arch_64 = false
   341             case "64" | "x86_64" => arch_64 = true
   342             case bad => error("Bad processor architecture: " + quote(bad))
   343           },
   344         "n" -> (_ => nonfree = true),
   345         "r:" -> (arg => rev = arg),
   346         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
   347         "v" -> (_ => verbose = true))
   348 
   349       val more_args = getopts(args)
   350       val (root, build_args) =
   351         more_args match {
   352           case root :: build_args => (root, build_args)
   353           case _ => getopts.usage()
   354         }
   355 
   356       val hg = Mercurial.repository(Path.explode(root))
   357       val progress = new Console_Progress(stderr = true)
   358 
   359       val results =
   360         build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
   361           components_base = components_base, fresh = fresh, nonfree = nonfree,
   362           multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
   363           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
   364           max_heap = max_heap, more_settings = more_settings, verbose = verbose,
   365           build_tags = build_tags, build_args = build_args)
   366 
   367       for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
   368 
   369       val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
   370       if (rc != 0) sys.exit(rc)
   371     }
   372   }
   373 
   374 
   375 
   376   /** remote build_history -- via command-line **/
   377 
   378   def remote_build_history(
   379     ssh: SSH.Session,
   380     isabelle_repos_self: Path,
   381     isabelle_repos_other: Path,
   382     isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
   383     self_update: Boolean = false,
   384     push_isabelle_home: Boolean = false,
   385     progress: Progress = No_Progress,
   386     options: String = "",
   387     args: String = ""): (List[(String, Bytes)], Process_Result) =
   388   {
   389     val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
   390 
   391 
   392     /* prepare repository clones */
   393 
   394     val isabelle_hg =
   395       Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
   396 
   397     val rev =
   398       if (self_update) {
   399         val rev =
   400           if (push_isabelle_home) {
   401             val isabelle_home_hg = Mercurial.repository(Path.explode("~~"))
   402             val rev = isabelle_home_hg.id()
   403             isabelle_home_hg.push(isabelle_hg.root_url, rev = rev, force = true)
   404             rev
   405           }
   406           else {
   407             isabelle_hg.pull()
   408             isabelle_hg.id()
   409           }
   410         isabelle_hg.update(rev = rev, clean = true)
   411         ssh.execute(
   412           ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle"))
   413             + " components -a").check
   414         ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
   415         rev
   416       }
   417       else "tip"
   418 
   419     val other_hg =
   420       Mercurial.setup_repository(
   421         ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
   422     other_hg.pull(isabelle_hg.root.implode)
   423     other_hg.update(rev = rev, clean = true)
   424 
   425 
   426     /* Admin/build_history */
   427 
   428     val process_result =
   429       ssh.execute(
   430         ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
   431           ssh.bash_path(isabelle_repos_other) + " " + args,
   432         progress_stdout = progress.echo(_),
   433         progress_stderr = progress.echo(_),
   434         strict = false)
   435 
   436     val result =
   437       for (line <- process_result.out_lines)
   438       yield {
   439         val log = Path.explode(line)
   440         val bytes = ssh.read_bytes(log)
   441         ssh.rm(log)
   442         (log.base.implode, bytes)
   443       }
   444 
   445     (result, process_result)
   446   }
   447 }