src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Tue, 30 Jan 2024 12:48:27 +0100
changeset 79545 b8a6b2ec85a2
parent 79539 24d6c4165b23
child 79546 c9774306a879
permissions -rw-r--r--
more robust message;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/isabelle_cronjob.scala
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     3
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     4
Main entry point for administrative cronjob at TUM.
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     5
*/
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     6
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     7
package isabelle
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     8
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     9
67854
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    10
import java.nio.file.Files
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    11
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    12
import scala.annotation.tailrec
78990
f728be354ffb tuned: avoid recursion;
wenzelm
parents: 78989
diff changeset
    13
import scala.collection.mutable
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    14
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    15
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
    16
object Isabelle_Cronjob {
66897
wenzelm
parents: 66896
diff changeset
    17
  /* global resources: owned by main cronjob */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    18
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    19
  val backup = "lxbroy10:cronjob"
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
    20
  val main_dir: Path = Path.explode("~/cronjob")
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
    21
  val main_state_file: Path = main_dir + Path.explode("run/main.state")
75551
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75520
diff changeset
    22
  val build_release_log: Path = main_dir + Path.explode("run/build_release.log")
78877
45d570945fe4 more detailed progress for build_log_database, to see better what happens when;
wenzelm
parents: 78873
diff changeset
    23
  val build_log_database_log: Path = main_dir + Path.explode("run/build_log_database.log")
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
    24
  val current_log: Path = main_dir + Path.explode("run/main.log")  // owned by log service
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
    25
  val cumulative_log: Path = main_dir + Path.explode("log/main.log")  // owned by log service
78997
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
    26
  val isabelle_repos: Path = main_dir + Path.explode("isabelle")
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
    27
  val afp_repos: Path = main_dir + Path.explode("AFP")
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    28
78997
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
    29
  lazy val isabelle_hg: Mercurial.Repository = Mercurial.self_repository()
78995
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
    30
  lazy val afp_hg: Mercurial.Repository = Mercurial.repository(afp_repos)
64236
358f9ff08681 discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
wenzelm
parents: 64235
diff changeset
    31
72559
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    32
  val mailman_archives_dir = Path.explode("~/cronjob/Mailman")
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    33
66896
85e6748bf8b2 clarified signature;
wenzelm
parents: 66895
diff changeset
    34
  val build_log_dirs =
85e6748bf8b2 clarified signature;
wenzelm
parents: 66895
diff changeset
    35
    List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
85e6748bf8b2 clarified signature;
wenzelm
parents: 66895
diff changeset
    36
78872
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    37
  val isabelle_devel: Path = Path.explode("~/html-data/devel")
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    38
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    39
64192
wenzelm
parents: 64187
diff changeset
    40
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    41
  /** logger tasks **/
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    42
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    43
  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    44
64192
wenzelm
parents: 64187
diff changeset
    45
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    46
  /* init and exit */
64192
wenzelm
parents: 64187
diff changeset
    47
78997
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
    48
  def get_rev(): String = isabelle_hg.id()
78995
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
    49
  def get_afp_rev(): String = afp_hg.id()
67753
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    50
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
    51
  val init: Logger_Task =
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    52
    Logger_Task("init",
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    53
      { logger =>
78872
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    54
        val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    55
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    56
        HTML.write_document(isabelle_devel, "index.html",
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    57
          List(
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    58
            XML.Elem(Markup("meta",
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    59
              List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)),
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    60
          List(HTML.link(redirect, HTML.text("Isabelle Development Resources"))))
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    61
73611
cc36841eeff6 clarified signature: more operations;
wenzelm
parents: 73608
diff changeset
    62
        Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos)
64192
wenzelm
parents: 64187
diff changeset
    63
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    64
        File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
67753
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    65
          Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    66
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    67
        Isabelle_System.bash(
77788
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77751
diff changeset
    68
          File.bash_path(Component_Rsync.local_program) +
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77751
diff changeset
    69
            """ -a --include="*/" --include="plain_identify*" --exclude="*" """ +
69199
e5e4de2b93d9 more robust: allow log to be a symlink;
wenzelm
parents: 68650
diff changeset
    70
            Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
67854
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    71
78872
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
    72
        val cronjob_log = isabelle_devel + Path.basic("cronjob-main.log")
78871
3b21101c5b6b clarified signature;
wenzelm
parents: 78870
diff changeset
    73
        if (!cronjob_log.is_file) {
3b21101c5b6b clarified signature;
wenzelm
parents: 78870
diff changeset
    74
          Files.createSymbolicLink(cronjob_log.java_path, current_log.java_path)
78094
wenzelm
parents: 77788
diff changeset
    75
        }
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    76
      })
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    77
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
    78
  val exit: Logger_Task =
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    79
    Logger_Task("exit",
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    80
      { logger =>
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    81
        Isabelle_System.bash(
77788
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77751
diff changeset
    82
          File.bash_path(Component_Rsync.local_program) +
c2ce9ac85859 use remote copy of locally installed rsync component: for uniform version and options;
wenzelm
parents: 77751
diff changeset
    83
            " -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
67769
20c262dcfdf5 proper target directory;
wenzelm
parents: 67766
diff changeset
    84
            .check
67751
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    85
      })
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    86
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    87
72559
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    88
  /* Mailman archives */
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    89
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    90
  val mailman_archives: Logger_Task =
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    91
    Logger_Task("mailman_archives",
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    92
      { logger =>
74921
74655fd58f8e more mailing list content;
wenzelm
parents: 74907
diff changeset
    93
        Mailman.Isabelle_Users.download(mailman_archives_dir)
74655fd58f8e more mailing list content;
wenzelm
parents: 74907
diff changeset
    94
        Mailman.Isabelle_Dev.download(mailman_archives_dir)
72559
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    95
      })
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    96
274c9986e55b maintain Isabelle mailing list archives;
wenzelm
parents: 72483
diff changeset
    97
67751
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    98
  /* build release */
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    99
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
   100
  val build_release: Logger_Task =
75551
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75520
diff changeset
   101
    Logger_Task("build_release", { logger =>
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75520
diff changeset
   102
      build_release_log.file.delete
78872
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   103
      val rev = get_rev()
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   104
      val afp_rev = get_afp_rev()
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   105
      val progress = new File_Progress(build_release_log)
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   106
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   107
      Isabelle_System.with_tmp_dir("isadist") { target_dir =>
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   108
        Isabelle_System.update_directory(isabelle_devel + Path.explode("release_snapshot"),
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   109
          { website_dir =>
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   110
            val context = Build_Release.Release_Context(target_dir, progress = progress)
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   111
            Build_Release.build_release_archive(context, rev)
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   112
            Build_Release.build_release(logger.options, context, afp_rev = afp_rev,
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   113
              build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   114
              website = Some(website_dir))
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   115
          }
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   116
        )
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   117
      }
75551
4103b945c7b5 more informative release_snapshot, to see better where the cronjob fails;
wenzelm
parents: 75520
diff changeset
   118
    })
64192
wenzelm
parents: 64187
diff changeset
   119
wenzelm
parents: 64187
diff changeset
   120
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   121
  /* remote build_history */
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   122
64409
70c87ca55f2c tuned signature -- more friendly for experimentation;
wenzelm
parents: 64405
diff changeset
   123
  sealed case class Remote_Build(
65764
1af6d544c2a3 clarified description vs. file name;
wenzelm
parents: 65747
diff changeset
   124
    description: String,
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   125
    host: String,
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   126
    user: String = "",
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 65063
diff changeset
   127
    port: Int = 0,
65789
fccd7be5fa55 enter deeper into history;
wenzelm
parents: 65785
diff changeset
   128
    history: Int = 0,
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   129
    history_base: String = "build_history_base",
77132
53ce5a39c987 more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";
wenzelm
parents: 77131
diff changeset
   130
    components_base: String = Components.dynamic_components_base,
77135
515b6aaede32 enable clean_components by default: it saves a lot of local disk space, notably on virtual nodes;
wenzelm
parents: 77133
diff changeset
   131
    clean_components: Boolean = true,
71993
088e3aa85250 clarified signature;
wenzelm
parents: 71983
diff changeset
   132
    java_heap: String = "",
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   133
    options: String = "",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   134
    args: String = "",
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   135
    afp: Boolean = false,
69693
06153e2e0cdb more official AFP.groups;
wenzelm
parents: 69432
diff changeset
   136
    bulky: Boolean = false,
67075
eada9bd5fff2 avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries;
wenzelm
parents: 67070
diff changeset
   137
    more_hosts: List[String] = Nil,
75968
5a782ca6872b tuned signature: build_log db is specific to PostgreSQL;
wenzelm
parents: 75954
diff changeset
   138
    detect: PostgreSQL.Source = "",
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   139
    count: () => Int = () => 1
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   140
  ) {
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   141
    def active(): Boolean = count() > 0
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   142
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76027
diff changeset
   143
    def open_session(options: Options): SSH.Session =
76123
4a0b7151fedc removed remains of proxy_host management: delegated to .ssh/config;
wenzelm
parents: 76122
diff changeset
   144
      SSH.open_session(options, host = host, user = user, port = port)
67750
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   145
75968
5a782ca6872b tuned signature: build_log db is specific to PostgreSQL;
wenzelm
parents: 75954
diff changeset
   146
    def sql: PostgreSQL.Source =
77370
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
   147
      SQL.and(
77375
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
   148
        Build_Log.Prop.build_engine.equal(Build_History.engine),
324f5821a4a4 clarified signature: more concise operations;
wenzelm
parents: 77370
diff changeset
   149
        Build_Log.Prop.build_host.member(host :: more_hosts),
77370
47c2ac81ddd4 clarified signature: more robust operations;
wenzelm
parents: 77368
diff changeset
   150
        if_proper(detect, SQL.enclose(detect)))
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   151
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   152
    def profile: Build_Status.Profile =
69693
06153e2e0cdb more official AFP.groups;
wenzelm
parents: 69432
diff changeset
   153
      Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   154
78997
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
   155
    def history(db: SQL.Database, days: Int = 0): Build_Log.History = {
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
   156
      val rev = get_rev()
67753
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
   157
      val afp_rev = if (afp) Some(get_afp_rev()) else None
78997
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
   158
      val base_rev = isabelle_hg.id(history_base)
39fb869160d6 clarified isabelle_hg (again, see b9d59669904a);
wenzelm
parents: 78996
diff changeset
   159
      val filter_nodes = isabelle_hg.graph().all_succs(List(base_rev)).toSet
78995
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
   160
      Build_Log.History.retrieve(db, days, rev, afp_rev, sql,
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
   161
        entry => filter_nodes(entry.isabelle_version))
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
   162
    }
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
   163
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
   164
    def pick(options: Options): Option[(String, Option[String])] = {
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   165
      val store = Build_Log.store(options)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   166
      using(store.open_database()) { db =>
78991
ae2f5fd0bb5d clarified signature and modules: more explicit Build_Log.History;
wenzelm
parents: 78990
diff changeset
   167
        def get(days: Int, gap: Int): Option[(String, Option[String])] = {
78995
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
   168
          val runs = history(db, days = days).unknown_runs(filter = run => run.length >= gap)
78991
ae2f5fd0bb5d clarified signature and modules: more explicit Build_Log.History;
wenzelm
parents: 78990
diff changeset
   169
          Build_Log.History.Run.longest(runs).median.map(_.versions)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   170
        }
78991
ae2f5fd0bb5d clarified signature and modules: more explicit Build_Log.History;
wenzelm
parents: 78990
diff changeset
   171
        get(options.int("build_log_history") max history, 2) orElse
ae2f5fd0bb5d clarified signature and modules: more explicit Build_Log.History;
wenzelm
parents: 78990
diff changeset
   172
        get(300, 8) orElse
ae2f5fd0bb5d clarified signature and modules: more explicit Build_Log.History;
wenzelm
parents: 78990
diff changeset
   173
        get(3000, 32) orElse
ae2f5fd0bb5d clarified signature and modules: more explicit Build_Log.History;
wenzelm
parents: 78990
diff changeset
   174
        get(0, 1)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   175
      }
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   176
    }
73239
27dc8f899147 clarified signature;
wenzelm
parents: 73185
diff changeset
   177
27dc8f899147 clarified signature;
wenzelm
parents: 73185
diff changeset
   178
    def build_history_options: String =
27dc8f899147 clarified signature;
wenzelm
parents: 73185
diff changeset
   179
      " -h " + Bash.string(host) + " " +
77479
wenzelm
parents: 77375
diff changeset
   180
      if_proper(java_heap,
wenzelm
parents: 77375
diff changeset
   181
        "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + java_heap + "\"' ") +
wenzelm
parents: 77375
diff changeset
   182
      options
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   183
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   184
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   185
  val remote_builds_old: List[Remote_Build] =
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   186
    List(
79535
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   187
      Remote_Build("Linux A", "augsburg1",
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   188
        options = "-m32 -B -M4" +
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   189
          " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   190
          " -e ISABELLE_GHC_SETUP=true" +
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   191
          " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" +
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   192
          " -e ISABELLE_SMLNJ=sml" +
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   193
          " -e ISABELLE_SWIPL=swipl",
9ecb62e10621 disable test on "augsburg1": machine will be dismantled;
wenzelm
parents: 79066
diff changeset
   194
        args = "-a -d '~~/src/Benchmarks'"),
75954
7c72091abd55 disable laramac01 for now: system update pending;
wenzelm
parents: 75551
diff changeset
   195
      Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius",
7c72091abd55 disable laramac01 for now: system update pending;
wenzelm
parents: 75551
diff changeset
   196
        options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
7c72091abd55 disable laramac01 for now: system update pending;
wenzelm
parents: 75551
diff changeset
   197
        args = "-a -d '~~/src/Benchmarks'"),
73879
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   198
      Remote_Build("Linux A", "i21of4", user = "i21isatest",
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   199
        options = "-m32 -M1x4,2,4" +
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   200
          " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   201
          " -e ISABELLE_GHC_SETUP=true" +
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   202
          " -e ISABELLE_MLTON=mlton" +
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   203
          " -e ISABELLE_SMLNJ=sml" +
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   204
          " -e ISABELLE_SWIPL=swipl",
0db0cd462163 discontinue i21of4 (old Apple hardware);
wenzelm
parents: 73704
diff changeset
   205
        args = "-a -d '~~/src/Benchmarks'"),
72391
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   206
      Remote_Build("Linux A", "lxbroy9",
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   207
        java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing"),
78906
004b39bf06a5 clarified exploration of history: more uniform options;
wenzelm
parents: 78905
diff changeset
   208
      Remote_Build("Linux Benchmarks", "lxbroy5", history = 90,
72391
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   209
        java_heap = "2g",
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   210
        options = "-m32 -B -M1x2,2 -t Benchmarks" +
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   211
          " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   212
          " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" +
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   213
          " -e ISABELLE_SWIPL=swipl",
37c1fbcc88d0 discontinued old machines;
wenzelm
parents: 72390
diff changeset
   214
        args = "-N -a -d '~~/src/Benchmarks'",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   215
        detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("Benchmarks")),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   216
      Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3",
72390
ed95980cf198 updated tests for macOS 10.14 Mojave;
wenzelm
parents: 72376
diff changeset
   217
        options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
75520
65ecf4c5b868 removed obsolete self_update: always enabled, notably on lxbroy10 which is the only shared-home system (and still requires current isabelle_self);
wenzelm
parents: 75518
diff changeset
   218
        args = "-a -d '~~/src/Benchmarks'"),
65ecf4c5b868 removed obsolete self_update: always enabled, notably on lxbroy10 which is the only shared-home system (and still requires current isabelle_self);
wenzelm
parents: 75518
diff changeset
   219
      Remote_Build("AFP old bulky", "lrzcloud1",
70757
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70477
diff changeset
   220
        options = "-m64 -M6 -U30000 -s10 -t AFP",
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70477
diff changeset
   221
        args = "-g large -g slow",
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70477
diff changeset
   222
        afp = true,
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70477
diff changeset
   223
        bulky = true,
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   224
        detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
72073
f56522a44564 clarified names;
wenzelm
parents: 71999
diff changeset
   225
      Remote_Build("AFP old", "lxbroy7",
69693
06153e2e0cdb more official AFP.groups;
wenzelm
parents: 69432
diff changeset
   226
          args = "-N -X large -X slow",
67608
1b2be3666b89 retain remote_builds_old for build_status;
wenzelm
parents: 67607
diff changeset
   227
          afp = true,
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   228
          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   229
      Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   230
        history_base = "37074e22e8be",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   231
        options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   232
        args = "-N -g timing",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   233
        detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7") + " AND " +
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   234
          Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
66931
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   235
      Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   236
        history_base = "a9d5b59c3e12",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   237
        options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   238
        args = "-N -g timing",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   239
        detect =
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   240
          Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
66931
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   241
          Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   242
      Remote_Build("Poly/ML 5.7 macOS", "macbroy2",
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   243
        history_base = "37074e22e8be",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   244
        options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   245
        args = "-a",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   246
        detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7")),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   247
      Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2",
66931
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   248
        history_base = "a9d5b59c3e12",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   249
        options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   250
        args = "-a",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   251
        detect =
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   252
          Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   253
          Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   254
      Remote_Build("macOS", "macbroy2",
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   255
        options = "-m32 -M8" +
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   256
          " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   257
          " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   258
          " -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" +
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   259
          " -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml" +
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   260
          " -p pide_session=false",
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   261
        args = "-a",
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   262
        detect = Build_Log.Prop.build_tags.undefined,
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   263
        history_base = "2c0f24e927dd"),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   264
      Remote_Build("macOS, quick_and_dirty", "macbroy2",
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   265
        options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   266
        detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"),
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   267
        history_base = "2c0f24e927dd"),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   268
      Remote_Build("macOS, skip_proofs", "macbroy2",
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   269
        options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   270
        detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   271
        history_base = "2c0f24e927dd"),
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   272
      Remote_Build("Poly/ML test", "lxbroy8",
65843
d547173212d2 proper init_settings for init_component (before generated ML_OPTIONS etc.);
wenzelm
parents: 65840
diff changeset
   273
        options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   274
        args = "-N -g timing",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   275
        detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-test")),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   276
      Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   277
        detect = Build_Log.Prop.build_start.toString + " > date '2017-03-03'"),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   278
      Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"),
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   279
      Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   280
        detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) :::
71974
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   281
      {
78094
wenzelm
parents: 77788
diff changeset
   282
        for ((n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")))
71974
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   283
        yield {
72073
f56522a44564 clarified names;
wenzelm
parents: 71999
diff changeset
   284
          Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail,
71974
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   285
            options = "-m32 -M1x2 -t AFP -P" + n +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   286
              " -e ISABELLE_GHC=ghc" +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   287
              " -e ISABELLE_MLTON=mlton" +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   288
              " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   289
              " -e ISABELLE_SMLNJ=sml",
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   290
            args = "-N -X large -X slow",
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   291
            afp = true,
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   292
            detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"))
71974
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   293
        }
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71761
diff changeset
   294
      }
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   295
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   296
  val remote_builds1: List[List[Remote_Build]] = {
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   297
    List(
79536
d39976404aa7 routine build + test for linux_arm;
wenzelm
parents: 79535
diff changeset
   298
      List(Remote_Build("Linux (ARM)", "server-arm",
79538
d17d566d86c0 proper history_base for linux_arm;
wenzelm
parents: 79536
diff changeset
   299
        history_base = "build_history_base_arm",
79539
24d6c4165b23 proper test options;
wenzelm
parents: 79538
diff changeset
   300
        options = "-m32 -B -M1x2 -p timeout_scale=2" +
24d6c4165b23 proper test options;
wenzelm
parents: 79538
diff changeset
   301
          " -e ISABELLE_SWIPL=swipl",
24d6c4165b23 proper test options;
wenzelm
parents: 79538
diff changeset
   302
        args = "-a -d '~~/src/Benchmarks'")),
78906
004b39bf06a5 clarified exploration of history: more uniform options;
wenzelm
parents: 78905
diff changeset
   303
      List(Remote_Build("Linux B", "lxbroy10", history = 90,
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   304
        options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   305
      List(
78777
3b424f9cd5eb update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;
wenzelm
parents: 78771
diff changeset
   306
        Remote_Build("macOS 11 Big Sur (Intel)", "mini1",
73141
13bd167f4d97 more official support for macOS 11.1 Big Sur;
wenzelm
parents: 72997
diff changeset
   307
          options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
13bd167f4d97 more official support for macOS 11.1 Big Sur;
wenzelm
parents: 72997
diff changeset
   308
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
13bd167f4d97 more official support for macOS 11.1 Big Sur;
wenzelm
parents: 72997
diff changeset
   309
            " -e ISABELLE_GHC_SETUP=true" +
76181
d27ed188e0c4 support for ISABELLE_MLTON_OPTIONS, notably for Ubuntu 22.04 with external mlton executable;
wenzelm
parents: 76123
diff changeset
   310
            " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" +
73141
13bd167f4d97 more official support for macOS 11.1 Big Sur;
wenzelm
parents: 72997
diff changeset
   311
            " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
13bd167f4d97 more official support for macOS 11.1 Big Sur;
wenzelm
parents: 72997
diff changeset
   312
            " -e ISABELLE_SWIPL=/usr/local/bin/swipl",
75520
65ecf4c5b868 removed obsolete self_update: always enabled, notably on lxbroy10 which is the only shared-home system (and still requires current isabelle_self);
wenzelm
parents: 75518
diff changeset
   313
          args = "-a -d '~~/src/Benchmarks'")),
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   314
      List(
78905
wenzelm
parents: 78904
diff changeset
   315
        Remote_Build("macOS 14 Sonoma (ARM)", "studio1-sonoma",
78999
769e850bb1d7 prefer symbolic build_history_base_arm;
wenzelm
parents: 78998
diff changeset
   316
          history_base = "build_history_base_arm",
78905
wenzelm
parents: 78904
diff changeset
   317
          options = "-m32 -B -M1x4,2x4,4x2,8 -p pide_session=false" +
wenzelm
parents: 78904
diff changeset
   318
            " -e ISABELLE_GHC_SETUP=true" +
wenzelm
parents: 78904
diff changeset
   319
            " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
wenzelm
parents: 78904
diff changeset
   320
            " -e ISABELLE_SWIPL=/opt/homebrew/bin/swipl",
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   321
          args = "-a -d '~~/src/Benchmarks'",
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   322
          count = () => 2)),
78784
fb46520b9b7c proper parallel build tasks;
wenzelm
parents: 78783
diff changeset
   323
      List(
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   324
        Remote_Build("macOS, quick_and_dirty", "mini2",
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   325
          options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
75520
65ecf4c5b868 removed obsolete self_update: always enabled, notably on lxbroy10 which is the only shared-home system (and still requires current isabelle_self);
wenzelm
parents: 75518
diff changeset
   326
          args = "-a -o quick_and_dirty",
78744
a11c461a1a3a mini2 is not active due to upgrade;
wenzelm
parents: 78514
diff changeset
   327
          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"),
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   328
          count = () => 0),
72894
bd2269b6cd99 updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents: 72893
diff changeset
   329
        Remote_Build("macOS, skip_proofs", "mini2",
72893
fbdadf5760c2 updated test machines;
wenzelm
parents: 72559
diff changeset
   330
          options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
78744
a11c461a1a3a mini2 is not active due to upgrade;
wenzelm
parents: 78514
diff changeset
   331
          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   332
          count = () => 0)),
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   333
      List(
78905
wenzelm
parents: 78904
diff changeset
   334
        Remote_Build("macOS 13 Ventura (ARM)", "mini3",
78999
769e850bb1d7 prefer symbolic build_history_base_arm;
wenzelm
parents: 78998
diff changeset
   335
          history_base = "build_history_base_arm",
78905
wenzelm
parents: 78904
diff changeset
   336
          options = "-a -m32 -B -M1x4,2x2,4 -p pide_session=false" +
wenzelm
parents: 78904
diff changeset
   337
            " -e ISABELLE_GHC_SETUP=true" +
wenzelm
parents: 78904
diff changeset
   338
            " -e ISABELLE_MLTON=/opt/homebrew/bin/mlton -e ISABELLE_MLTON_OPTIONS=" +
wenzelm
parents: 78904
diff changeset
   339
            " -e ISABELLE_SWIPL=/opt/homebrew/bin/swipl",
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   340
          args = "-a -d '~~/src/Benchmarks'",
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   341
          count = () => 3)),
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   342
      List(
78906
004b39bf06a5 clarified exploration of history: more uniform options;
wenzelm
parents: 78905
diff changeset
   343
        Remote_Build("Windows", "vmnipkow9", history = 90,
77132
53ce5a39c987 more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";
wenzelm
parents: 77131
diff changeset
   344
          components_base = "/cygdrive/d/isatest/contrib",
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   345
          options = "-m32 -M4" +
69931
31ee094dea3d prefer ISABELLE_OCAML_SETUP: Cygwin lacks libzarith;
wenzelm
parents: 69927
diff changeset
   346
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
69952
385458b950e1 clarified GHC and OCaml test setup;
wenzelm
parents: 69937
diff changeset
   347
            " -e ISABELLE_GHC_SETUP=true" +
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   348
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   349
          args = "-a",
72317
d24a8cea343b proper Windows 32bit platform;
wenzelm
parents: 72074
diff changeset
   350
          detect =
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   351
            Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " +
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   352
            Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows"),
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   353
          count = () => 2),
78906
004b39bf06a5 clarified exploration of history: more uniform options;
wenzelm
parents: 78905
diff changeset
   354
        Remote_Build("Windows", "vmnipkow9", history = 90,
77132
53ce5a39c987 more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";
wenzelm
parents: 77131
diff changeset
   355
          components_base = "/cygdrive/d/isatest/contrib",
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   356
          options = "-m64 -M4" +
78918
8378354bbdad avoid option -C: free this latter for build-related configuration;
wenzelm
parents: 78907
diff changeset
   357
            " -S /cygdrive/d/isatest/contrib" +
69931
31ee094dea3d prefer ISABELLE_OCAML_SETUP: Cygwin lacks libzarith;
wenzelm
parents: 69927
diff changeset
   358
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
69952
385458b950e1 clarified GHC and OCaml test setup;
wenzelm
parents: 69937
diff changeset
   359
            " -e ISABELLE_GHC_SETUP=true" +
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   360
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   361
          args = "-a",
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   362
          detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows"),
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   363
          count = () => 2))
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   364
    )
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   365
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   366
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   367
  val remote_builds2: List[List[Remote_Build]] =
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   368
    List(
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   369
      List(
78451
c32b8d5a9e07 show more build history for AFP;
wenzelm
parents: 78257
diff changeset
   370
        Remote_Build("AFP", "lrzcloud2", history = 120,
71993
088e3aa85250 clarified signature;
wenzelm
parents: 71983
diff changeset
   371
          java_heap = "8g",
77171
e0e9f1b4c844 less ambitious parallelism: avoid exhaustion of memory (40GB total);
wenzelm
parents: 77163
diff changeset
   372
          options = "-m32 -M1x5 -t AFP" +
70467
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70466
diff changeset
   373
            " -e ISABELLE_GHC=ghc" +
76181
d27ed188e0c4 support for ISABELLE_MLTON_OPTIONS, notably for Ubuntu 22.04 with external mlton executable;
wenzelm
parents: 76123
diff changeset
   374
            " -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" +
70467
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70466
diff changeset
   375
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70466
diff changeset
   376
            " -e ISABELLE_SMLNJ=sml",
70477
90acc6ce5beb proper build options;
wenzelm
parents: 70467
diff changeset
   377
          args = "-a -X large -X slow",
70467
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70466
diff changeset
   378
          afp = true,
77163
7ceed24c88dc alternate AFP tests on lrzcloud2, to fit better into one day;
wenzelm
parents: 77135
diff changeset
   379
          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   380
          count = () => if (Date.now().unix_epoch_day % 2 == 0) 1 else 0),
76123
4a0b7151fedc removed remains of proxy_host management: delegated to .ssh/config;
wenzelm
parents: 76122
diff changeset
   381
        Remote_Build("AFP", "lrzcloud2",
71993
088e3aa85250 clarified signature;
wenzelm
parents: 71983
diff changeset
   382
          java_heap = "8g",
088e3aa85250 clarified signature;
wenzelm
parents: 71983
diff changeset
   383
          options = "-m64 -M8 -U30000 -s10 -t AFP",
70467
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70466
diff changeset
   384
          args = "-g large -g slow",
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70466
diff changeset
   385
          afp = true,
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70466
diff changeset
   386
          bulky = true,
77163
7ceed24c88dc alternate AFP tests on lrzcloud2, to fit better into one day;
wenzelm
parents: 77135
diff changeset
   387
          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   388
          count = () => if (Date.now().unix_epoch_day % 2 == 1) 1 else 0)))
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   389
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   390
  def remote_build_history(
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   391
    rev: String,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   392
    afp_rev: Option[String],
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   393
    i: Int,
78885
9d0faaa77e5d proper progress (see also 45d570945fe4);
wenzelm
parents: 78877
diff changeset
   394
    r: Remote_Build,
9d0faaa77e5d proper progress (see also 45d570945fe4);
wenzelm
parents: 78877
diff changeset
   395
    progress: Progress = new Progress
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   396
  ) : Logger_Task = {
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   397
    val task_name = "build_history-" + r.host
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   398
    Logger_Task(task_name,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   399
      { logger =>
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76027
diff changeset
   400
        using(r.open_session(logger.options)) { ssh =>
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   401
          val results =
75518
cb4af8c6152f clarified remote vs. local build_history: operate on hg_sync directory instead of repository;
wenzelm
parents: 75498
diff changeset
   402
            Build_History.remote_build(ssh,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   403
              isabelle_repos,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   404
              isabelle_repos.ext(r.host),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   405
              isabelle_identifier = "cronjob_build_history",
77132
53ce5a39c987 more uniform components context for the managing "self_isabelle" and the managed "other_isabelle";
wenzelm
parents: 77131
diff changeset
   406
              components_base = r.components_base,
77131
c8d34e74a12b tuned signature;
wenzelm
parents: 77128
diff changeset
   407
              clean_platform = r.clean_components,
77125
158790217aa9 more options to manage resolved components;
wenzelm
parents: 77083
diff changeset
   408
              clean_archives = r.clean_components,
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   409
              rev = rev,
75518
cb4af8c6152f clarified remote vs. local build_history: operate on hg_sync directory instead of repository;
wenzelm
parents: 75498
diff changeset
   410
              afp_repos = if (afp_rev.isDefined) Some(afp_repos) else None,
cb4af8c6152f clarified remote vs. local build_history: operate on hg_sync directory instead of repository;
wenzelm
parents: 75498
diff changeset
   411
              afp_rev = afp_rev.getOrElse(""),
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   412
              options =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   413
                " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
77083
092449efcb0e clarified defaults (see also b310b93563f6);
wenzelm
parents: 76365
diff changeset
   414
                " -f " + r.build_history_options,
78860
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   415
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   416
              args = "-o timeout=10800 " + r.args)
64346
5f49765a25ec process results immediately;
wenzelm
parents: 64338
diff changeset
   417
78860
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   418
          val log_files =
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   419
            for ((log_name, bytes) <- results) yield {
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   420
              val log_file = logger.log_dir + Path.explode(log_name)
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   421
              logger.log(Date.now(), log_name)
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   422
              Bytes.write(log_file, bytes)
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   423
              log_file
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   424
            }
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   425
78885
9d0faaa77e5d proper progress (see also 45d570945fe4);
wenzelm
parents: 78877
diff changeset
   426
          Build_Log.build_log_database(logger.options, log_files,
9d0faaa77e5d proper progress (see also 45d570945fe4);
wenzelm
parents: 78877
diff changeset
   427
            progress = progress, ml_statistics = true)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   428
        }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   429
      })
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   430
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   431
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   432
  val build_status_profiles: List[Build_Status.Profile] =
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   433
    (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   434
65746
dead16007097 present build status;
wenzelm
parents: 65736
diff changeset
   435
64192
wenzelm
parents: 64187
diff changeset
   436
wenzelm
parents: 64187
diff changeset
   437
  /** task logging **/
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   438
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   439
  object Log_Service {
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71684
diff changeset
   440
    def apply(options: Options, progress: Progress = new Progress): Log_Service =
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76027
diff changeset
   441
      new Log_Service(options, progress)
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   442
  }
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   443
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76027
diff changeset
   444
  class Log_Service private(val options: Options, progress: Progress) {
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   445
    current_log.file.delete
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   446
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   447
    private val thread: Consumer_Thread[String] =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   448
      Consumer_Thread.fork("cronjob: logger", daemon = true)(
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   449
        consume =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   450
          { (text: String) =>
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   451
            // critical
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   452
            File.append(current_log, text + "\n")
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   453
            File.append(cumulative_log, text + "\n")
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   454
            progress.echo(text)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   455
            true
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   456
          })
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   457
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73313
diff changeset
   458
    def shutdown(): Unit = { thread.shutdown() }
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   459
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71565
diff changeset
   460
    val hostname: String = Isabelle_System.hostname()
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   461
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   462
    def log(date: Date, task_name: String, msg: String): Unit =
78989
wenzelm
parents: 78918
diff changeset
   463
      if (task_name.nonEmpty) {
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   464
        thread.send(
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   465
          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
76365
24e951a8a318 tuned: more robust Scala syntax;
wenzelm
parents: 76265
diff changeset
   466
      }
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   467
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   468
    def start_logger(start_date: Date, task_name: String): Logger =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   469
      new Logger(this, start_date, task_name)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   470
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   471
    def run_task(start_date: Date, task: Logger_Task): Unit = {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   472
      val logger = start_logger(start_date, task.name)
78768
280a228dc2f1 prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
wenzelm
parents: 78744
diff changeset
   473
      val res = Exn.result { task.body(logger) }
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   474
      val end_date = Date.now()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   475
      val err =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   476
        res match {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   477
          case Exn.Res(_) => None
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   478
          case Exn.Exn(exn) =>
79545
b8a6b2ec85a2 more robust message;
wenzelm
parents: 79539
diff changeset
   479
            Output.writeln("Exception trace for " + quote(task.name) + ":\n" + Exn.trace(exn))
66923
wenzelm
parents: 66903
diff changeset
   480
            val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   481
            Some(first_line)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   482
        }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   483
      logger.log_end(end_date, err)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   484
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   485
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   486
    def fork_task(start_date: Date, task: Logger_Task): Task =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   487
      new Task(task.name, run_task(start_date, task))
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   488
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   489
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   490
  class Logger private[Isabelle_Cronjob](
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76027
diff changeset
   491
    log_service: Log_Service,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   492
    val start_date: Date,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   493
    val task_name: String
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   494
  ) {
76115
f17393e21388 clarified signature: discontinue somewhat pointless SSH.Context;
wenzelm
parents: 76027
diff changeset
   495
    def options: Options = log_service.options
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   496
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   497
    def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   498
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   499
    def log_end(end_date: Date, err: Option[String]): Unit = {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   500
      val elapsed_time = end_date.time - start_date.time
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   501
      val msg =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   502
        (if (err.isEmpty) "finished" else "ERROR " + err.get) +
64197
c43dedbb8118 tuned message;
wenzelm
parents: 64195
diff changeset
   503
        (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   504
      log(end_date, msg)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   505
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   506
78993
93abe74fe16f tuned signature: fewer warnings in IntelliJ IDEA;
wenzelm
parents: 78991
diff changeset
   507
    val log_dir: Path = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date))
64195
wenzelm
parents: 64194
diff changeset
   508
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   509
    log(start_date, "started")
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   510
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   511
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   512
  class Task private[Isabelle_Cronjob](name: String, body: => Unit) {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   513
    private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   514
    def is_finished: Boolean = future.is_finished
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64157
diff changeset
   515
  }
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   516
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   517
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   518
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   519
  /** cronjob **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   520
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   521
  def cronjob(progress: Progress, exclude_task: Set[String]): Unit = {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   522
    /* soft lock */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   523
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   524
    val still_running =
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   525
      try { Some(File.read(main_state_file)) }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   526
      catch { case ERROR(_) => None }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   527
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   528
    still_running match {
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   529
      case None | Some("") =>
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   530
      case Some(running) =>
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   531
        error("Isabelle cronjob appears to be still running: " + running)
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   532
    }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   533
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   534
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   535
    /* log service */
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   536
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   537
    val log_service = Log_Service(Options.init(), progress = progress)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   538
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73313
diff changeset
   539
    def run(start_date: Date, task: Logger_Task): Unit = log_service.run_task(start_date, task)
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   540
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73313
diff changeset
   541
    def run_now(task: Logger_Task): Unit = run(Date.now(), task)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   542
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   543
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   544
    /* structured tasks */
64184
wenzelm
parents: 64173
diff changeset
   545
78870
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   546
    def SEQ(tasks: List[() => Option[Logger_Task]]): Logger_Task =
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   547
      Logger_Task(body = _ =>
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   548
        for {
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   549
          t <- tasks.iterator
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   550
          task <- t()
78989
wenzelm
parents: 78918
diff changeset
   551
          if !exclude_task(task.name) || task.name.isEmpty
78870
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   552
        } run_now(task))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   553
78869
f464f6bc5809 tuned signature;
wenzelm
parents: 78861
diff changeset
   554
    def SEQUENTIAL(tasks: Logger_Task*): Logger_Task =
78870
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   555
      SEQ(List.from(for (task <- tasks.iterator) yield () => Some(task)))
78869
f464f6bc5809 tuned signature;
wenzelm
parents: 78861
diff changeset
   556
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   557
    def PAR(tasks: List[Logger_Task]): Logger_Task =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   558
      Logger_Task(body =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   559
        { _ =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   560
          @tailrec def join(running: List[Task]): Unit = {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   561
            running.partition(_.is_finished) match {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   562
              case (Nil, Nil) =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   563
              case (Nil, _ :: _) => Time.seconds(0.5).sleep(); join(running)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   564
              case (_ :: _, remaining) => join(remaining)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   565
            }
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   566
          }
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   567
          val start_date = Date.now()
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   568
          val running =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   569
            for (task <- tasks if !exclude_task(task.name))
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   570
              yield log_service.fork_task(start_date, task)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   571
          join(running)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   572
        })
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   573
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   574
66897
wenzelm
parents: 66896
diff changeset
   575
    /* main */
wenzelm
parents: 66896
diff changeset
   576
wenzelm
parents: 66896
diff changeset
   577
    val main_start_date = Date.now()
73342
0bf768567d9f tuned --- avoid deprecated Predef.any2stringadd;
wenzelm
parents: 73340
diff changeset
   578
    File.write(main_state_file, main_start_date.toString + " " + log_service.hostname)
66897
wenzelm
parents: 66896
diff changeset
   579
78877
45d570945fe4 more detailed progress for build_log_database, to see better what happens when;
wenzelm
parents: 78873
diff changeset
   580
    val build_log_database_progress = new File_Progress(build_log_database_log, verbose = true)
78896
3523df57df51 tuned output;
wenzelm
parents: 78885
diff changeset
   581
    build_log_database_progress.echo(
3523df57df51 tuned output;
wenzelm
parents: 78885
diff changeset
   582
      "Started at " + Build_Log.print_date(build_log_database_progress.start))
78877
45d570945fe4 more detailed progress for build_log_database, to see better what happens when;
wenzelm
parents: 78873
diff changeset
   583
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   584
    run(main_start_date,
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   585
      Logger_Task("isabelle_cronjob", logger =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   586
        run_now(
78869
f464f6bc5809 tuned signature;
wenzelm
parents: 78861
diff changeset
   587
          SEQUENTIAL(
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   588
            init,
78860
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   589
            PAR(
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   590
              List(
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   591
                mailman_archives,
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   592
                build_release,
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   593
                Logger_Task("build_log_database",
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   594
                  logger =>
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   595
                    Build_Log.build_log_database(logger.options, build_log_dirs,
78877
45d570945fe4 more detailed progress for build_log_database, to see better what happens when;
wenzelm
parents: 78873
diff changeset
   596
                      progress = build_log_database_progress,
78860
4838a27794ac performance tuning: parallel and incremental update of build_log_database;
wenzelm
parents: 78849
diff changeset
   597
                      vacuum = true, ml_statistics = true,
78872
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   598
                      snapshot = Some(isabelle_devel + Path.explode("build_log.db")))))),
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   599
            PAR(
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   600
              List(remote_builds1, remote_builds2).map(remote_builds =>
78870
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   601
                SEQUENTIAL(
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   602
                  PAR(remote_builds.map(seq =>
78870
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   603
                    SEQ(
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   604
                      for {
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   605
                        (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
78996
674954a49364 clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
wenzelm
parents: 78995
diff changeset
   606
                        _ <- List.from(1 to r.count())
78870
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   607
                      } yield () => {
78995
b9d59669904a clarified signature: more operations and options concerning Isabelle hg;
wenzelm
parents: 78993
diff changeset
   608
                        r.pick(logger.options)
78885
9d0faaa77e5d proper progress (see also 45d570945fe4);
wenzelm
parents: 78877
diff changeset
   609
                          .map({ case (rev, afp_rev) =>
9d0faaa77e5d proper progress (see also 45d570945fe4);
wenzelm
parents: 78877
diff changeset
   610
                            remote_build_history(rev, afp_rev, i, r,
9d0faaa77e5d proper progress (see also 45d570945fe4);
wenzelm
parents: 78877
diff changeset
   611
                              progress = build_log_database_progress) })
78870
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   612
                      }
674362fd8c96 clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
wenzelm
parents: 78869
diff changeset
   613
                    ))),
78872
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   614
                  Logger_Task("build_status", logger =>
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   615
                    Isabelle_System.update_directory(
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   616
                      isabelle_devel + Path.explode("build_status"),
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   617
                      dir =>
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   618
                        Build_Status.build_status(logger.options,
711acefe97a3 clarified modules;
wenzelm
parents: 78871
diff changeset
   619
                          target_dir = dir, ml_statistics = true)))))),
78869
f464f6bc5809 tuned signature;
wenzelm
parents: 78861
diff changeset
   620
            exit))))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   621
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   622
    log_service.shutdown()
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   623
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   624
    main_state_file.file.delete
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   625
  }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   626
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   627
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   628
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   629
  /** command line entry point **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   630
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74921
diff changeset
   631
  def main(args: Array[String]): Unit = {
71632
c1bc38327bc2 clarified signature;
wenzelm
parents: 71601
diff changeset
   632
    Command_Line.tool {
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   633
      var force = false
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   634
      var verbose = false
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   635
      var exclude_task = Set.empty[String]
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   636
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   637
      val getopts = Getopts("""
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   638
Usage: Admin/cronjob/main [OPTIONS]
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   639
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   640
  Options are:
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   641
    -f           apply force to do anything
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   642
    -v           verbose
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   643
    -x NAME      exclude tasks with this name
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   644
""",
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   645
        "f" -> (_ => force = true),
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   646
        "v" -> (_ => verbose = true),
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   647
        "x:" -> (arg => exclude_task += arg))
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   648
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   649
      val more_args = getopts(args)
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   650
      if (more_args.nonEmpty) getopts.usage()
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   651
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71684
diff changeset
   652
      val progress = if (verbose) new Console_Progress() else new Progress
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   653
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   654
      if (force) cronjob(progress, exclude_task)
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   655
      else error("Need to apply force to do anything")
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   656
    }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   657
  }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   658
}