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