src/Pure/Tools/build_history.scala
author wenzelm
Tue Oct 11 22:24:14 2016 +0200 (2016-10-11)
changeset 64155 646c4d6a6a02
parent 64151 be9b3cffe058
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Tools/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 
    24   /** other Isabelle environment **/
    25 
    26   private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
    27   {
    28     other_isabelle =>
    29 
    30 
    31     /* static system */
    32 
    33     def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    34       Isabelle_System.bash(
    35         "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
    36         env = null, cwd = isabelle_home.file, redirect = redirect,
    37         progress_stdout = progress.echo_if(echo, _),
    38         progress_stderr = progress.echo_if(echo, _))
    39 
    40     def copy_dir(dir1: Path, dir2: Path): Unit =
    41       bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
    42 
    43     def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    44       bash("bin/isabelle " + cmdline, redirect, echo)
    45 
    46     def resolve_components(echo: Boolean): Unit =
    47       other_isabelle("components -a", redirect = true, echo = echo).check
    48 
    49     val isabelle_home_user: Path =
    50       Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
    51 
    52     val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
    53     val log_dir: Path = isabelle_home_user + Path.explode("log")
    54 
    55 
    56     /* reset settings */
    57 
    58     def reset_settings(components_base: String, nonfree: Boolean)
    59     {
    60       if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
    61         error("Cannot proceed with existing user settings file: " + etc_settings)
    62 
    63       Isabelle_System.mkdirs(etc_settings.dir)
    64       File.write(etc_settings,
    65         "# generated by Isabelle " + Date.now() + "\n" +
    66         "#-*- shell-script -*- :mode=shellscript:\n")
    67 
    68       val component_settings =
    69       {
    70         val components_base_path =
    71           if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
    72           else Path.explode(components_base).expand
    73 
    74         val catalogs =
    75           if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
    76 
    77         catalogs.map(catalog =>
    78           "init_components " + File.bash_path(components_base_path) +
    79             " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
    80       }
    81       File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
    82     }
    83 
    84 
    85     /* augment settings */
    86 
    87     def augment_settings(
    88       threads: Int,
    89       arch_64: Boolean = false,
    90       heap: Int = default_heap,
    91       max_heap: Option[Int] = None,
    92       more_settings: List[String]): String =
    93     {
    94       val (ml_platform, ml_settings) =
    95       {
    96         val windows_32 = "x86-windows"
    97         val windows_64 = "x86_64-windows"
    98         val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
    99         val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
   100         val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
   101 
   102         val polyml_home =
   103           try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
   104           catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
   105 
   106         def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
   107 
   108         def err(platform: String): Nothing =
   109           error("Platform " + platform + " unavailable on this machine")
   110 
   111         def check_dir(platform: String): Boolean =
   112           platform != "" && ml_home(platform).is_dir
   113 
   114         val ml_platform =
   115           if (Platform.is_windows && arch_64) {
   116             if (check_dir(windows_64)) windows_64 else err(windows_64)
   117           }
   118           else if (Platform.is_windows && !arch_64) {
   119             if (check_dir(windows_32)) windows_32
   120             else platform_32  // x86-cygwin
   121           }
   122           else {
   123             val (platform, platform_name) =
   124               if (arch_64) (platform_64, "x86_64-" + platform_family)
   125               else (platform_32, "x86-" + platform_family)
   126             if (check_dir(platform)) platform else err(platform_name)
   127           }
   128 
   129         val ml_options =
   130           "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
   131           " --gcthreads " + threads +
   132           (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
   133 
   134         (ml_platform,
   135           List(
   136             "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
   137             "ML_PLATFORM=" + quote(ml_platform),
   138             "ML_OPTIONS=" + quote(ml_options)))
   139       }
   140 
   141       val thread_settings =
   142         List(
   143           "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
   144           "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
   145 
   146       val settings =
   147         List(ml_settings, thread_settings) :::
   148           (if (more_settings.isEmpty) Nil else List(more_settings))
   149 
   150       File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_))))
   151 
   152       ml_platform
   153     }
   154   }
   155 
   156 
   157 
   158   /** build_history **/
   159 
   160   private val default_rev = "tip"
   161   private val default_threads = 1
   162   private val default_heap = 1000
   163   private val default_isabelle_identifier = "build_history"
   164 
   165   def build_history(
   166     progress: Progress,
   167     hg: Mercurial.Repository,
   168     rev: String = default_rev,
   169     isabelle_identifier: String = default_isabelle_identifier,
   170     components_base: String = "",
   171     fresh: Boolean = false,
   172     nonfree: Boolean = false,
   173     multicore_base: Boolean = false,
   174     threads_list: List[Int] = List(default_threads),
   175     arch_64: Boolean = false,
   176     heap: Int = default_heap,
   177     max_heap: Option[Int] = None,
   178     more_settings: List[String] = Nil,
   179     verbose: Boolean = false,
   180     build_args: List[String] = Nil): List[Process_Result] =
   181   {
   182     /* sanity checks */
   183 
   184     if (File.eq(Path.explode("~~").file, hg.root.file))
   185       error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
   186 
   187     for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
   188 
   189     if (heap < 100) error("Bad heap value < 100: " + heap)
   190 
   191     if (max_heap.isDefined && max_heap.get < heap)
   192       error("Bad max_heap value < heap: " + max_heap.get)
   193 
   194     System.getenv("ISABELLE_SETTINGS_PRESENT") match {
   195       case null | "" =>
   196       case _ => error("Cannot run build_history within existing Isabelle settings environment")
   197     }
   198 
   199 
   200     /* init repository */
   201 
   202     hg.update(rev = rev, clean = true)
   203     progress.echo_if(verbose, hg.log(rev, options = "-l1"))
   204 
   205     val isabelle_version = hg.identify(rev, options = "-i")
   206     val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
   207 
   208 
   209     /* main */
   210 
   211     val build_history_date = Date.now()
   212     val build_host = Isabelle_System.hostname()
   213 
   214     var first_build = true
   215     for (threads <- threads_list) yield
   216     {
   217       /* init settings */
   218 
   219       other_isabelle.reset_settings(components_base, nonfree)
   220       other_isabelle.resolve_components(verbose)
   221       val ml_platform =
   222         other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
   223 
   224       val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
   225       val isabelle_output_log = isabelle_output + Path.explode("log")
   226       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
   227 
   228       if (first_build) {
   229         other_isabelle.resolve_components(verbose)
   230         other_isabelle.bash(
   231           "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
   232             "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
   233           redirect = true, echo = verbose).check
   234 
   235         Isabelle_System.rm_tree(isabelle_base_log.file)
   236       }
   237 
   238       Isabelle_System.rm_tree(isabelle_output.file)
   239       Isabelle_System.mkdirs(isabelle_output)
   240 
   241 
   242       /* build */
   243 
   244       if (multicore_base && !first_build && isabelle_base_log.is_dir)
   245         other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log)
   246 
   247       val build_start = Date.now()
   248       val res =
   249         other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
   250       val build_end = Date.now()
   251 
   252 
   253       /* output log */
   254 
   255       val log_path =
   256         other_isabelle.log_dir +
   257           Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
   258 
   259       val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
   260 
   261       val meta_info =
   262         List(Build_Log.Field.build_engine -> BUILD_HISTORY,
   263           Build_Log.Field.build_host -> build_host,
   264           Build_Log.Field.build_start -> Build_Log.print_date(build_start),
   265           Build_Log.Field.build_end -> Build_Log.print_date(build_end),
   266           Build_Log.Field.isabelle_version -> isabelle_version)
   267 
   268       val ml_statistics =
   269         build_info.finished_sessions.flatMap(session_name =>
   270           {
   271             val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
   272             if (session_log.is_file) {
   273               Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
   274                 ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
   275             }
   276             else Nil
   277           })
   278 
   279       val heap_sizes =
   280         build_info.finished_sessions.flatMap(session_name =>
   281           {
   282             val heap = isabelle_output + Path.explode(session_name)
   283             if (heap.is_file)
   284               Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
   285             else None
   286           })
   287 
   288       Isabelle_System.mkdirs(log_path.dir)
   289       File.write_gzip(log_path,
   290         Library.terminate_lines(
   291           Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
   292           ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
   293           heap_sizes))
   294 
   295       Output.writeln(log_path.implode, stdout = true)
   296 
   297 
   298       /* next build */
   299 
   300       if (multicore_base && first_build && isabelle_output_log.is_dir)
   301         other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
   302 
   303       first_build = false
   304 
   305       res
   306     }
   307   }
   308 
   309 
   310   /* command line entry point */
   311 
   312   def main(args: Array[String])
   313   {
   314     Command_Line.tool0 {
   315       var multicore_base = false
   316       var components_base = ""
   317       var heap: Option[Int] = None
   318       var max_heap: Option[Int] = None
   319       var threads_list = List(default_threads)
   320       var isabelle_identifier = default_isabelle_identifier
   321       var more_settings: List[String] = Nil
   322       var fresh = false
   323       var arch_64 = false
   324       var nonfree = false
   325       var rev = default_rev
   326       var verbose = false
   327 
   328       val getopts = Getopts("""
   329 Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
   330 
   331   Options are:
   332     -B           first multicore build serves as base for scheduling information
   333     -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
   334     -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
   335     -M THREADS   multicore configurations (comma-separated list, default: """ + default_threads + """)
   336     -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
   337     -U SIZE      maximal ML heap in MB (default: unbounded)
   338     -e TEXT      additional text for generated etc/settings
   339     -f           fresh build of Isabelle/Scala components (recommended)
   340     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
   341     -n           include nonfree components
   342     -r REV       update to revision (default: """ + default_rev + """)
   343     -v           verbose
   344 
   345   Build Isabelle sessions from the history of another REPOSITORY clone,
   346   passing ARGS directly to its isabelle build tool.
   347 """,
   348         "B" -> (_ => multicore_base = true),
   349         "C:" -> (arg => components_base = arg),
   350         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
   351         "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
   352         "N:" -> (arg => isabelle_identifier = arg),
   353         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
   354         "e:" -> (arg => more_settings = more_settings ::: List(arg)),
   355         "f" -> (_ => fresh = true),
   356         "m:" ->
   357           {
   358             case "32" | "x86" => arch_64 = false
   359             case "64" | "x86_64" => arch_64 = true
   360             case bad => error("Bad processor architecture: " + quote(bad))
   361           },
   362         "n" -> (_ => nonfree = true),
   363         "r:" -> (arg => rev = arg),
   364         "v" -> (_ => verbose = true))
   365 
   366       val more_args = getopts(args)
   367       val (root, build_args) =
   368         more_args match {
   369           case root :: build_args => (root, build_args)
   370           case _ => getopts.usage()
   371         }
   372 
   373       using(Mercurial.open_repository(Path.explode(root)))(hg =>
   374         {
   375           val progress = new Console_Progress(stderr = true)
   376           val results =
   377             build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
   378               components_base = components_base, fresh = fresh, nonfree = nonfree,
   379               multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
   380               heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
   381               max_heap = max_heap, more_settings = more_settings, verbose = verbose,
   382               build_args = build_args)
   383           val rc = (0 /: results) { case (rc, res) => rc max res.rc }
   384           if (rc != 0) sys.exit(rc)
   385         })
   386     }
   387   }
   388 }