Admin/lib/Tools/build_doc
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 49131 aa1e2ba3c697
child 52740 bceec99254b0
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     2
#
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     3
# Author: Makarius
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     4
#
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: build Isabelle documentation
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     6
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     7
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     8
## diagnostics
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
     9
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    11
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    12
function usage()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    13
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    14
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    16
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    17
  echo "  Options are:"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    18
  echo "    -a           select all doc sessions"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    19
  echo "    -j INT       maximum number of parallel jobs (default 1)"
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    20
  echo "    -p           build only pdf documents"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    21
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    22
  echo "  Build Isabelle documentation from (doc) sessions."
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    23
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    24
  exit 1
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    25
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    26
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    27
function fail()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    28
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    29
  echo "$1" >&2
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    30
  exit 2
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    31
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    32
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    33
function check_number()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    34
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    35
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    36
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    37
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    38
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    39
## process command line
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    40
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    41
# options
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    42
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    43
ALL_DOCS="false"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    44
JOBS=""
49005
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    45
PDF_ONLY=""
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    46
49005
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    47
while getopts "aj:p" OPT
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    48
do
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    49
  case "$OPT" in
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    50
    a)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    51
      ALL_DOCS="true"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    52
      ;;
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    53
    j)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    54
      check_number "$OPTARG"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    55
      JOBS="-j $OPTARG"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    56
      ;;
49005
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    57
    p)
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    58
      PDF_ONLY="true"
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    59
      ;;
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    60
    \?)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    61
      usage
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    62
      ;;
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    63
  esac
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    64
done
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    65
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    66
shift $(($OPTIND - 1))
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    67
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    68
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    69
# arguments
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    70
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    71
if [ "$ALL_DOCS" = true ]; then
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    72
  declare -a BUILD_ARGS=(-g doc)
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    73
else
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    74
  declare -a BUILD_ARGS=()
49073
88fe93ae61cf tuned boundary cases of command-line;
wenzelm
parents: 49005
diff changeset
    75
  [ "$#" -eq 0 ] && usage
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    76
fi
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    77
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    78
BUILD_ARGS["${#BUILD_ARGS[@]}"]="--"
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    79
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    80
while [ "$#" -ne 0 ]; do
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    81
  BUILD_ARGS["${#BUILD_ARGS[@]}"]="$1"
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    82
  shift
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    83
done
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    84
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    85
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    86
## main
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    87
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    88
OUTPUT="$ISABELLE_TMP_PREFIX$$"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    89
mkdir -p "$OUTPUT" || fail "Bad directory: \"$OUTPUT\""
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    90
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    91
"$ISABELLE_TOOL" build -R -b $JOBS "${BUILD_ARGS[@]}"
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    92
RC=$?
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    93
49005
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    94
if [ "$PDF_ONLY" = true ]; then
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    95
  FORMATS="pdf"
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    96
else
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    97
  FORMATS="dvi pdf"
49005
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    98
fi
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    99
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
   100
for FORMAT in $FORMATS
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   101
do
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   102
  if [ "$RC" = 0 ]; then
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   103
    echo "Document format: $FORMAT"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   104
    "$ISABELLE_TOOL" build -o browser_info=false -o "document=$FORMAT" \
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
   105
      -o "document_output=$OUTPUT" -c $JOBS "${BUILD_ARGS[@]}"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   106
    RC=$?
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   107
  fi
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   108
done
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   109
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   110
if [ "$RC" = 0 ]; then
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   111
  for FILE in $(find "$OUTPUT" -name "*.eps" -o -name "*.ps")
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   112
  do
48988
f4d4d6d6702b prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools;
wenzelm
parents: 48972
diff changeset
   113
    cp -f "$FILE" "$ISABELLE_HOME/doc"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   114
  done
49073
88fe93ae61cf tuned boundary cases of command-line;
wenzelm
parents: 49005
diff changeset
   115
  if [ "$PDF_ONLY" = true ]; then
88fe93ae61cf tuned boundary cases of command-line;
wenzelm
parents: 49005
diff changeset
   116
    cp -f "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
88fe93ae61cf tuned boundary cases of command-line;
wenzelm
parents: 49005
diff changeset
   117
  else
88fe93ae61cf tuned boundary cases of command-line;
wenzelm
parents: 49005
diff changeset
   118
    cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
88fe93ae61cf tuned boundary cases of command-line;
wenzelm
parents: 49005
diff changeset
   119
  fi
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   120
fi
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   121
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   122
rm -rf "$OUTPUT"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   123
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
   124
exit $RC