Admin/cronjob/plain_identify
author wenzelm
Sat, 22 Jan 2022 13:00:03 +0100
changeset 74994 26794ec7c78e
parent 73483 804e75127f29
permissions -rwxr-xr-x
some updates and clarification on Assumption.export_term;
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
73483
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73479
diff changeset
    10
export LANG=C
804e75127f29 more robust invocation of hg;
wenzelm
parents: 73479
diff changeset
    11
export HGPLAIN=
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    12
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    13
REPOS_DIR="$HOME/cronjob/plain_identify_repos"
72393
b8f25ceac57f updated URL;
wenzelm
parents: 71979
diff changeset
    14
ISABELLE_REPOS_SOURCE="https://isabelle.sketis.net/repos/isabelle"
71979
6678e4d9508f more uniform URL (see 60b5a4731695);
wenzelm
parents: 67744
diff changeset
    15
AFP_REPOS_SOURCE="https://isabelle.sketis.net/repos/afp-devel"
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    16
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    17
function setup_repos ()
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    18
{
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    19
  local NAME="$1"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    20
  local SOURCE="$2"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    21
  mkdir -p "$REPOS_DIR"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    22
  if [ ! -d "$REPOS_DIR/$NAME" ]; then
73479
6e20976d58f5 more robust invocation of hg;
wenzelm
parents: 72393
diff changeset
    23
    "${HG:-hg}" clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME"
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    24
  fi
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
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    27
function identify_repos ()
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    28
{
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    29
  local NAME="$1"
73479
6e20976d58f5 more robust invocation of hg;
wenzelm
parents: 72393
diff changeset
    30
  "${HG:-hg}" pull -R "$REPOS_DIR/$NAME" -q
6e20976d58f5 more robust invocation of hg;
wenzelm
parents: 72393
diff changeset
    31
  local ID="$("${HG:-hg}" tip -R "$REPOS_DIR/$NAME" --template "{node|short}")"
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    32
  echo "$NAME version: $ID"
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
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    35
setup_repos "Isabelle" "$ISABELLE_REPOS_SOURCE"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    36
setup_repos "AFP" "$AFP_REPOS_SOURCE"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    37
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    38
NOW="$(date --rfc-3339=ns)"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    39
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
    40
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
    41
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
    42
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    43
mkdir -p "$LOG_DIR"
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
{
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    46
  echo -n "isabelle_identify: "
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    47
  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
    48
  echo
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    49
  identify_repos "Isabelle"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    50
  identify_repos "AFP"
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
    51
} > "$LOG_DIR/$LOG_NAME"