| author | wenzelm | 
| Sat, 10 Oct 2020 21:45:58 +0200 | |
| changeset 72428 | b7351ffe0dbc | 
| parent 72421 | 9a8bc089890d | 
| child 72439 | 7f6800b2e8c2 | 
| 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=( | |
| 72176 | 12 | src/HOL/Tools/Nitpick/kodkod.scala | 
| 71367 | 13 | src/Pure/Admin/afp.scala | 
| 72414 
af24c0dd6975
build Isabelle CSDP component from official downloads;
 wenzelm parents: 
72411diff
changeset | 14 | src/Pure/Admin/build_csdp.scala | 
| 71367 | 15 | src/Pure/Admin/build_cygwin.scala | 
| 16 | src/Pure/Admin/build_doc.scala | |
| 72363 
fc5f10691147
build Isabelle E prover component from official downloads;
 wenzelm parents: 
72346diff
changeset | 17 | src/Pure/Admin/build_e.scala | 
| 71367 | 18 | src/Pure/Admin/build_fonts.scala | 
| 19 | src/Pure/Admin/build_history.scala | |
| 20 | src/Pure/Admin/build_jdk.scala | |
| 21 | src/Pure/Admin/build_log.scala | |
| 22 | src/Pure/Admin/build_polyml.scala | |
| 23 | src/Pure/Admin/build_release.scala | |
| 72411 
b8cc129ece05
build Isabelle SPASS component from unofficial download;
 wenzelm parents: 
72363diff
changeset | 24 | src/Pure/Admin/build_spass.scala | 
| 72346 
93e533198bf6
build Isabelle sqlite-jdbc component from official download;
 wenzelm parents: 
72338diff
changeset | 25 | src/Pure/Admin/build_sqlite.scala | 
| 71367 | 26 | src/Pure/Admin/build_status.scala | 
| 27 | src/Pure/Admin/check_sources.scala | |
| 28 | src/Pure/Admin/ci_profile.scala | |
| 29 | src/Pure/Admin/components.scala | |
| 30 | src/Pure/Admin/isabelle_cronjob.scala | |
| 31 | src/Pure/Admin/isabelle_devel.scala | |
| 32 | src/Pure/Admin/jenkins.scala | |
| 33 | src/Pure/Admin/other_isabelle.scala | |
| 34 | src/Pure/Concurrent/consumer_thread.scala | |
| 35 | src/Pure/Concurrent/counter.scala | |
| 71704 | 36 | src/Pure/Concurrent/delay.scala | 
| 71367 | 37 | src/Pure/Concurrent/event_timer.scala | 
| 38 | src/Pure/Concurrent/future.scala | |
| 71692 | 39 | src/Pure/Concurrent/isabelle_thread.scala | 
| 71367 | 40 | src/Pure/Concurrent/mailbox.scala | 
| 41 | src/Pure/Concurrent/par_list.scala | |
| 42 | src/Pure/Concurrent/synchronized.scala | |
| 43 | src/Pure/GUI/color_value.scala | |
| 44 | src/Pure/GUI/gui.scala | |
| 45 | src/Pure/GUI/gui_thread.scala | |
| 46 | src/Pure/GUI/popup.scala | |
| 47 | src/Pure/GUI/wrap_panel.scala | |
| 48 | src/Pure/General/antiquote.scala | |
| 49 | src/Pure/General/bytes.scala | |
| 50 | src/Pure/General/cache.scala | |
| 51 | src/Pure/General/codepoint.scala | |
| 52 | src/Pure/General/comment.scala | |
| 53 | src/Pure/General/completion.scala | |
| 54 | src/Pure/General/csv.scala | |
| 55 | src/Pure/General/date.scala | |
| 56 | src/Pure/General/exn.scala | |
| 57 | src/Pure/General/file.scala | |
| 58 | src/Pure/General/file_watcher.scala | |
| 59 | src/Pure/General/graph.scala | |
| 60 | src/Pure/General/graph_display.scala | |
| 61 | src/Pure/General/graphics_file.scala | |
| 62 | src/Pure/General/http.scala | |
| 63 | src/Pure/General/json.scala | |
| 64 | src/Pure/General/linear_set.scala | |
| 65 | src/Pure/General/logger.scala | |
| 66 | src/Pure/General/long_name.scala | |
| 67 | src/Pure/General/mercurial.scala | |
| 68 | src/Pure/General/multi_map.scala | |
| 69 | src/Pure/General/output.scala | |
| 70 | src/Pure/General/path.scala | |
| 71 | src/Pure/General/position.scala | |
| 72 | src/Pure/General/pretty.scala | |
| 73 | src/Pure/General/properties.scala | |
| 74 | src/Pure/General/rdf.scala | |
| 75 | src/Pure/General/scan.scala | |
| 76 | src/Pure/General/sha1.scala | |
| 77 | src/Pure/General/sql.scala | |
| 78 | src/Pure/General/ssh.scala | |
| 79 | src/Pure/General/symbol.scala | |
| 80 | src/Pure/General/time.scala | |
| 81 | src/Pure/General/timing.scala | |
| 82 | src/Pure/General/untyped.scala | |
| 83 | src/Pure/General/url.scala | |
| 84 | src/Pure/General/utf8.scala | |
| 85 | src/Pure/General/uuid.scala | |
| 86 | src/Pure/General/value.scala | |
| 87 | src/Pure/General/word.scala | |
| 88 | src/Pure/General/xz.scala | |
| 89 | src/Pure/Isar/document_structure.scala | |
| 90 | src/Pure/Isar/keyword.scala | |
| 91 | src/Pure/Isar/line_structure.scala | |
| 92 | src/Pure/Isar/outer_syntax.scala | |
| 93 | src/Pure/Isar/parse.scala | |
| 94 | src/Pure/Isar/token.scala | |
| 95 | src/Pure/ML/ml_console.scala | |
| 96 | src/Pure/ML/ml_lex.scala | |
| 97 | src/Pure/ML/ml_process.scala | |
| 98 | src/Pure/ML/ml_statistics.scala | |
| 99 | src/Pure/ML/ml_syntax.scala | |
| 100 | src/Pure/PIDE/byte_message.scala | |
| 101 | src/Pure/PIDE/command.scala | |
| 102 | src/Pure/PIDE/command_span.scala | |
| 103 | src/Pure/PIDE/document.scala | |
| 104 | src/Pure/PIDE/document_id.scala | |
| 105 | src/Pure/PIDE/document_status.scala | |
| 106 | src/Pure/PIDE/editor.scala | |
| 107 | src/Pure/PIDE/headless.scala | |
| 108 | src/Pure/PIDE/line.scala | |
| 109 | src/Pure/PIDE/markup.scala | |
| 110 | src/Pure/PIDE/markup_tree.scala | |
| 111 | src/Pure/PIDE/protocol.scala | |
| 112 | src/Pure/PIDE/protocol_handlers.scala | |
| 113 | src/Pure/PIDE/protocol_message.scala | |
| 114 | src/Pure/PIDE/prover.scala | |
| 115 | src/Pure/PIDE/query_operation.scala | |
| 116 | src/Pure/PIDE/rendering.scala | |
| 117 | src/Pure/PIDE/resources.scala | |
| 118 | src/Pure/PIDE/session.scala | |
| 119 | src/Pure/PIDE/text.scala | |
| 120 | src/Pure/PIDE/xml.scala | |
| 121 | src/Pure/PIDE/yxml.scala | |
| 122 | src/Pure/ROOT.scala | |
| 123 | src/Pure/System/bash.scala | |
| 124 | src/Pure/System/command_line.scala | |
| 125 | src/Pure/System/cygwin.scala | |
| 126 | src/Pure/System/distribution.scala | |
| 127 | src/Pure/System/getopts.scala | |
| 128 | src/Pure/System/isabelle_charset.scala | |
| 129 | src/Pure/System/isabelle_fonts.scala | |
| 72338 | 130 | src/Pure/System/isabelle_platform.scala | 
| 71367 | 131 | src/Pure/System/isabelle_process.scala | 
| 132 | src/Pure/System/isabelle_system.scala | |
| 133 | src/Pure/System/isabelle_tool.scala | |
| 72250 | 134 | src/Pure/System/java_statistics.scala | 
| 71367 | 135 | src/Pure/System/linux.scala | 
| 72421 | 136 | src/Pure/System/mingw.scala | 
| 71367 | 137 | src/Pure/System/numa.scala | 
| 138 | src/Pure/System/options.scala | |
| 139 | src/Pure/System/platform.scala | |
| 140 | src/Pure/System/posix_interrupt.scala | |
| 141 | src/Pure/System/process_result.scala | |
| 142 | src/Pure/System/progress.scala | |
| 71849 | 143 | src/Pure/System/scala.scala | 
| 71367 | 144 | src/Pure/System/system_channel.scala | 
| 145 | src/Pure/System/tty_loop.scala | |
| 146 | src/Pure/Thy/bibtex.scala | |
| 147 | src/Pure/Thy/export.scala | |
| 148 | src/Pure/Thy/export_theory.scala | |
| 149 | src/Pure/Thy/file_format.scala | |
| 150 | src/Pure/Thy/html.scala | |
| 151 | src/Pure/Thy/latex.scala | |
| 152 | src/Pure/Thy/present.scala | |
| 153 | src/Pure/Thy/sessions.scala | |
| 154 | src/Pure/Thy/thy_element.scala | |
| 155 | src/Pure/Thy/thy_header.scala | |
| 156 | src/Pure/Thy/thy_syntax.scala | |
| 157 | src/Pure/Tools/build.scala | |
| 158 | src/Pure/Tools/build_docker.scala | |
| 159 | src/Pure/Tools/check_keywords.scala | |
| 160 | src/Pure/Tools/debugger.scala | |
| 161 | src/Pure/Tools/doc.scala | |
| 162 | src/Pure/Tools/dump.scala | |
| 163 | src/Pure/Tools/fontforge.scala | |
| 164 | src/Pure/Tools/main.scala | |
| 165 | src/Pure/Tools/mkroot.scala | |
| 166 | src/Pure/Tools/phabricator.scala | |
| 167 | src/Pure/Tools/print_operation.scala | |
| 168 | src/Pure/Tools/profiling_report.scala | |
| 71378 
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
 wenzelm parents: 
71375diff
changeset | 169 | src/Pure/Tools/scala_project.scala | 
| 71367 | 170 | src/Pure/Tools/server.scala | 
| 171 | src/Pure/Tools/server_commands.scala | |
| 172 | src/Pure/Tools/simplifier_trace.scala | |
| 173 | src/Pure/Tools/spell_checker.scala | |
| 174 | src/Pure/Tools/task_statistics.scala | |
| 175 | src/Pure/Tools/update.scala | |
| 176 | src/Pure/Tools/update_cartouches.scala | |
| 177 | src/Pure/Tools/update_comments.scala | |
| 178 | src/Pure/Tools/update_header.scala | |
| 179 | src/Pure/Tools/update_then.scala | |
| 180 | src/Pure/Tools/update_theorems.scala | |
| 181 | src/Pure/library.scala | |
| 182 | src/Pure/pure_thy.scala | |
| 183 | src/Pure/term.scala | |
| 184 | src/Pure/term_xml.scala | |
| 185 | src/Pure/thm_name.scala | |
| 186 | src/Tools/Graphview/graph_file.scala | |
| 187 | src/Tools/Graphview/graph_panel.scala | |
| 188 | src/Tools/Graphview/graphview.scala | |
| 189 | src/Tools/Graphview/layout.scala | |
| 190 | src/Tools/Graphview/main_panel.scala | |
| 191 | src/Tools/Graphview/metrics.scala | |
| 192 | src/Tools/Graphview/model.scala | |
| 193 | src/Tools/Graphview/mutator.scala | |
| 194 | src/Tools/Graphview/mutator_dialog.scala | |
| 195 | src/Tools/Graphview/mutator_event.scala | |
| 196 | src/Tools/Graphview/popups.scala | |
| 197 | src/Tools/Graphview/shapes.scala | |
| 198 | src/Tools/Graphview/tree_panel.scala | |
| 199 | src/Tools/VSCode/src/build_vscode.scala | |
| 200 | src/Tools/VSCode/src/channel.scala | |
| 201 | src/Tools/VSCode/src/document_model.scala | |
| 202 | src/Tools/VSCode/src/dynamic_output.scala | |
| 203 | src/Tools/VSCode/src/grammar.scala | |
| 204 | src/Tools/VSCode/src/preview_panel.scala | |
| 205 | src/Tools/VSCode/src/protocol.scala | |
| 206 | src/Tools/VSCode/src/server.scala | |
| 207 | src/Tools/VSCode/src/state_panel.scala | |
| 208 | src/Tools/VSCode/src/vscode_rendering.scala | |
| 209 | src/Tools/VSCode/src/vscode_resources.scala | |
| 210 | src/Tools/VSCode/src/vscode_spell_checker.scala | |
| 43320 | 211 | ) | 
| 212 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 213 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 214 | ## diagnostics | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 215 | |
| 43280 | 216 | PRG="$(basename "$0")" | 
| 217 | ||
| 218 | function usage() | |
| 219 | {
 | |
| 220 | echo | |
| 221 | echo "Usage: isabelle $PRG [OPTIONS]" | |
| 222 | echo | |
| 223 | echo " Options are:" | |
| 224 | echo " -f fresh build" | |
| 225 | echo | |
| 226 | exit 1 | |
| 227 | } | |
| 228 | ||
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 229 | function fail() | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 230 | {
 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 231 | echo "$1" >&2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 232 | exit 2 | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 233 | } | 
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 234 | |
| 42899 | 235 | [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 236 | |
| 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 237 | |
| 43280 | 238 | ## process command line | 
| 239 | ||
| 240 | # options | |
| 241 | ||
| 242 | FRESH="" | |
| 243 | ||
| 64370 
865b39487b5d
discontinued unused / untested distinction of separate PIDE modules;
 wenzelm parents: 
64369diff
changeset | 244 | while getopts "f" OPT | 
| 43280 | 245 | do | 
| 246 | case "$OPT" in | |
| 247 | f) | |
| 248 | FRESH=true | |
| 249 | ;; | |
| 250 | \?) | |
| 251 | usage | |
| 252 | ;; | |
| 253 | esac | |
| 254 | done | |
| 255 | ||
| 256 | shift $(($OPTIND - 1)) | |
| 257 | ||
| 258 | ||
| 259 | # args | |
| 260 | ||
| 261 | [ "$#" -ne 0 ] && usage | |
| 262 | ||
| 263 | ||
| 71367 | 264 | ## target | 
| 265 | ||
| 266 | TARGET_DIR="lib/classes" | |
| 267 | TARGET_JAR="$TARGET_DIR/Pure.jar" | |
| 268 | TARGET_SHASUM="$TARGET_DIR/Pure.shasum" | |
| 269 | ||
| 71374 | 270 | function target_shasum() | 
| 271 | {
 | |
| 272 |   shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null
 | |
| 273 | } | |
| 274 | ||
| 71367 | 275 | function target_clean() | 
| 276 | {
 | |
| 277 | rm -rf "$TARGET_DIR" | |
| 278 | } | |
| 279 | ||
| 280 | [ -n "$FRESH" ] && target_clean | |
| 281 | ||
| 282 | ||
| 49558 | 283 | ## build | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 284 | |
| 71375 | 285 | target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null | 
| 71367 | 286 | if [ "$?" -ne 0 ]; then | 
| 49173 
fa01a202399c
eliminated potentially confusing terminology of Scala "layer";
 wenzelm parents: 
