src/Pure/Admin/isabelle_devel.scala
author wenzelm
Tue, 09 May 2017 11:21:42 +0200
changeset 65785 6107504371fb
parent 65771 688a7dd22cbb
child 65793 96b4799a2e04
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/isabelle_devel.scala
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     3
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     4
Website for Isabelle development resources.
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     5
*/
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     6
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     8
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
     9
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    10
object Isabelle_Devel
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    11
{
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    12
  val root = Path.explode("~/html-data/devel")
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    13
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    14
  val RELEASE_SNAPSHOT = "release_snapshot"
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    15
  val BUILD_LOG_DB = "build_log.db"
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    16
  val BUILD_STATUS = "build_status"
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    17
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    18
  val standard_log_dirs =
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    19
    List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    20
65785
6107504371fb tuned signature;
wenzelm
parents: 65771
diff changeset
    21
  val build_status_dir = root + Path.explode(BUILD_STATUS)
6107504371fb tuned signature;
wenzelm
parents: 65771
diff changeset
    22
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    23
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    24
  /* index */
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    25
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    26
  def make_index()
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    27
  {
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    28
    val header = "Isabelle Development Resources"
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    29
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    30
    Isabelle_System.mkdirs(root)
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    31
    File.write(root + Path.explode("index.html"),
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    32
      HTML.output_document(
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    33
        List(HTML.title(header)),
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    34
        List(HTML.chapter(header),
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    35
          HTML.itemize(
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    36
            List(
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    37
              HTML.text("Isabelle nightly ") :::
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    38
              List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    39
              HTML.text(" (for all platforms)"),
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    40
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    41
              HTML.text("Isabelle ") :::
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    42
              List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    43
              HTML.text(" information"),
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    44
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    45
              HTML.text("Database with recent ") :::
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    46
              List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    47
              HTML.text(" information (e.g. for ") :::
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    48
              List(HTML.link("http://sqlitebrowser.org",
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    49
                List(HTML.code(HTML.text("sqlitebrowser"))))))))))
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    50
  }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    51
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    52
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    53
  /* release snapshot */
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    54
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    55
  def release_snapshot(
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    56
    rev: String = "",
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    57
    afp_rev: String = "",
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    58
    parallel_jobs: Int = 1,
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    59
    remote_mac: String = "")
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    60
  {
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    61
    Isabelle_System.with_tmp_dir("isadist")(base_dir =>
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    62
      {
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    63
        val release_snapshot_dir = root + Path.explode(RELEASE_SNAPSHOT)
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    64
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    65
        val new_snapshot = release_snapshot_dir.ext("new")
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    66
        val old_snapshot = release_snapshot_dir.ext("old")
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    67
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    68
        Isabelle_System.rm_tree(new_snapshot)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    69
        Isabelle_System.rm_tree(old_snapshot)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    70
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    71
        Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    72
          parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(new_snapshot))
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    73
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    74
        if (release_snapshot_dir.is_dir) File.move(release_snapshot_dir, old_snapshot)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    75
        File.move(new_snapshot, release_snapshot_dir)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    76
        Isabelle_System.rm_tree(old_snapshot)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    77
      })
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    78
  }
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    79
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    80
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    81
  /* maintain build_log database */
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    82
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    83
  def build_log_database(options: Options, log_dirs: List[Path] = standard_log_dirs)
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    84
  {
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    85
    val store = Build_Log.store(options)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    86
    using(store.open_database())(db =>
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    87
    {
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    88
      store.update_database(db, log_dirs, ml_statistics = true)
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    89
      store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    90
    })
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    91
  }
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    92
}