| 1 | # Common functions for soil/
 | 
| 2 | 
 | 
| 3 | # Include guard.
 | 
| 4 | test -n "${__SOIL_COMMON_SH:-}" && return
 | 
| 5 | readonly __SOIL_COMMON_SH=1
 | 
| 6 | 
 | 
| 7 | log() {
 | 
| 8 |   echo "$@" 1>&2
 | 
| 9 | }
 | 
| 10 | 
 | 
| 11 | log-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 | 
 | 
| 19 | dump-env() {
 | 
| 20 |   env | grep -v '^encrypted_' | sort
 | 
| 21 | }
 | 
| 22 | 
 | 
| 23 | if false; then
 | 
| 24 |   readonly SOIL_USER='travis_admin'
 | 
| 25 |   readonly SOIL_HOST='travis-ci.oilshell.org'
 | 
| 26 |   readonly SOIL_HOST_DIR=~/travis-ci.oilshell.org  # used on server
 | 
| 27 |   readonly SOIL_REMOTE_DIR=travis-ci.oilshell.org  # used on client
 | 
| 28 | elif false; then
 | 
| 29 |   readonly SOIL_USER='oils'
 | 
| 30 |   readonly SOIL_HOST='mb.oils.pub'
 | 
| 31 |   # Extra level
 | 
| 32 |   readonly SOIL_HOST_DIR=~/www/mb.oils.pub  # used on server
 | 
| 33 |   readonly SOIL_REMOTE_DIR=www/mb.oils.pub  # used on client
 | 
| 34 | else
 | 
| 35 |   readonly SOIL_USER='oils'
 | 
| 36 |   readonly SOIL_HOST='op.oils.pub'
 | 
| 37 |   readonly SOIL_HOST_DIR=~/op.oils.pub  # used on server
 | 
| 38 |   readonly SOIL_REMOTE_DIR=op.oils.pub  # used on client
 | 
| 39 | fi
 | 
| 40 | 
 | 
| 41 | readonly SOIL_USER_HOST="$SOIL_USER@$SOIL_HOST"
 | 
| 42 | 
 | 
| 43 | html-head() {
 | 
| 44 |   # TODO: Shebang line should change too
 | 
| 45 |   PYTHONPATH=. python3 doctools/html_head.py "$@"
 | 
| 46 | }
 | 
| 47 | 
 | 
| 48 | # NOTE: soil-html-head and table-sort-html-head are distinct, because they
 | 
| 49 | # collide with <td> styling and so forth
 | 
| 50 | 
 | 
| 51 | soil-html-head() {
 | 
| 52 |   local title="$1"
 | 
| 53 |   local web_base_url=${2:-'/web'}
 | 
| 54 | 
 | 
| 55 |   html-head --title "$title" \
 | 
| 56 |     "$web_base_url/base.css?cache=0" "$web_base_url/soil.css?cache=0"
 | 
| 57 | }
 | 
| 58 | 
 | 
| 59 | table-sort-html-head() {
 | 
| 60 |   local title="$1"
 | 
| 61 |   local web_base_url=${2:-'/web'}
 | 
| 62 | 
 | 
| 63 |   html-head --title "$title" \
 | 
| 64 |     "$web_base_url/base.css?cache=0" \
 | 
| 65 |     "$web_base_url/ajax.js?cache=0" \
 | 
| 66 |     "$web_base_url/table/table-sort.css?cache=0" "$web_base_url/table/table-sort.js?cache=0" 
 | 
| 67 | }
 | 
| 68 | 
 | 
| 69 | git-commit-dir() {
 | 
| 70 |   local prefix=$1
 | 
| 71 | 
 | 
| 72 |   # written by save-metadata in soil/worker.sh
 | 
| 73 |   local commit_hash
 | 
| 74 |   commit_hash=$(cat _tmp/soil/commit-hash.txt)
 | 
| 75 | 
 | 
| 76 |   local git_commit_dir="$SOIL_REMOTE_DIR/${prefix}jobs/git-$commit_hash"
 | 
| 77 | 
 | 
| 78 |   echo $git_commit_dir
 | 
| 79 | }
 | 
| 80 | 
 | 
| 81 | git-commit-url() {
 | 
| 82 |   local prefix=$1
 | 
| 83 | 
 | 
| 84 |   # written by save-metadata in soil/worker.sh
 | 
| 85 |   local commit_hash
 | 
| 86 |   commit_hash=$(cat _tmp/soil/commit-hash.txt)
 | 
| 87 | 
 | 
| 88 |   # https:// not working on Github Actions?
 | 
| 89 |   local url="http://$SOIL_HOST/${prefix}jobs/git-$commit_hash"
 | 
| 90 | 
 | 
| 91 |   echo $url
 | 
| 92 | }
 |