| author | wenzelm | 
| Tue, 14 Mar 2017 11:16:23 +0100 | |
| changeset 65223 | 844c067bc3d4 | 
| parent 65214 | a2ec0db555c7 | 
| child 65313 | 347ed6219dab | 
| 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=( | |
| 65071 | 12 | Admin/build_cygwin.scala | 
| 64161 | 13 | Admin/build_doc.scala | 
| 64890 
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
 wenzelm parents: 
64872diff
changeset | 14 | Admin/build_docker.scala | 
| 64160 | 15 | Admin/build_history.scala | 
| 64929 | 16 | Admin/build_jdk.scala | 
| 64160 | 17 | Admin/build_log.scala | 
| 64483 | 18 | Admin/build_polyml.scala | 
| 64202 | 19 | Admin/build_release.scala | 
| 64161 | 20 | Admin/build_stats.scala | 
| 21 | Admin/check_sources.scala | |
| 64160 | 22 | Admin/ci_api.scala | 
| 23 | Admin/ci_profile.scala | |
| 64148 | 24 | Admin/isabelle_cronjob.scala | 
| 64369 | 25 | Admin/news.scala | 
| 64188 | 26 | Admin/other_isabelle.scala | 
| 64161 | 27 | Admin/remote_dmg.scala | 
| 56695 
963732291084
consumer thread with unbounded queueing of requests (similar to Message_Channel in ML);
 wenzelm parents: 
56693diff
changeset | 28 | Concurrent/consumer_thread.scala | 
| 43660 | 29 | Concurrent/counter.scala | 
| 56768 | 30 | Concurrent/event_timer.scala | 
| 43320 | 31 | Concurrent/future.scala | 
| 56693 | 32 | Concurrent/mailbox.scala | 
| 59136 
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
 wenzelm parents: 
58928diff
changeset | 33 | Concurrent/par_list.scala | 
| 61556 | 34 | Concurrent/standard_thread.scala | 
| 56685 | 35 | Concurrent/synchronized.scala | 
| 57647 | 36 | GUI/color_value.scala | 
| 37 | GUI/gui.scala | |
| 38 | GUI/gui_thread.scala | |
| 39 | GUI/html5_panel.scala | |
| 57908 
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
 wenzelm parents: 
57905diff
changeset | 40 | GUI/jfx_gui.scala | 
| 57647 | 41 | GUI/popup.scala | 
| 42 | GUI/wrap_panel.scala | |
| 55511 
984e210d412e
antiquotations within plain text: Scala version in accordance to ML;
 wenzelm parents: 
55497diff
changeset | 43 | General/antiquote.scala | 
| 54439 | 44 | General/bytes.scala | 
| 64610 | 45 | General/codepoint.scala | 
| 55673 
0286219c1261
clarified module location (again, see 763d35697338);
 wenzelm parents: 
55511diff
changeset | 46 | General/completion.scala | 
| 64056 | 47 | General/date.scala | 
| 62508 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
 wenzelm parents: 
62452diff
changeset | 48 | General/exn.scala | 
| 48411 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
 wenzelm parents: 
48410diff
changeset | 49 | General/file.scala | 
| 64699 | 50 | General/file_watcher.scala | 
| 46611 | 51 | General/graph.scala | 
| 59244 
19b5fc4b2b38
more uniform support for graph display in ML/Scala;
 wenzelm parents: 
59232diff
changeset | 52 | General/graph_display.scala | 
| 51098 | 53 | General/graphics_file.scala | 
| 65077 | 54 | General/http.scala | 
| 63644 | 55 | General/json.scala | 
| 43320 | 56 | General/linear_set.scala | 
| 64606 | 57 | General/logger.scala | 
| 56800 | 58 | General/long_name.scala | 
| 63997 
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
 wenzelm parents: 
63823diff
changeset | 59 | General/mercurial.scala | 
| 52975 | 60 | General/multi_map.scala | 
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: 
56768diff
changeset | 61 | General/output.scala | 
| 43600 
4ac04bf9ff89
abstract algebra of file paths in Scala (cf. path.ML);
 wenzelm parents: 
43523diff
changeset | 62 | General/path.scala | 
| 43320 | 63 | General/position.scala | 
| 64 | General/pretty.scala | |
| 43780 | 65 | General/properties.scala | 
| 43320 | 66 | General/scan.scala | 
| 67 | General/sha1.scala | |
| 63788 | 68 | General/sql.scala | 
| 64123 | 69 | General/ssh.scala | 
| 43320 | 70 | General/symbol.scala | 
| 45674 | 71 | General/time.scala | 
| 45666 | 72 | General/timing.scala | 
| 57647 | 73 | General/untyped.scala | 
| 56501 
5fda9e5c5874
basic URL operations (with Isabelle/Scala error handling);
 wenzelm parents: 
56429diff
changeset | 74 | General/url.scala | 
| 64639 | 75 | General/utf8.scala | 
| 63805 | 76 | General/value.scala | 
| 56599 | 77 | General/word.scala | 
| 64000 | 78 | General/xz.scala | 
| 63604 | 79 | Isar/document_structure.scala | 
| 43320 | 80 | Isar/keyword.scala | 
| 63603 | 81 | Isar/line_structure.scala | 
| 43320 | 82 | Isar/outer_syntax.scala | 
| 83 | Isar/parse.scala | |
| 84 | Isar/token.scala | |
| 55497 | 85 | ML/ml_lex.scala | 
| 62528 | 86 | ML/ml_syntax.scala | 
| 59362 | 87 | PIDE/batch_session.scala | 
| 43320 | 88 | PIDE/command.scala | 
| 57905 
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
 wenzelm parents: 
57900diff
changeset | 89 | PIDE/command_span.scala | 
| 43320 | 90 | PIDE/document.scala | 
| 52530 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
 wenzelm parents: 
52444diff
changeset | 91 | PIDE/document_id.scala | 
| 52971 
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
 wenzelm parents: 
52671diff
changeset | 92 | PIDE/editor.scala | 
| 64611 | 93 | PIDE/line.scala | 
| 45670 | 94 | PIDE/markup.scala | 
| 43320 | 95 | PIDE/markup_tree.scala | 
| 45709 
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
 wenzelm parents: 
45674diff
changeset | 96 | PIDE/protocol.scala | 
| 65214 | 97 | PIDE/protocol_handlers.scala | 
| 59713 | 98 | PIDE/protocol_message.scala | 
| 56385 | 99 | PIDE/prover.scala | 
| 52981 | 100 | PIDE/query_operation.scala | 
| 64622 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
 wenzelm parents: 
64617diff
changeset | 101 | PIDE/rendering.scala | 
| 56208 | 102 | PIDE/resources.scala | 
| 56210 | 103 | PIDE/session.scala | 
| 43320 | 104 | PIDE/text.scala | 
| 44698 | 105 | PIDE/xml.scala | 
| 106 | PIDE/yxml.scala | |
| 57647 | 107 | ROOT.scala | 
| 62584 | 108 | System/bash.scala | 
| 61925 | 109 | System/command_line.scala | 
| 61282 | 110 | System/cygwin.scala | 
| 62845 | 111 | System/distribution.scala | 
| 62431 | 112 | System/getopts.scala | 
| 43744 
2c7e1565b4a3
some support to invoke Scala methods under program control;
 wenzelm parents: 
43730diff
changeset | 113 | System/invoke_scala.scala | 
| 43517 | 114 | System/isabelle_charset.scala | 
| 43320 | 115 | System/isabelle_process.scala | 
| 116 | System/isabelle_system.scala | |
| 62829 
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
 wenzelm parents: 
62631diff
changeset | 117 | System/isabelle_tool.scala | 
| 64264 
42138702d6ec
support for Non-Uniform Memory Access of separate CPU nodes;
 wenzelm parents: 
64202diff
changeset | 118 | System/numa.scala | 
| 48365 
d88aefda01c4
basic support for stand-alone options with external string representation;
 wenzelm parents: 
48346diff
changeset | 119 | System/options.scala | 
| 43320 | 120 | System/platform.scala | 
| 56860 | 121 | System/posix_interrupt.scala | 
| 62400 | 122 | System/process_result.scala | 
| 61276 | 123 | System/progress.scala | 
| 45027 
f459e93a038e
more abstract wrapping of fifos as System_Channel;
 wenzelm parents: 
44698diff
changeset | 124 | System/system_channel.scala | 
| 43320 | 125 | Thy/html.scala | 
| 50707 
5b2bf7611662
maintain session index on Scala side, for more determistic results;
 wenzelm parents: 
50689diff
changeset | 126 | Thy/present.scala | 
| 62631 | 127 | Thy/sessions.scala | 
| 43320 | 128 | Thy/thy_header.scala | 
| 43651 
511df47bcadc
some support for theory files within Isabelle/Scala session;
 wenzelm parents: 
43600diff
changeset | 129 | Thy/thy_info.scala | 
| 43320 | 130 | Thy/thy_syntax.scala | 
| 58523 | 131 | Tools/bibtex.scala | 
| 57647 | 132 | Tools/build.scala | 
| 59891 
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
 wenzelm parents: 
59713diff
changeset | 133 | Tools/check_keywords.scala | 
| 60749 | 134 | Tools/debugger.scala | 
| 52444 
2cfe6656d6d6
slightly improved "isabelle doc" based on Isabelle/Scala;
 wenzelm parents: 
52439diff
changeset | 135 | Tools/doc.scala | 
| 50687 | 136 | Tools/main.scala | 
| 62559 | 137 | Tools/ml_console.scala | 
| 62586 | 138 | Tools/ml_process.scala | 
| 50981 | 139 | Tools/ml_statistics.scala | 
| 56864 | 140 | Tools/print_operation.scala | 
| 64342 | 141 | Tools/profiling_report.scala | 
| 54730 | 142 | Tools/simplifier_trace.scala | 
| 65139 | 143 | Tools/spell_checker.scala | 
| 50980 | 144 | Tools/task_statistics.scala | 
| 58610 | 145 | Tools/update_cartouches.scala | 
| 58872 | 146 | Tools/update_header.scala | 
| 61216 | 147 | Tools/update_then.scala | 
| 61337 | 148 | Tools/update_theorems.scala | 
| 43320 | 149 | library.scala | 
| 43730 
a0ed7bc688b5
lambda terms with XML data representation in Scala;
 wenzelm parents: 
43715diff
changeset | 150 | term.scala | 
| 43779 | 151 | term_xml.scala | 
| 64609 | 152 | ../Tools/Graphview/graph_file.scala | 
| 153 | ../Tools/Graphview/graph_panel.scala | |
| 154 | ../Tools/Graphview/graphview.scala | |
| 155 | ../Tools/Graphview/layout.scala | |
| 156 | ../Tools/Graphview/main_panel.scala | |
| 157 | ../Tools/Graphview/metrics.scala | |
| 158 | ../Tools/Graphview/model.scala | |
| 159 | ../Tools/Graphview/mutator.scala | |
| 160 | ../Tools/Graphview/mutator_dialog.scala | |
| 161 | ../Tools/Graphview/mutator_event.scala | |
| 162 | ../Tools/Graphview/popups.scala | |
| 163 | ../Tools/Graphview/shapes.scala | |
| 164 | ../Tools/Graphview/tree_panel.scala | |
| 65138 | 165 | ../Tools/VSCode/src/build_vscode.scala | 
| 64609 | 166 | ../Tools/VSCode/src/channel.scala | 
| 167 | ../Tools/VSCode/src/document_model.scala | |
| 65191 
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
 wenzelm parents: 
65139diff
changeset | 168 | ../Tools/VSCode/src/dynamic_output.scala | 
| 64738 
bcdecd466cb2
generate static TextMate grammar for VSCode editor;
 wenzelm parents: 
64699diff
changeset | 169 | ../Tools/VSCode/src/grammar.scala | 
| 64609 | 170 | ../Tools/VSCode/src/protocol.scala | 
| 171 | ../Tools/VSCode/src/server.scala | |
| 64622 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
 wenzelm parents: 
64617diff
changeset | 172 | ../Tools/VSCode/src/vscode_rendering.scala | 
| 64623 | 173 | ../Tools/VSCode/src/vscode_resources.scala | 
| 43320 | 174 | ) | 
| 175 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 176 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 177 | ## diagnostics | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 178 | |
| 43280 | 179 | PRG="$(basename "$0")" | 
| 180 | ||
| 181 | function usage() | |
| 182 | {
 | |
| 183 | echo | |
| 184 | echo "Usage: isabelle $PRG [OPTIONS]" | |
| 185 | echo | |
| 186 | echo " Options are:" | |
| 187 | echo " -f fresh build" | |
| 188 | echo | |
| 189 | exit 1 | |
| 190 | } | |
| 191 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 192 | function fail() | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 193 | {
 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 194 | echo "$1" >&2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 195 | exit 2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 196 | } | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 197 | |
