author  wenzelm 
Tue, 16 Jan 2018 09:58:17 +0100  
changeset 67445  4311845b0412 
parent 66995  9cb263dbb2f7 
child 67744  5c781dcd5864 
permissions  rwxrxrx 
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" 
9cb263dbb2f7
plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff
changeset

13 
ISABELLE_REPOS_SOURCE="http://isabelle.in.tum.de/repos/isabelle" 
9cb263dbb2f7
plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff
changeset

14 
AFP_REPOS_SOURCE="https://bitbucket.org/isaafp/afpdevel" 
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 "{nodeshort}")" 
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 rfc3339=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" 