basic setup for Admin/build_history -- outside of Isabelle environment;
authorwenzelm
Mon Oct 03 16:50:29 2016 +0200 (2016-10-03)
changeset 640211e23caac8757
parent 64020 355b78441650
child 64022 3c0193f82d20
basic setup for Admin/build_history -- outside of Isabelle environment;
Admin/build_history
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build_history.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/build_history	Mon Oct 03 16:50:29 2016 +0200
     1.3 @@ -0,0 +1,10 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# DESCRIPTION: build history versions from another repository clone
     1.7 +
     1.8 +
     1.9 +THIS="$(cd "$(dirname "$0")"; pwd)"
    1.10 +
    1.11 +"$THIS/build" jars || exit $?
    1.12 +
    1.13 +exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"
     2.1 --- a/src/Pure/System/isabelle_system.scala	Mon Oct 03 16:15:59 2016 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Oct 03 16:50:29 2016 +0200
     2.3 @@ -260,7 +260,10 @@
     2.4      val proc = new ProcessBuilder
     2.5      proc.command(command_line:_*)  // fragile on Windows
     2.6      if (cwd != null) proc.directory(cwd)
     2.7 -    proc.environment.clear; for ((x, y) <- env) proc.environment.put(x, y)
     2.8 +    if (env != null) {
     2.9 +      proc.environment.clear
    2.10 +      for ((x, y) <- env) proc.environment.put(x, y)
    2.11 +    }
    2.12      proc.redirectErrorStream(redirect)
    2.13      proc.start
    2.14    }
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/build_history.scala	Mon Oct 03 16:50:29 2016 +0200
     3.3 @@ -0,0 +1,79 @@
     3.4 +/*  Title:      Pure/Tools/build_history.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Build other history versions.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +import java.io.{File => JFile}
    3.14 +
    3.15 +
    3.16 +object Build_History
    3.17 +{
    3.18 +  val rev0 = "0cebcbeac4c7"  // wenzelm 29-Aug-2012: provide polyml-5.4.1 as regular component
    3.19 +
    3.20 +  def apply(hg: Mercurial.Repository, rev: String = "",
    3.21 +    isabelle_identifier: String = "build_history"): Build_History =
    3.22 +      new Build_History(hg, rev, isabelle_identifier)
    3.23 +
    3.24 +
    3.25 +  /* command line entry point */
    3.26 +
    3.27 +  def main(args: Array[String])
    3.28 +  {
    3.29 +    Command_Line.tool0 {
    3.30 +      var force = false
    3.31 +
    3.32 +      val getopts = Getopts("""
    3.33 +Usage: isabelle build_history [OPTIONS] REPOSITORY [REV]
    3.34 +
    3.35 +  Options are:
    3.36 +    -f           force -- allow irreversible operations on REPOSITORY
    3.37 +
    3.38 +  Build Isabelle sessions from the history of another REPOSITORY clone,
    3.39 +  starting at changeset REV (default: tip).
    3.40 +""",
    3.41 +        "f" -> (_ => force = true))
    3.42 +
    3.43 +      val more_args = getopts(args)
    3.44 +
    3.45 +      val (root, rev) =
    3.46 +        more_args match {
    3.47 +          case List(root, rev) => (root, rev)
    3.48 +          case List(root) => (root, "tip")
    3.49 +          case _ => getopts.usage()
    3.50 +        }
    3.51 +
    3.52 +      using(Mercurial.open_repository(Path.explode(root)))(hg =>
    3.53 +        {
    3.54 +          val build_history = Build_History(hg, rev)
    3.55 +
    3.56 +          if (!force)
    3.57 +            error("Repository " + hg + " will be cleaned by force!\n" +
    3.58 +              "Need to provide option -f to confirm this.")
    3.59 +
    3.60 +          build_history.init()
    3.61 +
    3.62 +          Output.writeln(
    3.63 +            build_history.bash("bin/isabelle getenv ISABELLE_HOME ISABELLE_HOME_USER").check.out)
    3.64 +        })
    3.65 +    }
    3.66 +  }
    3.67 +}
    3.68 +
    3.69 +class Build_History private(hg: Mercurial.Repository, rev: String, isabelle_identifier: String)
    3.70 +{
    3.71 +  override def toString: String =
    3.72 +    List(hg.toString, rev, isabelle_identifier).mkString("Build_History(", ",", ")")
    3.73 +
    3.74 +  def bash(script: String): Process_Result =
    3.75 +    Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +
    3.76 +      " " + script, cwd = hg.root.file, env = null)
    3.77 +
    3.78 +  def init()
    3.79 +  {
    3.80 +    hg.update(rev = rev, clean = true)
    3.81 +  }
    3.82 +}
     4.1 --- a/src/Pure/build-jars	Mon Oct 03 16:15:59 2016 +0200
     4.2 +++ b/src/Pure/build-jars	Mon Oct 03 16:50:29 2016 +0200
     4.3 @@ -107,6 +107,7 @@
     4.4    Tools/bibtex.scala
     4.5    Tools/build.scala
     4.6    Tools/build_doc.scala
     4.7 +  Tools/build_history.scala
     4.8    Tools/build_stats.scala
     4.9    Tools/check_keywords.scala
    4.10    Tools/check_sources.scala