src/Pure/Tools/build_history.scala
author wenzelm
Mon, 03 Oct 2016 16:50:29 +0200
changeset 64021 1e23caac8757
child 64023 41f7e383c19e
permissions -rw-r--r--
basic setup for Admin/build_history -- outside of Isabelle environment;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/build_history.scala
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     3
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     4
Build other history versions.
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     5
*/
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     6
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     7
package isabelle
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     8
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
     9
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    10
import java.io.{File => JFile}
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    11
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    12
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    13
object Build_History
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    14
{
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    15
  val rev0 = "0cebcbeac4c7"  // wenzelm 29-Aug-2012: provide polyml-5.4.1 as regular component
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    16
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    17
  def apply(hg: Mercurial.Repository, rev: String = "",
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    18
    isabelle_identifier: String = "build_history"): Build_History =
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    19
      new Build_History(hg, rev, isabelle_identifier)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    20
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    21
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    22
  /* command line entry point */
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    23
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    24
  def main(args: Array[String])
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    25
  {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    26
    Command_Line.tool0 {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    27
      var force = false
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    28
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    29
      val getopts = Getopts("""
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    30
Usage: isabelle build_history [OPTIONS] REPOSITORY [REV]
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    31
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    32
  Options are:
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    33
    -f           force -- allow irreversible operations on REPOSITORY
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    34
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    35
  Build Isabelle sessions from the history of another REPOSITORY clone,
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    36
  starting at changeset REV (default: tip).
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    37
""",
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    38
        "f" -> (_ => force = true))
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    39
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    40
      val more_args = getopts(args)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    41
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    42
      val (root, rev) =
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    43
        more_args match {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    44
          case List(root, rev) => (root, rev)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    45
          case List(root) => (root, "tip")
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    46
          case _ => getopts.usage()
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    47
        }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    48
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    49
      using(Mercurial.open_repository(Path.explode(root)))(hg =>
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    50
        {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    51
          val build_history = Build_History(hg, rev)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    52
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    53
          if (!force)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    54
            error("Repository " + hg + " will be cleaned by force!\n" +
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    55
              "Need to provide option -f to confirm this.")
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    56
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    57
          build_history.init()
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    58
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    59
          Output.writeln(
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    60
            build_history.bash("bin/isabelle getenv ISABELLE_HOME ISABELLE_HOME_USER").check.out)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    61
        })
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    62
    }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    63
  }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    64
}
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    65
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    66
class Build_History private(hg: Mercurial.Repository, rev: String, isabelle_identifier: String)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    67
{
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    68
  override def toString: String =
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    69
    List(hg.toString, rev, isabelle_identifier).mkString("Build_History(", ",", ")")
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    70
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    71
  def bash(script: String): Process_Result =
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    72
    Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    73
      " " + script, cwd = hg.root.file, env = null)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    74
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    75
  def init()
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    76
  {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    77
    hg.update(rev = rev, clean = true)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    78
  }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    79
}