src/Pure/Admin/isabelle_devel.scala
author wenzelm
Tue, 31 Oct 2023 17:24:19 +0100
changeset 78871 3b21101c5b6b
parent 77744 1398add8c414
permissions -rw-r--r--
clarified 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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74857
diff changeset
    10
object Isabelle_Devel {
78871
3b21101c5b6b clarified signature;
wenzelm
parents: 77744
diff changeset
    11
  val isabelle_devel: Path = Path.explode("~/html-data/devel")
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    12
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
  /* index */
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    15
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74857
diff changeset
    16
  def make_index(): Unit = {
71272
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    17
    val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    18
78871
3b21101c5b6b clarified signature;
wenzelm
parents: 77744
diff changeset
    19
    HTML.write_document(isabelle_devel, "index.html",
71272
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    20
      List(
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    21
        XML.Elem(Markup("meta",
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    22
          List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)),
1e7319957408 clarified website: redirect to isabelle-dev Phabricator Overview;
wenzelm
parents: 70105
diff changeset
    23
      List(HTML.link(redirect, HTML.text("Isabelle Development Resources"))))
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    24
  }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    25
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    26
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    27
  /* release snapshot */
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    28
75551
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75394
diff changeset
    29
  def release_snapshot(options: Options, rev: String, afp_rev: String,
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75394
diff changeset
    30
    progress: Progress = new Progress
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75394
diff changeset
    31
  ): Unit = {
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    32
    Isabelle_System.with_tmp_dir("isadist") { target_dir =>
78871
3b21101c5b6b clarified signature;
wenzelm
parents: 77744
diff changeset
    33
      Isabelle_System.update_directory(isabelle_devel + Path.explode("release_snapshot"),
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    34
        { website_dir =>
75551
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75394
diff changeset
    35
          val context = Build_Release.Release_Context(target_dir, progress = progress)
73629
a771807df752 support for existing release archive;
wenzelm
parents: 73625
diff changeset
    36
          Build_Release.build_release_archive(context, rev)
a771807df752 support for existing release archive;
wenzelm
parents: 73625
diff changeset
    37
          Build_Release.build_release(options, context, afp_rev = afp_rev,
73625
f8f065e20837 misc tuning and clarification: more explicit types Release_Context, Release_Archive;
wenzelm
parents: 73607
diff changeset
    38
            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
    39
            website = Some(website_dir))
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    40
        }
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    41
      )
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    42
    }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    43
  }
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    44
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    45
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    46
  /* present build status */
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65785
diff changeset
    47
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74857
diff changeset
    48
  def build_status(options: Options): Unit = {
78871
3b21101c5b6b clarified signature;
wenzelm
parents: 77744
diff changeset
    49
    Isabelle_System.update_directory(isabelle_devel + Path.explode("build_status"),
65854
db070951dfee include full ML statistics: max heap size;
wenzelm
parents: 65838
diff changeset
    50
      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
    51
  }
65770
fb8a7962f2ae clarified modules;
wenzelm
parents:
diff changeset
    52
}