Admin/cronjob/plain_identify
author wenzelm
Fri Nov 03 19:20:47 2017 +0100 (19 months ago)
changeset 66997 17eb23e43630
parent 66995 9cb263dbb2f7
child 67744 5c781dcd5864
permissions -rwxr-xr-x
avoid slow IntInf.pow in Poly/ML 5.7.1 testing version, e.g. relevant for AFP/Lorenz_C0;
     1 #!/bin/bash
     2 #
     3 # Plain identify job for Isabelle + AFP
     4 #
     5 
     6 set -e
     7 
     8 source "$HOME/.bashrc"
     9 
    10 LANG=C
    11 
    12 REPOS_DIR="$HOME/cronjob/plain_identify_repos"
    13 ISABELLE_REPOS_SOURCE="http://isabelle.in.tum.de/repos/isabelle"
    14 AFP_REPOS_SOURCE="https://bitbucket.org/isa-afp/afp-devel"
    15 
    16 function setup_repos ()
    17 {
    18   local NAME="$1"
    19   local SOURCE="$2"
    20   mkdir -p "$REPOS_DIR"
    21   if [ ! -d "$REPOS_DIR/$NAME" ]; then
    22     hg clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
    23   fi
    24 }
    25 
    26 function identify_repos ()
    27 {
    28   local NAME="$1"
    29   hg pull -R "$REPOS_DIR/$NAME" -q
    30   local ID="$(hg tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
    31   echo "$NAME version: $ID"
    32 }
    33 
    34 setup_repos "Isabelle" "$ISABELLE_REPOS_SOURCE"
    35 setup_repos "AFP" "$AFP_REPOS_SOURCE"
    36 
    37 NOW="$(date --rfc-3339=ns)"
    38 LOG_DIR="$HOME/cronjob/log/$(date -d "$NOW" "+%Y")"
    39 LOG_SECONDS="$(($(date -d "$NOW" +"%s") - $(date -d 'today 00:00:00' "+%s")))"
    40 LOG_NAME="plain_identify_$(date -d "$NOW" "+%Y-%m-%d").$(printf "%05d" "$LOG_SECONDS").log"
    41 
    42 mkdir -p "$LOG_DIR"
    43 
    44 {
    45   echo -n "isabelle_identify: "
    46   date -d "$NOW" "+%a %b %-d %H:%M:%S %Z %Y"
    47   echo
    48   identify_repos "Isabelle"
    49   identify_repos "AFP"
    50 } > "$LOG_DIR/$LOG_NAME"