| author | blanchet | 
| Fri, 23 Aug 2013 16:51:53 +0200 | |
| changeset 53159 | a5805fe4e91c | 
| parent 53055 | 0fe8a9972eda | 
| child 53279 | 763d35697338 | 
| permissions | -rwxr-xr-x | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 1 | #!/usr/bin/env bash | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 2 | # | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 3 | # Author: Makarius | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 4 | # | 
| 42899 | 5 | # build-jars - build Isabelle/Scala | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 6 | # | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 7 | # Requires proper Isabelle settings environment. | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 8 | |
| 43320 | 9 | ## sources | 
| 10 | ||
| 11 | declare -a SOURCES=( | |
| 43660 | 12 | Concurrent/counter.scala | 
| 43320 | 13 | Concurrent/future.scala | 
| 14 | Concurrent/simple_thread.scala | |
| 15 | Concurrent/volatile.scala | |
| 16 | General/exn.scala | |
| 48411 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 wenzelm parents: 
48410diff
changeset | 17 | General/file.scala | 
| 46611 | 18 | General/graph.scala | 
| 51098 | 19 | General/graphics_file.scala | 
| 43320 | 20 | General/linear_set.scala | 
| 52975 | 21 | General/multi_map.scala | 
| 43600 
4ac04bf9ff89
abstract algebra of file paths in Scala (cf. path.ML);
 wenzelm parents: 
43523diff
changeset | 22 | General/path.scala | 
| 43320 | 23 | General/position.scala | 
| 24 | General/pretty.scala | |
| 43780 | 25 | General/properties.scala | 
| 43320 | 26 | General/scan.scala | 
| 27 | General/sha1.scala | |
| 28 | General/symbol.scala | |
| 45674 | 29 | General/time.scala | 
| 45666 | 30 | General/timing.scala | 
| 52671 
9a360530eac8
separate module XZ_File to avoid initial dependency on org.tukaani.xz;
 wenzelm parents: 
52667diff
changeset | 31 | General/xz_file.scala | 
| 43320 | 32 | Isar/keyword.scala | 
| 33 | Isar/outer_syntax.scala | |
| 34 | Isar/parse.scala | |
| 35 | Isar/token.scala | |
| 36 | PIDE/command.scala | |
| 37 | PIDE/document.scala | |
| 52530 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
 wenzelm parents: 
52444diff
changeset | 38 | PIDE/document_id.scala | 
| 52971 
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
 wenzelm parents: 
52671diff
changeset | 39 | PIDE/editor.scala | 
| 45670 | 40 | PIDE/markup.scala | 
| 43320 | 41 | PIDE/markup_tree.scala | 
| 45709 
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
 wenzelm parents: 
45674diff
changeset | 42 | PIDE/protocol.scala | 
| 52981 | 43 | PIDE/query_operation.scala | 
| 43320 | 44 | PIDE/text.scala | 
| 44698 | 45 | PIDE/xml.scala | 
| 46 | PIDE/yxml.scala | |
| 49294 | 47 | System/color_value.scala | 
| 48346 
e2382bede914
more general support for Isabelle/Scala command line tools;
 wenzelm parents: 
48276diff
changeset | 48 | System/command_line.scala | 
| 52667 | 49 | System/cygwin_init.scala | 
| 43320 | 50 | System/event_bus.scala | 
| 51615 
072a7249e1ac
separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
 wenzelm parents: 
51614diff
changeset | 51 | System/gui.scala | 
| 43320 | 52 | System/gui_setup.scala | 
| 49066 | 53 | System/html5_panel.scala | 
| 51250 
ca13a14cc52e
support for POSIX interrupts (bypassed on Windows);
 wenzelm parents: 
51098diff
changeset | 54 | System/interrupt.scala | 
| 43744 
2c7e1565b4a3
some support to invoke Scala methods under program control;
 wenzelm parents: 
43730diff
changeset | 55 | System/invoke_scala.scala | 
| 43517 | 56 | System/isabelle_charset.scala | 
| 51614 
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
 wenzelm parents: 
51508diff
changeset | 57 | System/isabelle_font.scala | 
| 43320 | 58 | System/isabelle_process.scala | 
| 59 | System/isabelle_system.scala | |
| 49065 | 60 | System/jfx_thread.scala | 
| 48365 
d88aefda01c4
basic support for stand-alone options with external string representation;
 wenzelm parents: 
48346diff
changeset | 61 | System/options.scala | 
| 43320 | 62 | System/platform.scala | 
| 63 | System/session.scala | |
| 64 | System/swing_thread.scala | |
| 45027 
f459e93a038e
more abstract wrapping of fifos as System_Channel;
 wenzelm parents: 
44698diff
changeset | 65 | System/system_channel.scala | 
| 50203 | 66 | System/utf8.scala | 
| 43320 | 67 | Thy/completion.scala | 
| 68 | Thy/html.scala | |
| 50707 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
 wenzelm parents: 
50689diff
changeset | 69 | Thy/present.scala | 
| 43320 | 70 | Thy/thy_header.scala | 
| 43651 
511df47bcadc
some support for theory files within Isabelle/Scala session;
 wenzelm parents: 
43600diff
changeset | 71 | Thy/thy_info.scala | 
| 
511df47bcadc
some support for theory files within Isabelle/Scala session;
 wenzelm parents: 
43600diff
changeset | 72 | Thy/thy_load.scala | 
| 43320 | 73 | Thy/thy_syntax.scala | 
| 50686 | 74 | Tools/build.scala | 
| 75 | Tools/build_dialog.scala | |
| 52444 
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
 wenzelm parents: 
52439diff
changeset | 76 | Tools/doc.scala | 
| 52439 
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
 wenzelm parents: 
52427diff
changeset | 77 | Tools/keywords.scala | 
| 50687 | 78 | Tools/main.scala | 
| 50981 | 79 | Tools/ml_statistics.scala | 
| 53055 
0fe8a9972eda
some protocol to determine provers according to ML;
 wenzelm parents: 
52981diff
changeset | 80 | Tools/sledgehammer_params.scala | 
| 50980 | 81 | Tools/task_statistics.scala | 
| 43320 | 82 | library.scala | 
| 83 | package.scala | |
| 43730 
a0ed7bc688b5
lambda terms with XML data representation in Scala;
 wenzelm parents: 
43715diff
changeset | 84 | term.scala | 
| 43779 | 85 | term_xml.scala | 
| 43320 | 86 | ) | 
| 87 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 88 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 89 | ## diagnostics | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 90 | |
| 43280 | 91 | PRG="$(basename "$0")" | 
| 92 | ||
| 93 | function usage() | |
| 94 | {
 | |
| 95 | echo | |
| 96 | echo "Usage: isabelle $PRG [OPTIONS]" | |
| 97 | echo | |
| 98 | echo " Options are:" | |
| 99 | echo " -f fresh build" | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 100 | echo " -t test separate compilation of PIDE" | 
| 43280 | 101 | echo | 
| 102 | exit 1 | |
| 103 | } | |
| 104 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 105 | function fail() | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 106 | {
 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 107 | echo "$1" >&2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 108 | exit 2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 109 | } | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 110 | |
