Admin/lib/Tools/build_doc
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61135 8f7d802b7a71
child 62435 2c390ad93bc8
permissions -rwxr-xr-x
proper syntax;
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
61135
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
     7
## settings
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
     8
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
     9
case "$ISABELLE_JAVA_PLATFORM" in
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    10
  x86-*)
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    11
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    12
    ;;
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    13
  x86_64-*)
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    14
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    15
    ;;
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    16
esac
8f7d802b7a71 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents: 56432
diff changeset
    17
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    18
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    19
## diagnostics
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    20
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    21
PRG="$(basename "$0")"
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    22
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    23
function usage()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    24
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    25
  echo
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    26
  echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    27
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    28
  echo "  Options are:"
56432
wenzelm
parents: 56429
diff changeset
    29
  echo "    -a           select all documentation sessions"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    30
  echo "    -j INT       maximum number of parallel jobs (default 1)"
53208
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    31
  echo "    -s           system build mode"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    32
  echo
56432
wenzelm
parents: 56429
diff changeset
    33
  echo "  Build Isabelle documentation from documentation sessions with"
wenzelm
parents: 56429
diff changeset
    34
  echo "  suitable document_variants entry."
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    35
  echo
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    36
  exit 1
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
function fail()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    40
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    41
  echo "$1" >&2
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    42
  exit 2
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    43
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    44
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    45
function check_number()
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    46
{
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    47
  [ -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
    48
}
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    49
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    50
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    51
## process command line
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
ALL_DOCS="false"
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    54
MAX_JOBS="1"
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    55
SYSTEM_MODE="false"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    56
53208
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    57
while getopts "aj:s" OPT
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    58
do
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    59
  case "$OPT" in
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    60
    a)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    61
      ALL_DOCS="true"
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
    j)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    64
      check_number "$OPTARG"
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    65
      MAX_JOBS="$OPTARG"
53208
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    66
      ;;
bec95e287d26 prefer build_doc -s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents: 52740
diff changeset
    67
    s)
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    68
      SYSTEM_MODE="true"
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    69
      ;;
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    70
    \?)
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    71
      usage
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    72
      ;;
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    73
  esac
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    74
done
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    75
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    76
shift $(($OPTIND - 1))
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    77
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    78
[ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    79
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    80
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    81
## main
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    82
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    83
isabelle_admin_build jars || exit $?
48972
196520d51afd more formal build_doc tool (Admin only);
wenzelm
parents:
diff changeset
    84
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    85
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 49073
diff changeset
    86
56429
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    87
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \
bc61161a5bd0 re-implemented build_doc in Isabelle/Scala;
wenzelm
parents: 53208
diff changeset
    88
  "$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@"
49005
96d5e42e5e3a approximative build of pdf documents in 1 pass instead of 3;
wenzelm
parents: 49002
diff changeset
    89