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