| 42899 | 111 | [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 112 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 113 | |
| 43280 | 114 | ## process command line | 
| 115 | ||
| 116 | # options | |
| 117 | ||
| 118 | FRESH="" | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 119 | TEST_PIDE="" | 
| 43280 | 120 | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 121 | while getopts "ft" OPT | 
| 43280 | 122 | do | 
| 123 | case "$OPT" in | |
| 124 | f) | |
| 125 | FRESH=true | |
| 126 | ;; | |
| 47408 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 127 | t) | 
| 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 128 | TEST_PIDE=true | 
| 
63c05991882e
slightly faster default compilation of Isabelle/Scala;
 wenzelm parents: 
47115diff
changeset | 129 | ;; | 
| 43280 | 130 | \?) | 
| 131 | usage | |
| 132 | ;; | |
| 133 | esac | |
| 134 | done | |
| 135 | ||
| 136 | shift $(($OPTIND - 1)) | |
| 137 | ||
| 138 | ||
| 139 | # args | |
| 140 | ||
| 141 | [ "$#" -ne 0 ] && usage | |
| 142 | ||
| 143 | ||
| 50689 | 144 | ## dependencies | 
| 145 | ||
| 146 | declare -a JFREECHART_JARS=() | |
| 147 | for NAME in $JFREECHART_JAR_NAMES | |
| 148 | do | |
| 149 |   JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
 | |
| 150 | done | |
| 151 | ||
| 152 | ||
| 49558 | 153 | ## build | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 154 | |
| 34284 | 155 | TARGET_DIR="$ISABELLE_HOME/lib/classes" | 
| 43523 | 156 | TARGET="$TARGET_DIR/ext/Pure.jar" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 157 | |
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 158 | declare -a PIDE_SOURCES=() | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 159 | declare -a PURE_SOURCES=() | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 160 | |
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 161 | for DEP in "${SOURCES[@]}"
 | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 162 | do | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 163 | if grep "Module:.*PIDE" "$DEP" >/dev/null | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 164 | then | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 165 |     PIDE_SOURCES["${#PIDE_SOURCES[@]}"]="$DEP"
 | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 166 | else | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 167 |     PURE_SOURCES["${#PURE_SOURCES[@]}"]="$DEP"
 | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 168 | fi | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 169 | done | 
