# HG changeset patch
# User wenzelm
# Date 1604778384 -3600
# Node ID 274c9986e55b59733041232813ea9bdd9298baf7
# Parent  38ebf696fd0cb9f985e93437d2a57748ca7315db
maintain Isabelle mailing list archives;

diff -r 38ebf696fd0c -r 274c9986e55b src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 07 20:24:34 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 07 20:46:24 2020 +0100
@@ -27,6 +27,8 @@
   val isabelle_repos: Path = main_dir + Path.explode("isabelle")
   val afp_repos: Path = main_dir + Path.explode("AFP")
 
+  val mailman_archives_dir = Path.explode("~/cronjob/Mailman")
+
   val build_log_dirs =
     List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
 
@@ -70,6 +72,16 @@
       })
 
 
+  /* Mailman archives */
+
+  val mailman_archives: Logger_Task =
+    Logger_Task("mailman_archives", logger =>
+      {
+        Mailman.isabelle_users.download(mailman_archives_dir)
+        Mailman.isabelle_dev.download(mailman_archives_dir)
+      })
+
+
   /* build release */
 
   val build_release: Logger_Task =
@@ -567,8 +579,7 @@
         run_now(
           SEQ(List(
             init,
-            build_history_base,
-            build_release,
+            PAR(List(mailman_archives, SEQ(List(build_history_base, build_release)))),
             PAR(
               List(remote_builds1, remote_builds2).map(remote_builds =>
               SEQ(List(
diff -r 38ebf696fd0c -r 274c9986e55b src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Sat Nov 07 20:24:34 2020 +0100
+++ b/src/Pure/General/mailman.scala	Sat Nov 07 20:46:24 2020 +0100
@@ -12,6 +12,8 @@
 
 object Mailman
 {
+  /* mailing list archives */
+
   def archive(url: URL, name: String = ""): Archive =
   {
     val text = Url.read(url)
@@ -57,4 +59,13 @@
         })
     }
   }
+
+
+  /* Isabelle mailing lists */
+
+  def isabelle_users: Archive =
+    archive(Url("https://lists.cam.ac.uk/pipermail/cl-isabelle-users"), name = "isabelle-users")
+
+  def isabelle_dev: Archive =
+    archive(Url("https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev"))
 }