| author | haftmann | 
| Tue, 16 Jun 2020 08:41:39 +0000 | |
| changeset 71938 | e1b262e7480c | 
| parent 67744 | 5c781dcd5864 | 
| child 71979 | 6678e4d9508f | 
| permissions | -rwxr-xr-x | 
| 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 | 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" |