src/Pure/Admin/isabelle_devel.scala
author wenzelm
Wed, 05 Dec 2018 19:42:40 +0100
changeset 69401 7a1b7b737c02
parent 68229 18c36ac0acaa
child 69432 d072f3287ffa
permissions -rw-r--r--
eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala; more robust components and classpath via Other_Isabelle; updated macos_app to include full dmg template; misc tuning and clarification;
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 RELEASE_SNAPSHOT = "release_snapshot"
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    13
  val BUILD_LOG_DB = "build_log.db"
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    14
  val BUILD_STATUS = "build_status"
67854
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 66896
diff changeset
    15
  val CRONJOB_LOG = "cronjob-main.log"
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 66896
diff changeset
    16
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 66896
diff changeset
    17
  val root = Path.explode("~/html-data/devel")
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 66896
diff changeset
    18
  val cronjob_log = root + Path.basic(CRONJOB_LOG)
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    19
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    20
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    21
  /* index */
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    22
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    23
  def make_index()
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    24
  {
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    25
    val header = "Isabelle Development Resources"
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    26
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    27
    HTML.write_document(root, "index.html",
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    28
      List(HTML.title(header)),
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    29
      List(HTML.chapter(header),
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    30
        HTML.itemize(
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    31
          List(
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    32
            HTML.text("Isabelle nightly ") :::
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    33
            List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    34
            HTML.text(" (for all platforms)"),
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    35
68229
18c36ac0acaa tuned output;
wenzelm
parents: 68224
diff changeset
    36
            HTML.text("Cronjob ") ::: List(HTML.link(CRONJOB_LOG, HTML.text("log file"))),
18c36ac0acaa tuned output;
wenzelm
parents: 68224
diff changeset
    37
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    38
            HTML.text("Isabelle ") :::
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    39
            List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    40
            HTML.text(" information"),
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    41
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    42
            HTML.text("Database with recent ") :::
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    43
            List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    44
            HTML.text(" information (e.g. for ") :::
68224
1f7308050349 prefer HTTPS;
wenzelm
parents: 67854
diff changeset
    45
            List(HTML.link("https://sqlitebrowser.org",
65838
30c2d78b5d38 tuned signature;
wenzelm
parents: 65836
diff changeset
    46
              List(HTML.code(HTML.text("sqlitebrowser"))))) :::
68229
18c36ac0acaa tuned output;
wenzelm
parents: 68224
diff changeset
    47
            HTML.text(")")))))
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    48
  }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    49
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    50
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    51
  /* release snapshot */
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    52
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    53
  def release_snapshot(
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 68229
diff changeset
    54
    options: Options,
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    55
    rev: String = "",
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    56
    afp_rev: String = "",
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    57
    parallel_jobs: Int = 1,
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    58
    remote_mac: String = "")
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    59
  {
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    60
    Isabelle_System.with_tmp_dir("isadist")(base_dir =>
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    61
      {
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    62
        Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    63
          website_dir =>
69401
7a1b7b737c02 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala;
wenzelm
parents: 68229
diff changeset
    64
            Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev,
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    65
              parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir)))
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    66
      })
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    67
  }
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    68
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    69
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    70
  /* maintain build_log database */
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    71
66896
85e6748bf8b2 clarified signature;
wenzelm
parents: 66047
diff changeset
    72
  def build_log_database(options: Options, log_dirs: List[Path])
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    73
  {
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    74
    val store = Build_Log.store(options)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    75
    using(store.open_database())(db =>
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    76
    {
66047
3e8a897042d9 more robust: store important meta info before potential failure;
wenzelm
parents: 65854
diff changeset
    77
      store.update_database(db, log_dirs)
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    78
      store.update_database(db, log_dirs, ml_statistics = true)
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    79
      store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    80
    })
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    81
  }
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    82
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    83
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    84
  /* present build status */
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    85
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    86
  def build_status(options: Options)
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    87
  {
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    88
    Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS),
65854
db070951dfee include full ML statistics: max heap size;
wenzelm
parents: 65838
diff changeset
    89
      dir => Build_Status.build_status(options, target_dir = dir, ml_statistics = true))
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    90
  }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    91
}