# HG changeset patch
# User wenzelm
# Date 1509726420 -3600
# Node ID 9cb263dbb2f74f333fde92b8bb9159ed2f42072a
# Parent  38fd865aae453ac19fcdb6b28f94353780ee3a7f
plain identify job for Isabelle + AFP, independent of any Isabelle technology;

diff -r 38fd865aae45 -r 9cb263dbb2f7 Admin/cronjob/README
--- a/Admin/cronjob/README	Fri Nov 03 14:14:17 2017 +0100
+++ b/Admin/cronjob/README	Fri Nov 03 17:27:00 2017 +0100
@@ -1,13 +1,14 @@
 Administrative Isabelle cronjob at TUM
 ======================================
 
+- jobs: manual installation on target directory:
+    cp "$ISABELLE_HOME/Admin/cronjob/self_update "$HOME/cronjob/self_update"
+    cp "$ISABELLE_HOME/Admin/cronjob/plain_identify "$HOME/cronjob/plain_identify"
+
 - crontab: manual update on target machine
     crontab -l
     crontab -e
 
-- self_update: manual installation on target directory
-    cp "$ISABELLE_HOME/Admin/cronjob/self_update "$HOME/cronjob/self_update"
-
 - $HOME/cronjob/run/ -- run-time state
 
 - $HOME/cronjob/log/ -- cumulative log area
diff -r 38fd865aae45 -r 9cb263dbb2f7 Admin/cronjob/crontab.lxbroy5
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/cronjob/crontab.lxbroy5	Fri Nov 03 17:27:00 2017 +0100
@@ -0,0 +1,4 @@
+SHELL=/bin/bash
+MAILTO=wenzelm
+
+47 00 * * *       $HOME/cronjob/plain_identify
diff -r 38fd865aae45 -r 9cb263dbb2f7 Admin/cronjob/plain_identify
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/cronjob/plain_identify	Fri Nov 03 17:27:00 2017 +0100
@@ -0,0 +1,50 @@
+#!/bin/bash
+#
+# Plain identify job for Isabelle + AFP
+#
+
+set -e
+
+source "$HOME/.bashrc"
+
+LANG=C
+
+REPOS_DIR="$HOME/cronjob/plain_identify_repos"
+ISABELLE_REPOS_SOURCE="http://isabelle.in.tum.de/repos/isabelle"
+AFP_REPOS_SOURCE="https://bitbucket.org/isa-afp/afp-devel"
+
+function setup_repos ()
+{
+  local NAME="$1"
+  local SOURCE="$2"
+  mkdir -p "$REPOS_DIR"
+  if [ ! -d "$REPOS_DIR/$NAME" ]; then
+    hg clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
+  fi
+}
+
+function identify_repos ()
+{
+  local NAME="$1"
+  hg pull -R "$REPOS_DIR/$NAME" -q
+  local ID="$(hg tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
+  echo "$NAME version: $ID"
+}
+
+setup_repos "Isabelle" "$ISABELLE_REPOS_SOURCE"
+setup_repos "AFP" "$AFP_REPOS_SOURCE"
+
+NOW="$(date --rfc-3339=ns)"
+LOG_DIR="$HOME/cronjob/log/$(date -d "$NOW" "+%Y")"
+LOG_SECONDS="$(($(date -d "$NOW" +"%s") - $(date -d 'today 00:00:00' "+%s")))"
+LOG_NAME="plain_identify_$(date -d "$NOW" "+%Y-%m-%d").$(printf "%05d" "$LOG_SECONDS").log"
+
+mkdir -p "$LOG_DIR"
+
+{
+  echo -n "isabelle_identify: "
+  date -d "$NOW" "+%a %b %-d %H:%M:%S %Z %Y"
+  echo
+  identify_repos "Isabelle"
+  identify_repos "AFP"
+} > "$LOG_DIR/$LOG_NAME"
diff -r 38fd865aae45 -r 9cb263dbb2f7 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Nov 03 14:14:17 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Fri Nov 03 17:27:00 2017 +0100
@@ -133,8 +133,8 @@
 
     def is_log(file: JFile,
       prefixes: List[String] =
-        List(Build_History.log_prefix, Identify.log_prefix, Isatest.log_prefix,
-          AFP_Test.log_prefix, Jenkins.log_prefix),
+        List(Build_History.log_prefix, Identify.log_prefix, Identify.log_prefix2,
+          Isatest.log_prefix, AFP_Test.log_prefix, Jenkins.log_prefix),
       suffixes: List[String] = List(".log", ".log.gz", ".log.xz")): Boolean =
     {
       val name = file.getName
@@ -314,9 +314,11 @@
   object Identify
   {
     val log_prefix = "isabelle_identify_"
+    val log_prefix2 = "plain_identify_"
 
     def engine(log_file: Log_File): String =
       if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify"
+      else if (log_file.name.startsWith(log_prefix2)) "plain_identify"
       else "identify"
 
     def content(date: Date, isabelle_version: Option[String], afp_version: Option[String]): String =