| 42899 | 198 | [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 199 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 200 | |
| 43280 | 201 | ## process command line | 
| 202 | ||
| 203 | # options | |
| 204 | ||
| 205 | FRESH="" | |
| 206 | ||
| 64370 
865b39487b5d
discontinued unused / untested distinction of separate PIDE modules;
 wenzelm parents: 
64369diff
changeset | 207 | while getopts "f" OPT | 
| 43280 | 208 | do | 
| 209 | case "$OPT" in | |
| 210 | f) | |
| 211 | FRESH=true | |
| 212 | ;; | |
| 213 | \?) | |
| 214 | usage | |
| 215 | ;; | |
| 216 | esac | |
| 217 | done | |
| 218 | ||
| 219 | shift $(($OPTIND - 1)) | |
| 220 | ||
| 221 | ||
| 222 | # args | |
| 223 | ||
| 224 | [ "$#" -ne 0 ] && usage | |
| 225 | ||
| 226 | ||
| 49558 | 227 | ## build | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 228 | |
| 34284 | 229 | TARGET_DIR="$ISABELLE_HOME/lib/classes" | 
| 53577 | 230 | TARGET="$TARGET_DIR/Pure.jar" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 231 | |
| 43405 | 232 | declare -a UPDATED=() | 
| 233 | ||
| 43280 | 234 | if [ -n "$FRESH" ]; then | 
| 235 | OUTDATED=true | |
| 236 | else | |
| 237 | OUTDATED=false | |
| 43523 | 238 | if [ ! -e "$TARGET" ]; then | 
| 239 | OUTDATED=true | |
| 240 | else | |
| 43405 | 241 |     for DEP in "${SOURCES[@]}"
 | 
