equal
deleted
inserted
replaced
|
1 #!/bin/bash |
|
2 # |
|
3 # Plain identify job for Isabelle + AFP |
|
4 # |
|
5 |
|
6 set -e |
|
7 |
|
8 source "$HOME/.bashrc" |
|
9 |
|
10 LANG=C |
|
11 |
|
12 REPOS_DIR="$HOME/cronjob/plain_identify_repos" |
|
13 ISABELLE_REPOS_SOURCE="http://isabelle.in.tum.de/repos/isabelle" |
|
14 AFP_REPOS_SOURCE="https://bitbucket.org/isa-afp/afp-devel" |
|
15 |
|
16 function setup_repos () |
|
17 { |
|
18 local NAME="$1" |
|
19 local SOURCE="$2" |
|
20 mkdir -p "$REPOS_DIR" |
|
21 if [ ! -d "$REPOS_DIR/$NAME" ]; then |
|
22 hg clone --noupdate -q "$SOURCE" "$REPOS_DIR/$NAME" |
|
23 fi |
|
24 } |
|
25 |
|
26 function identify_repos () |
|
27 { |
|
28 local NAME="$1" |
|
29 hg pull -R "$REPOS_DIR/$NAME" -q |
|
30 local ID="$(hg tip -R "$REPOS_DIR/$NAME" --template "{node|short}")" |
|
31 echo "$NAME version: $ID" |
|
32 } |
|
33 |
|
34 setup_repos "Isabelle" "$ISABELLE_REPOS_SOURCE" |
|
35 setup_repos "AFP" "$AFP_REPOS_SOURCE" |
|
36 |
|
37 NOW="$(date --rfc-3339=ns)" |
|
38 LOG_DIR="$HOME/cronjob/log/$(date -d "$NOW" "+%Y")" |
|
39 LOG_SECONDS="$(($(date -d "$NOW" +"%s") - $(date -d 'today 00:00:00' "+%s")))" |
|
40 LOG_NAME="plain_identify_$(date -d "$NOW" "+%Y-%m-%d").$(printf "%05d" "$LOG_SECONDS").log" |
|
41 |
|
42 mkdir -p "$LOG_DIR" |
|
43 |
|
44 { |
|
45 echo -n "isabelle_identify: " |
|
46 date -d "$NOW" "+%a %b %-d %H:%M:%S %Z %Y" |
|
47 echo |
|
48 identify_repos "Isabelle" |
|
49 identify_repos "AFP" |
|
50 } > "$LOG_DIR/$LOG_NAME" |