OILS / soil / common.sh View on Github | oilshell.org

85 lines, 47 significant
1# Common functions for soil/
2
3# Include guard.
4test -n "${__SOIL_COMMON_SH:-}" && return
5readonly __SOIL_COMMON_SH=1
6
7log() {
8 echo "$@" 1>&2
9}
10
11log-context() {
12 local label=$1
13
14 log ''
15 log "$label: running as user '$(whoami)' on host '$(hostname)' in dir $PWD"
16 log ''
17}
18
19dump-env() {
20 env | grep -v '^encrypted_' | sort
21}
22
23readonly SOIL_USER='travis_admin'
24readonly SOIL_HOST='travis-ci.oilshell.org'
25readonly SOIL_USER_HOST="$SOIL_USER@$SOIL_HOST"
26
27html-head() {
28 # TODO: Shebang line should chang ecahnge to
29 PYTHONPATH=. python3 doctools/html_head.py "$@"
30}
31
32# NOTE: soil-html-head and table-sort-html-head are distinct, because they
33# collide with <td> styling and so forth
34
35soil-html-head() {
36 local title="$1"
37 local web_base_url=${2:-'/web'}
38
39 html-head --title "$title" \
40 "$web_base_url/base.css?cache=0" "$web_base_url/soil.css?cache=0"
41}
42
43table-sort-html-head() {
44 local title="$1"
45 local web_base_url=${2:-'/web'}
46
47 html-head --title "$title" \
48 "$web_base_url/base.css?cache=0" \
49 "$web_base_url/ajax.js?cache=0" \
50 "$web_base_url/table/table-sort.css?cache=0" "$web_base_url/table/table-sort.js?cache=0"
51}
52
53# Used by mycpp/build.sh and benchmarks/auto.sh
54find-dir-html() {
55 local dir=$1
56 local out_name=${2:-index}
57
58 #local txt=$dir/$out_name.txt
59 #find $dir -type f | sort > $txt
60 #echo "Wrote $txt"
61
62 local html=$dir/$out_name.html
63
64 # Note: no HTML escaping. Would be nice for Oil.
65 find $dir -type f | sort | gawk -v dir="$dir" '
66 match($0, dir "/(.*)", m) {
67 url = m[1]
68 printf("<a href=\"%s\">%s</a> <br/>\n", url, url)
69 }
70 ' > $html
71
72 log "Wrote $html"
73}
74
75git-commit-dir() {
76 local prefix=$1
77
78 local commit_hash
79 # written by save-metadata in soil/worker.sh
80 commit_hash=$(cat _tmp/soil/commit-hash.txt)
81
82 local git_commit_dir="travis-ci.oilshell.org/${prefix}jobs/git-$commit_hash"
83
84 echo $git_commit_dir
85}