| author | wenzelm | 
| Sat, 20 Aug 2022 17:01:34 +0200 | |
| changeset 75927 | 040a59abe196 | 
| parent 73483 | 804e75127f29 | 
| 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 | |
| 73483 | 10 | export LANG=C | 
| 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 | 14 | ISABELLE_REPOS_SOURCE="https://isabelle.sketis.net/repos/isabelle" | 
| 71979 | 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 | 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 | 30 |   "${HG:-hg}" pull -R "$REPOS_DIR/$NAME" -q
 | 
| 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" |