| 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 170 | |
| 43405 | 171 | declare -a UPDATED=() | 
| 172 | ||
| 43280 | 173 | if [ -n "$FRESH" ]; then | 
| 174 | OUTDATED=true | |
| 175 | else | |
| 176 | OUTDATED=false | |
| 43523 | 177 | if [ ! -e "$TARGET" ]; then | 
| 178 | OUTDATED=true | |
| 179 | else | |
| 43405 | 180 |     for DEP in "${SOURCES[@]}"
 | 
| 43280 | 181 | do | 
| 43405 | 182 | [ ! -e "$DEP" ] && fail "Missing file: $DEP" | 
| 43523 | 183 |       [ "$DEP" -nt "$TARGET" ] && {
 | 
| 184 | OUTDATED=true | |
| 185 |         UPDATED["${#UPDATED[@]}"]="$DEP"
 | |
| 186 | } | |
| 43280 | 187 | done | 
| 43405 | 188 | fi | 
| 43280 | 189 | fi | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 190 | |
| 34284 | 191 | if [ "$OUTDATED" = true ] | 
| 192 | then | |
| 49173 
fa01a202399c
eliminated potentially confusing terminology of Scala "layer";
 wenzelm parents: 
49068diff
changeset | 193 | echo "### Building Isabelle/Scala ..." | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 194 | |
| 43405 | 195 |   [ "${#UPDATED[@]}" -gt 0 ] && {
 | 
| 196 | echo "Changed files:" | |
| 197 |     for FILE in "${UPDATED[@]}"
 | |
| 198 | do | |
| 199 | echo " $FILE" | |
| 200 | done | |
| 201 | } | |
| 202 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 203 | rm -rf classes && mkdir classes | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 204 | |
| 47009 | 205 | SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes" | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 206 | |
| 49067 | 207 | JFXRT="$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar" | 
| 208 | ||
| 50689 | 209 | ( | 
| 51504 | 210 |     for X in "$JFXRT" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar" classes
 | 
| 50689 | 211 | do | 
| 212 | CLASSPATH="$CLASSPATH:$X" | |
| 213 | done | |
| 214 | CLASSPATH="$(jvmpath "$CLASSPATH")" | |
| 215 | ||
| 216 | if [ "$TEST_PIDE" = true ]; then | |
| 217 |       isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
 | |
| 218 | fail "Failed to compile PIDE sources" | |
| 219 |       isabelle_scala scalac $SCALAC_OPTIONS "${PURE_SOURCES[@]}" || \
 | |
| 220 | fail "Failed to compile Pure sources" | |
| 221 | else | |
| 222 |       isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
 | |
| 223 | fail "Failed to compile sources" | |
| 224 | fi | |
| 51508 | 225 | ) || exit "$?" | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 226 | |
| 43523 | 227 | mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext" | 
| 43280 | 228 | |
| 43285 | 229 | pushd classes >/dev/null | 
| 43280 | 230 | |
| 43517 | 231 | CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" | 
| 232 | mkdir -p "$(dirname "$CHARSET_SERVICE")" | |
| 233 | echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" | |
| 234 | ||
| 47115 
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
 wenzelm parents: 
47113diff
changeset | 235 | isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \ | 
| 43523 | 236 | fail "Failed to produce $TARGET" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 237 | |
| 49449 | 238 | cp "$SCALA_HOME/lib/scala-compiler.jar" \ | 
| 47995 
72f52cd7c633
include scala-compiler.jar in basic Isabelle/Scala environment, to make Isabelle/jEdit console work with scala-2.10.0-M3;
 wenzelm parents: 
47849diff
changeset | 239 | "$SCALA_HOME/lib/scala-library.jar" \ | 
| 
72f52cd7c633
include scala-compiler.jar in basic Isabelle/Scala environment, to make Isabelle/jEdit console work with scala-2.10.0-M3;
 wenzelm parents: 
47849diff
changeset | 240 | "$SCALA_HOME/lib/scala-swing.jar" "$TARGET_DIR/ext" | 
| 
72f52cd7c633
include scala-compiler.jar in basic Isabelle/Scala environment, to make Isabelle/jEdit console work with scala-2.10.0-M3;
 wenzelm parents: 
47849diff
changeset | 241 | |
| 47849 | 242 | [ -e "$SCALA_HOME/lib/scala-actors.jar" ] && \ | 
| 243 | cp "$SCALA_HOME/lib/scala-actors.jar" "$TARGET_DIR/ext" | |
| 43521 
d477b92109b8
provide Isabelle/Scala environment as Java extension, instead of user classpath
 wenzelm parents: 
43517diff
changeset | 244 | |
| 49955 | 245 | [ -e "$SCALA_HOME/lib/scala-reflect.jar" ] && \ | 
| 246 | cp "$SCALA_HOME/lib/scala-reflect.jar" "$TARGET_DIR/ext" | |
| 247 | ||
| 43280 | 248 | popd >/dev/null | 
| 249 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 250 | rm -rf classes | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 251 | fi |