| 43280 | 242 | do | 
| 43405 | 243 | [ ! -e "$DEP" ] && fail "Missing file: $DEP" | 
| 43523 | 244 |       [ "$DEP" -nt "$TARGET" ] && {
 | 
| 245 | OUTDATED=true | |
| 246 |         UPDATED["${#UPDATED[@]}"]="$DEP"
 | |
| 247 | } | |
| 43280 | 248 | done | 
| 43405 | 249 | fi | 
| 43280 | 250 | fi | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 251 | |
| 34284 | 252 | if [ "$OUTDATED" = true ] | 
| 253 | then | |
| 49173 
fa01a202399c
eliminated potentially confusing terminology of Scala "layer";
 wenzelm parents: 
49068diff
changeset | 254 | echo "### Building Isabelle/Scala ..." | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 255 | |
| 43405 | 256 |   [ "${#UPDATED[@]}" -gt 0 ] && {
 | 
| 257 | echo "Changed files:" | |
| 258 |     for FILE in "${UPDATED[@]}"
 | |
| 259 | do | |
| 260 | echo " $FILE" | |
| 261 | done | |
| 262 | } | |
| 263 | ||
| 64375 
74a2af7c5145
remove old target: it is on the classpath and may break scalac;
 wenzelm parents: 
64370diff
changeset | 264 | rm -f "$TARGET" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 265 | rm -rf classes && mkdir classes | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 266 | |
| 64900 | 267 | SCALAC_OPTIONS="$ISABELLE_SCALAC_OPTIONS -d classes" | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 268 | |
| 50689 | 269 | ( | 
| 58791 | 270 | classpath "$JAVA_HOME/lib/jfxrt.jar" | 
| 53576 
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
 wenzelm parents: 
53519diff
changeset | 271 | classpath classes | 
| 61294 | 272 | export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" | 
| 50689 | 273 | |
| 64370 
865b39487b5d
discontinued unused / untested distinction of separate PIDE modules;
 wenzelm parents: 
64369diff
changeset | 274 |     isabelle_scala scalac $SCALAC_OPTIONS "${SOURCES[@]}" || \
 | 
| 
865b39487b5d
discontinued unused / untested distinction of separate PIDE modules;
 wenzelm parents: 
64369diff
changeset | 275 | fail "Failed to compile sources" | 
| 51508 | 276 | ) || exit "$?" | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 277 | |
| 53577 | 278 | mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR" | 
| 43280 | 279 | |
| 43285 | 280 | pushd classes >/dev/null | 
| 43280 | 281 | |
| 43517 | 282 | CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" | 
| 283 | mkdir -p "$(dirname "$CHARSET_SERVICE")" | |
| 284 | echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" | |
| 285 | ||
| 54676 
6b2ca4850b71
uniform use of transparent icons, as for main "apps";
 wenzelm parents: 
54671diff
changeset | 286 | cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/. | 
| 54709 | 287 | cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/. | 
| 53452 
8181bc357dc4
more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;
 wenzelm parents: 
53279diff
changeset | 288 | |
| 61294 | 289 | isabelle_jdk jar cfe "$(platform_path "$TARGET")" isabelle.Main META-INF isabelle || \ | 
| 43523 | 290 | fail "Failed to produce $TARGET" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 291 | |
| 43280 | 292 | popd >/dev/null | 
| 293 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 294 | rm -rf classes | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 295 | fi |