author  wenzelm 
Sat, 22 Jan 2022 13:00:03 +0100  
changeset 74994  26794ec7c78e 
parent 73483  804e75127f29 
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 

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/afpdevel" 
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 "{nodeshort}")" 

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 rfc3339=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" 