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;
wenzelm@66995
     1
#!/bin/bash
wenzelm@66995
     2
#
wenzelm@66995
     3
# Plain identify job for Isabelle + AFP
wenzelm@66995
     4
#
wenzelm@66995
     5
wenzelm@66995
     6
set -e
wenzelm@66995
     7
wenzelm@66995
     8
source "$HOME/.bashrc"
wenzelm@66995
     9
wenzelm@66995
    10
LANG=C
wenzelm@66995
    11
wenzelm@66995
    12
REPOS_DIR="$HOME/cronjob/plain_identify_repos"
wenzelm@66995
    13
ISABELLE_REPOS_SOURCE="http://isabelle.in.tum.de/repos/isabelle"
wenzelm@66995
    14
AFP_REPOS_SOURCE="https://bitbucket.org/isa-afp/afp-devel"
wenzelm@66995
    15
wenzelm@66995
    16
function setup_repos ()
wenzelm@66995
    17
{
wenzelm@66995
    18
  local NAME="$1"
wenzelm@66995
    19
  local SOURCE="$2"
wenzelm@66995
    20
  mkdir -p "$REPOS_DIR"
wenzelm@66995
    21
  if [ ! -d "$REPOS_DIR/$NAME" ]; then
wenzelm@66995
    22
    hg clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
wenzelm@66995
    23
  fi
wenzelm@66995
    24
}
wenzelm@66995
    25
wenzelm@66995
    26
function identify_repos ()
wenzelm@66995
    27
{
wenzelm@66995
    28
  local NAME="$1"
wenzelm@66995
    29
  hg pull -R "$REPOS_DIR/$NAME" -q
wenzelm@66995
    30
  local ID="$(hg tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
wenzelm@66995
    31
  echo "$NAME version: $ID"
wenzelm@66995
    32
}
wenzelm@66995
    33
wenzelm@66995
    34
setup_repos "Isabelle" "$ISABELLE_REPOS_SOURCE"
wenzelm@66995
    35
setup_repos "AFP" "$AFP_REPOS_SOURCE"
wenzelm@66995
    36
wenzelm@66995
    37
NOW="$(date --rfc-3339=ns)"
wenzelm@66995
    38
LOG_DIR="$HOME/cronjob/log/$(date -d "$NOW" "+%Y")"
wenzelm@66995
    39
LOG_SECONDS="$(($(date -d "$NOW" +"%s") - $(date -d 'today 00:00:00' "+%s")))"
wenzelm@66995
    40
LOG_NAME="plain_identify_$(date -d "$NOW" "+%Y-%m-%d").$(printf "%05d" "$LOG_SECONDS").log"
wenzelm@66995
    41
wenzelm@66995
    42
mkdir -p "$LOG_DIR"
wenzelm@66995
    43
wenzelm@66995
    44
{
wenzelm@66995
    45
  echo -n "isabelle_identify: "
wenzelm@66995
    46
  date -d "$NOW" "+%a %b %-d %H:%M:%S %Z %Y"
wenzelm@66995
    47
  echo
wenzelm@66995
    48
  identify_repos "Isabelle"
wenzelm@66995
    49
  identify_repos "AFP"
wenzelm@66995
    50
} > "$LOG_DIR/$LOG_NAME"