Admin/cronjob/plain_identify
author wenzelm
Sat, 28 Nov 2020 16:25:29 +0100
changeset 72759 bd5ee3148132
parent 72393 b8f25ceac57f
child 73479 6e20976d58f5
permissions -rwxr-xr-x
more antiquotations (reverting 4df341249348);

#!/bin/bash
#
# Plain identify job for Isabelle + AFP
#

set -e

source "$HOME/.bashrc"

LANG=C

REPOS_DIR="$HOME/cronjob/plain_identify_repos"
ISABELLE_REPOS_SOURCE="https://isabelle.sketis.net/repos/isabelle"
AFP_REPOS_SOURCE="https://isabelle.sketis.net/repos/afp-devel"

function setup_repos ()
{
  local NAME="$1"
  local SOURCE="$2"
  mkdir -p "$REPOS_DIR"
  if [ ! -d "$REPOS_DIR/$NAME" ]; then
    hg clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
  fi
}

function identify_repos ()
{
  local NAME="$1"
  hg pull -R "$REPOS_DIR/$NAME" -q
  local ID="$(hg tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
  echo "$NAME version: $ID"
}

setup_repos "Isabelle" "$ISABELLE_REPOS_SOURCE"
setup_repos "AFP" "$AFP_REPOS_SOURCE"

NOW="$(date --rfc-3339=ns)"
LOG_DIR="$HOME/cronjob/log/$(date -d "$NOW" "+%Y")"
LOG_SECONDS="$(($(date -d "$NOW" +"%s") - $(date -d 'today 00:00:00' "+%s")))"
LOG_NAME="plain_identify_$(date -d "$NOW" "+%Y-%m-%d").$(printf "%05d" "$LOG_SECONDS").log"

mkdir -p "$LOG_DIR"

{
  echo -n "isabelle_identify: "
  date -d "$NOW" "+%a %b %-d %H:%M:%S %Z %Y"
  echo
  identify_repos "Isabelle"
  identify_repos "AFP"
} > "$LOG_DIR/$LOG_NAME"