49068diff
changeset | 287 | echo "### Building Isabelle/Scala ..." | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 288 | |
| 71367 | 289 | target_clean | 
| 43405 | 290 | |
| 71367 | 291 | BUILD_DIR="$TARGET_DIR/build" | 
| 292 | mkdir -p "$BUILD_DIR" | |
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45672diff
changeset | 293 | |
| 50689 | 294 | ( | 
| 61294 | 295 | export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" | 
| 71367 | 296 | isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \ | 
| 297 |       -d "$BUILD_DIR" "${SOURCES[@]}"
 | |
| 298 | ) || fail "Failed to compile sources" | |
| 43280 | 299 | |
| 43517 | 300 | CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" | 
| 71367 | 301 | mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")" | 
| 302 | echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE" | |
| 43517 | 303 | |
| 71367 | 304 | cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/." | 
| 305 | cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/." | |
| 53452 
8181bc357dc4
more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;
 wenzelm parents: 
53279diff
changeset | 306 | |
| 71367 | 307 | isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \ | 
| 308 | -C "$BUILD_DIR" META-INF \ | |
| 309 | -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR" | |
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 310 | |
| 71367 | 311 | rm -rf "$BUILD_DIR" | 
| 43280 | 312 | |
| 71367 | 313 | target_shasum > "$TARGET_SHASUM" | 
| 34282 
549969a7f582
simplified build/bootstrap of Isabelle/Scala components -- avoid make;
 wenzelm parents: diff
changeset | 314 | fi |