src/Pure/Admin/isabelle_devel.scala
author wenzelm
Tue, 04 May 2021 20:02:08 +0200
changeset 73625 f8f065e20837
parent 73607 fc13738e1933
child 73629 a771807df752
permissions -rw-r--r--
misc tuning and clarification: more explicit types Release_Context, Release_Archive;
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
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71272
diff changeset
    17
  val root: Path = Path.explode("~/html-data/devel")
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71272
diff changeset
    18
  val cronjob_log: Path = 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
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71601
diff changeset
    23
  def make_index(): Unit =
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    24
  {
71272
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    25
    val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
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",
71272
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    28
      List(
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    29
        XML.Elem(Markup("meta",
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    30
          List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)),
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    31
      List(HTML.link(redirect, HTML.text("Isabelle Development Resources"))))
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    32
  }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    33
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    34
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    35
  /* release snapshot */
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    36
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    37
  def release_snapshot(options: Options, rev: String, afp_rev: String): Unit =
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    38
  {
73607
fc13738e1933 clarified command-line, following other build_XYZ tools;
wenzelm
parents: 73340
diff changeset
    39
    Isabelle_System.with_tmp_dir("isadist")(target_dir =>
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    40
      {
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    41
        Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    42
          website_dir =>
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    43
        {
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    44
          val context = Build_Release.Release_Context(target_dir)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    45
          val release_archive = Build_Release.build_release_archive(context, rev)
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    46
          Build_Release.build_release(options, context, release_archive, afp_rev = afp_rev,
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    47
            build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    48
            website = Some(website_dir))
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    49
        })
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    50
      })
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    51
  }
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    52
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    53
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    54
  /* maintain build_log database */
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    55
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71601
diff changeset
    56
  def build_log_database(options: Options, log_dirs: List[Path]): Unit =
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    57
  {
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    58
    val store = Build_Log.store(options)
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    59
    using(store.open_database())(db =>
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    60
    {
66047
3e8a897042d9 more robust: store important meta info before potential failure;
wenzelm
parents: 65854
diff changeset
    61
      store.update_database(db, log_dirs)
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    62
      store.update_database(db, log_dirs, ml_statistics = true)
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    63
      store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    64
    })
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    65
  }
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    66
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    67
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    68
  /* present build status */
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    69
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71601
diff changeset
    70
  def build_status(options: Options): Unit =
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    71
  {
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    72
    Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS),
65854
db070951dfee include full ML statistics: max heap size;
wenzelm
parents: 65838
diff changeset
    73
      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
    74
  }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    75
}