| author | wenzelm | 
| Sat, 15 Mar 2014 15:49:23 +0100 | |
| changeset 56163 | 331f4aba14b3 | 
| parent 51064 | 9c425ed4a52c | 
| child 56902 | f901a08c5653 | 
| permissions | -rwxr-xr-x | 
| 50899 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 1 | #!/usr/bin/env bash | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 2 | # | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 3 | # Author: Makarius | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 4 | # | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 5 | # build full Isabelle distribution from repository | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 6 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 7 | THIS="$(cd "$(dirname "$0")"; pwd)" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 8 | PRG="$(basename "$0")" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 9 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 10 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 11 | ## diagnostics | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 12 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 13 | PRG="$(basename "$0")" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 14 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 15 | function usage() | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 16 | {
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 17 | echo | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 18 | echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 19 | echo | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 20 | echo " Options are:" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 21 | echo " -j INT maximum number of parallel jobs (default 1)" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 22 | echo " -r RELEASE proper release with name" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 23 | echo | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 24 | echo " Make Isabelle distribution DIR, using the local repository clone." | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 25 | echo | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 26 | echo " VERSION identifies the snapshot, using usual Mercurial terminology;" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 27 | echo " the default is RELEASE if given, otherwise \"tip\"." | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 28 | echo | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 29 | exit 1 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 30 | } | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 31 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 32 | function fail() | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 33 | {
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 34 | echo "$1" >&2 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 35 | exit 2 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 36 | } | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 37 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 38 | function check_number() | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 39 | {
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 40 | [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 41 | } | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 42 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 43 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 44 | ## process command line | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 45 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 46 | # options | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 47 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 48 | JOBS="" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 49 | RELEASE="" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 50 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 51 | while getopts "j:r:" OPT | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 52 | do | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 53 | case "$OPT" in | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 54 | j) | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 55 | check_number "$OPTARG" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 56 | JOBS="-j $OPTARG" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 57 | ;; | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 58 | r) | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 59 | RELEASE="$OPTARG" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 60 | ;; | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 61 | \?) | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 62 | usage | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 63 | ;; | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 64 | esac | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 65 | done | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 66 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 67 | shift $(($OPTIND - 1)) | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 68 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 69 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 70 | # args | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 71 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 72 | BASE_DIR="" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 73 | [ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; }
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 74 | [ -z "$BASE_DIR" ] && usage | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 75 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 76 | VERSION="" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 77 | [ "$#" -gt 0 ] && { VERSION="$1"; shift; }
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 78 | [ -z "$VERSION" ] && VERSION="$RELEASE" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 79 | [ -z "$VERSION" ] && VERSION="tip" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 80 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 81 | [ "$#" -gt 0 ] && usage | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 82 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 83 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 84 | ## Isabelle settings | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 85 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 86 | ISABELLE_TOOL="$THIS/../../bin/isabelle" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 87 | ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)"
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 88 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 89 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 90 | ## main | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 91 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 92 | if [ -z "$RELEASE" ]; then | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 93 | DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 94 | "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 95 | else | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 96 | DISTNAME="$RELEASE" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 97 | "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS -r "$RELEASE" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 98 | fi | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 99 | [ "$?" = 0 ] || exit "$?" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 100 | |
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 101 | DISTBASE="$BASE_DIR/dist-${DISTNAME}"
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 102 | |
| 51064 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 103 | |
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 104 | for PLATFORM_FAMILY in linux macos windows | 
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 105 | do | 
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 106 | |
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 107 | echo | 
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 108 | echo "*** $PLATFORM_FAMILY ***" | 
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 109 | |
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 110 | "$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY"
 | 
| 50899 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 111 | [ "$?" = 0 ] || exit "$?" | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 112 | |
| 51064 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 113 | done | 
| 
9c425ed4a52c
separate makedist_bundle for each platform family, which is more useful for manual use;
 wenzelm parents: 
50899diff
changeset | 114 | |
| 50899 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 115 | "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
 | 
| 
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
 wenzelm parents: diff
changeset | 116 |