Admin/cronjob/plain_identify
author wenzelm
Thu, 14 Jun 2018 17:50:23 +0200
changeset 68449 6d0f1a5a16ea
parent 67744 5c781dcd5864
child 71979 6678e4d9508f
permissions -rwxr-xr-x
auto update;
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"
67744
5c781dcd5864 prefer https;
wenzelm
parents: 66995
diff changeset
    13
ISABELLE_REPOS_SOURCE="https://isabelle.in.tum.de/repos/isabelle"
66995
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"