src/Pure/Tools/build_history.scala
author wenzelm
Mon, 03 Oct 2016 21:14:21 +0200
changeset 64026 cbecd26e063f
parent 64025 ff4910ced9ba
child 64027 4a33d740c9dc
permissions -rw-r--r--
clarified command line; clarified result;
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}
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    11
import java.util.Calendar
64021
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
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    14
object Build_History
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    15
{
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    16
  /* build_history */
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    17
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    18
  private val default_rev = "tip"
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    19
  private val default_isabelle_identifier = "build_history"
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    20
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    21
  def build_history(
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    22
    hg: Mercurial.Repository,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    23
    rev: String = default_rev,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    24
    isabelle_identifier: String = default_isabelle_identifier,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    25
    components_base: String = "",
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    26
    fresh: Boolean = false,
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    27
    nonfree: Boolean = false,
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    28
    verbose: Boolean = false,
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    29
    build_args: List[String] = Nil): Process_Result =
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    30
  {
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    31
    hg.update(rev = rev, clean = true)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    32
    if (verbose) hg.command("log -l1").check.print
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    33
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    34
    def bash(script: String): Process_Result =
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    35
      Isabelle_System.bash("env ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) +
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    36
        " " + script, cwd = hg.root.file, env = null)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    37
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    38
    def isabelle(cmdline: String): Process_Result = bash("bin/isabelle " + cmdline)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    39
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    40
    val isabelle_home_user: Path = Path.explode(isabelle("getenv -b ISABELLE_HOME_USER").check.out)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    41
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    42
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    43
    /* init settings */
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    44
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    45
    {
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    46
      val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    47
      if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    48
        error("User settings file already exists: " + etc_settings)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    49
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    50
      Isabelle_System.mkdirs(etc_settings.dir)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    51
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    52
      val components_base_path =
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    53
        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    54
        else Path.explode(components_base).expand
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    55
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    56
      val catalogs =
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    57
        if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    58
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    59
      val settings =
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    60
        catalogs.map(catalog =>
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    61
          "init_components " + File.bash_path(components_base_path) +
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    62
            " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    63
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    64
      File.write(etc_settings,
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    65
        "# generated by Isabelle " + Calendar.getInstance.getTime + "\n" +
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    66
        "#-*- shell-script -*- :mode=shellscript:\n\n" +
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    67
        Library.terminate_lines(settings))
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    68
    }
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    69
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    70
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    71
    /* components */
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    72
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    73
    isabelle("components -a").check.print_if(verbose)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    74
    isabelle("jedit -b" + (if (fresh) " -f" else "")).check.print_if(verbose)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    75
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    76
    isabelle("build " + File.bash_args(build_args))
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    77
  }
64021
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
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    80
  /* command line entry point */
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    81
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    82
  def main(args: Array[String])
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    83
  {
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    84
    Command_Line.tool0 {
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    85
      var allow = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    86
      var components_base = ""
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    87
      var isabelle_identifier = default_isabelle_identifier
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    88
      var fresh = false
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    89
      var nonfree = false
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    90
      var rev = default_rev
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    91
      var verbose = false
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    92
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    93
      val getopts = Getopts("""
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    94
Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    95
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
    96
  Options are:
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
    97
    -A           allow irreversible cleanup of REPOSITORY clone
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    98
    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
    99
    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   100
    -f           fresh build of Isabelle/Scala components (recommended)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   101
    -n           include nonfree components
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   102
    -r REV       update to revision (default: """ + default_rev + """)
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   103
    -v           verbose
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   104
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   105
  Build Isabelle sessions from the history of another REPOSITORY clone,
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   106
  passing ARGS directly to its isabelle build tool.
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   107
""",
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   108
        "A" -> (_ => allow = true),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   109
        "C:" -> (arg => components_base = arg),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   110
        "N:" -> (arg => isabelle_identifier = arg),
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   111
        "f" -> (_ => fresh = true),
64025
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   112
        "n" -> (_ => nonfree = true),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   113
        "r:" -> (arg => rev = arg),
ff4910ced9ba clarified command-line;
wenzelm
parents: 64023
diff changeset
   114
        "v" -> (_ => verbose = true))
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   115
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   116
      val more_args = getopts(args)
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   117
      val (root, build_args) =
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   118
        more_args match {
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   119
          case root :: build_args => (root, build_args)
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   120
          case _ => getopts.usage()
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   121
        }
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   122
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   123
      using(Mercurial.open_repository(Path.explode(root)))(hg =>
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   124
        {
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   125
          if (!allow)
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   126
            error("Repository " + hg + " will be cleaned thoroughly!\n" +
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   127
              "Provide option -A to allow this explicitly.")
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   128
64026
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   129
          val res =
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   130
            build_history(hg, rev = rev, isabelle_identifier = isabelle_identifier,
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   131
              components_base = components_base, fresh = fresh, nonfree = nonfree,
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   132
              verbose = verbose, build_args = build_args)
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   133
          res.print
cbecd26e063f clarified command line;
wenzelm
parents: 64025
diff changeset
   134
          if (!res.ok) sys.exit(res.rc)
64021
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   135
        })
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   136
    }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   137
  }
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents:
diff changeset
   138
}