plain identify job for Isabelle + AFP, independent of any Isabelle technology;
authorwenzelm
Fri Nov 03 17:27:00 2017 +0100 (18 months ago)
changeset 669959cb263dbb2f7
parent 66994 38fd865aae45
child 66996 22ca0f37f491
plain identify job for Isabelle + AFP, independent of any Isabelle technology;
Admin/cronjob/README
Admin/cronjob/crontab.lxbroy5
Admin/cronjob/plain_identify
src/Pure/Admin/build_log.scala
     1.1 --- a/Admin/cronjob/README	Fri Nov 03 14:14:17 2017 +0100
     1.2 +++ b/Admin/cronjob/README	Fri Nov 03 17:27:00 2017 +0100
     1.3 @@ -1,13 +1,14 @@
     1.4  Administrative Isabelle cronjob at TUM
     1.5  ======================================
     1.6  
     1.7 +- jobs: manual installation on target directory:
     1.8 +    cp "$ISABELLE_HOME/Admin/cronjob/self_update "$HOME/cronjob/self_update"
     1.9 +    cp "$ISABELLE_HOME/Admin/cronjob/plain_identify "$HOME/cronjob/plain_identify"
    1.10 +
    1.11  - crontab: manual update on target machine
    1.12      crontab -l
    1.13      crontab -e
    1.14  
    1.15 -- self_update: manual installation on target directory
    1.16 -    cp "$ISABELLE_HOME/Admin/cronjob/self_update "$HOME/cronjob/self_update"
    1.17 -
    1.18  - $HOME/cronjob/run/ -- run-time state
    1.19  
    1.20  - $HOME/cronjob/log/ -- cumulative log area
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/cronjob/crontab.lxbroy5	Fri Nov 03 17:27:00 2017 +0100
     2.3 @@ -0,0 +1,4 @@
     2.4 +SHELL=/bin/bash
     2.5 +MAILTO=wenzelm
     2.6 +
     2.7 +47 00 * * *       $HOME/cronjob/plain_identify
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/cronjob/plain_identify	Fri Nov 03 17:27:00 2017 +0100
     3.3 @@ -0,0 +1,50 @@
     3.4 +#!/bin/bash
     3.5 +#
     3.6 +# Plain identify job for Isabelle + AFP
     3.7 +#
     3.8 +
     3.9 +set -e
    3.10 +
    3.11 +source "$HOME/.bashrc"
    3.12 +
    3.13 +LANG=C
    3.14 +
    3.15 +REPOS_DIR="$HOME/cronjob/plain_identify_repos"
    3.16 +ISABELLE_REPOS_SOURCE="http://isabelle.in.tum.de/repos/isabelle"
    3.17 +AFP_REPOS_SOURCE="https://bitbucket.org/isa-afp/afp-devel"
    3.18 +
    3.19 +function setup_repos ()
    3.20 +{
    3.21 +  local NAME="$1"
    3.22 +  local SOURCE="$2"
    3.23 +  mkdir -p "$REPOS_DIR"
    3.24 +  if [ ! -d "$REPOS_DIR/$NAME" ]; then
    3.25 +    hg clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
    3.26 +  fi
    3.27 +}
    3.28 +
    3.29 +function identify_repos ()
    3.30 +{
    3.31 +  local NAME="$1"
    3.32 +  hg pull -R "$REPOS_DIR/$NAME" -q
    3.33 +  local ID="$(hg tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
    3.34 +  echo "$NAME version: $ID"
    3.35 +}
    3.36 +
    3.37 +setup_repos "Isabelle" "$ISABELLE_REPOS_SOURCE"
    3.38 +setup_repos "AFP" "$AFP_REPOS_SOURCE"
    3.39 +
    3.40 +NOW="$(date --rfc-3339=ns)"
    3.41 +LOG_DIR="$HOME/cronjob/log/$(date -d "$NOW" "+%Y")"
    3.42 +LOG_SECONDS="$(($(date -d "$NOW" +"%s") - $(date -d 'today 00:00:00' "+%s")))"
    3.43 +LOG_NAME="plain_identify_$(date -d "$NOW" "+%Y-%m-%d").$(printf "%05d" "$LOG_SECONDS").log"
    3.44 +
    3.45 +mkdir -p "$LOG_DIR"
    3.46 +
    3.47 +{
    3.48 +  echo -n "isabelle_identify: "
    3.49 +  date -d "$NOW" "+%a %b %-d %H:%M:%S %Z %Y"
    3.50 +  echo
    3.51 +  identify_repos "Isabelle"
    3.52 +  identify_repos "AFP"
    3.53 +} > "$LOG_DIR/$LOG_NAME"
     4.1 --- a/src/Pure/Admin/build_log.scala	Fri Nov 03 14:14:17 2017 +0100
     4.2 +++ b/src/Pure/Admin/build_log.scala	Fri Nov 03 17:27:00 2017 +0100
     4.3 @@ -133,8 +133,8 @@
     4.4  
     4.5      def is_log(file: JFile,
     4.6        prefixes: List[String] =
     4.7 -        List(Build_History.log_prefix, Identify.log_prefix, Isatest.log_prefix,
     4.8 -          AFP_Test.log_prefix, Jenkins.log_prefix),
     4.9 +        List(Build_History.log_prefix, Identify.log_prefix, Identify.log_prefix2,
    4.10 +          Isatest.log_prefix, AFP_Test.log_prefix, Jenkins.log_prefix),
    4.11        suffixes: List[String] = List(".log", ".log.gz", ".log.xz")): Boolean =
    4.12      {
    4.13        val name = file.getName
    4.14 @@ -314,9 +314,11 @@
    4.15    object Identify
    4.16    {
    4.17      val log_prefix = "isabelle_identify_"
    4.18 +    val log_prefix2 = "plain_identify_"
    4.19  
    4.20      def engine(log_file: Log_File): String =
    4.21        if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify"
    4.22 +      else if (log_file.name.startsWith(log_prefix2)) "plain_identify"
    4.23        else "identify"
    4.24  
    4.25      def content(date: Date, isabelle_version: Option[String], afp_version: Option[String]): String =