diff --git a/src/Pure/System/mingw.scala b/src/Pure/System/mingw.scala new file mode 100644 --- /dev/null +++ b/src/Pure/System/mingw.scala @@ -0,0 +1,52 @@ +/* Title: Pure/System/mingw.scala + Author: Makarius + +Support for MSYS2/MinGW64 on Windows. +*/ + +package isabelle + + +object MinGW +{ + val none: Context = new Context(None) + def context(root: Path) = new Context(Some(root)) + + def environment: List[(String, String)] = + List("PATH" -> "/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE" -> "/mingw64/etc/config.site") + + def environment_prefix: String = + (for ((a, b) <- environment) yield Bash.string(a) + "=" + Bash.string(b)) + .mkString("/usr/bin/env ", " ", " ") + + class Context private[MinGW](val root: Option[Path]) + { + override def toString: String = + root match { + case None => "MinGW.none" + case Some(msys_root) => "MinGW.context(" + msys_root.toString + ")" + } + + def bash_command(command: String): String = + root match { + case None => command + case Some(msys_root) => + File.bash_path(msys_root + Path.explode("usr/bin/bash")) + + " -c " + Bash.string(environment_prefix + command) + } + + def get_root: Path = + if (!Platform.is_windows) error("Windows platform required") + else if (root.isEmpty) error("Windows platform needs specification of msys root directory") + else root.get + + def check + { + if (Platform.is_windows) { + get_root + val result = Isabelle_System.bash(bash_command("uname -s")).check + if (!result.out.startsWith("MSYS")) error("Bad msys installation " + get_root) + } + } + } +} diff --git a/src/Pure/build-jars b/src/Pure/build-jars --- a/src/Pure/build-jars +++ b/src/Pure/build-jars @@ -1,313 +1,314 @@ #!/usr/bin/env bash # # Author: Makarius # # build-jars - build Isabelle/Scala # # Requires proper Isabelle settings environment. ## sources declare -a SOURCES=( src/HOL/Tools/Nitpick/kodkod.scala src/Pure/Admin/afp.scala src/Pure/Admin/build_csdp.scala src/Pure/Admin/build_cygwin.scala src/Pure/Admin/build_doc.scala src/Pure/Admin/build_e.scala src/Pure/Admin/build_fonts.scala src/Pure/Admin/build_history.scala src/Pure/Admin/build_jdk.scala src/Pure/Admin/build_log.scala src/Pure/Admin/build_polyml.scala src/Pure/Admin/build_release.scala src/Pure/Admin/build_spass.scala src/Pure/Admin/build_sqlite.scala src/Pure/Admin/build_status.scala src/Pure/Admin/check_sources.scala src/Pure/Admin/ci_profile.scala src/Pure/Admin/components.scala src/Pure/Admin/isabelle_cronjob.scala src/Pure/Admin/isabelle_devel.scala src/Pure/Admin/jenkins.scala src/Pure/Admin/other_isabelle.scala src/Pure/Concurrent/consumer_thread.scala src/Pure/Concurrent/counter.scala src/Pure/Concurrent/delay.scala src/Pure/Concurrent/event_timer.scala src/Pure/Concurrent/future.scala src/Pure/Concurrent/isabelle_thread.scala src/Pure/Concurrent/mailbox.scala src/Pure/Concurrent/par_list.scala src/Pure/Concurrent/synchronized.scala src/Pure/GUI/color_value.scala src/Pure/GUI/gui.scala src/Pure/GUI/gui_thread.scala src/Pure/GUI/popup.scala src/Pure/GUI/wrap_panel.scala src/Pure/General/antiquote.scala src/Pure/General/bytes.scala src/Pure/General/cache.scala src/Pure/General/codepoint.scala src/Pure/General/comment.scala src/Pure/General/completion.scala src/Pure/General/csv.scala src/Pure/General/date.scala src/Pure/General/exn.scala src/Pure/General/file.scala src/Pure/General/file_watcher.scala src/Pure/General/graph.scala src/Pure/General/graph_display.scala src/Pure/General/graphics_file.scala src/Pure/General/http.scala src/Pure/General/json.scala src/Pure/General/linear_set.scala src/Pure/General/logger.scala src/Pure/General/long_name.scala src/Pure/General/mercurial.scala src/Pure/General/multi_map.scala src/Pure/General/output.scala src/Pure/General/path.scala src/Pure/General/position.scala src/Pure/General/pretty.scala src/Pure/General/properties.scala src/Pure/General/rdf.scala src/Pure/General/scan.scala src/Pure/General/sha1.scala src/Pure/General/sql.scala src/Pure/General/ssh.scala src/Pure/General/symbol.scala src/Pure/General/time.scala src/Pure/General/timing.scala src/Pure/General/untyped.scala src/Pure/General/url.scala src/Pure/General/utf8.scala src/Pure/General/uuid.scala src/Pure/General/value.scala src/Pure/General/word.scala src/Pure/General/xz.scala src/Pure/Isar/document_structure.scala src/Pure/Isar/keyword.scala src/Pure/Isar/line_structure.scala src/Pure/Isar/outer_syntax.scala src/Pure/Isar/parse.scala src/Pure/Isar/token.scala src/Pure/ML/ml_console.scala src/Pure/ML/ml_lex.scala src/Pure/ML/ml_process.scala src/Pure/ML/ml_statistics.scala src/Pure/ML/ml_syntax.scala src/Pure/PIDE/byte_message.scala src/Pure/PIDE/command.scala src/Pure/PIDE/command_span.scala src/Pure/PIDE/document.scala src/Pure/PIDE/document_id.scala src/Pure/PIDE/document_status.scala src/Pure/PIDE/editor.scala src/Pure/PIDE/headless.scala src/Pure/PIDE/line.scala src/Pure/PIDE/markup.scala src/Pure/PIDE/markup_tree.scala src/Pure/PIDE/protocol.scala src/Pure/PIDE/protocol_handlers.scala src/Pure/PIDE/protocol_message.scala src/Pure/PIDE/prover.scala src/Pure/PIDE/query_operation.scala src/Pure/PIDE/rendering.scala src/Pure/PIDE/resources.scala src/Pure/PIDE/session.scala src/Pure/PIDE/text.scala src/Pure/PIDE/xml.scala src/Pure/PIDE/yxml.scala src/Pure/ROOT.scala src/Pure/System/bash.scala src/Pure/System/command_line.scala src/Pure/System/cygwin.scala src/Pure/System/distribution.scala src/Pure/System/getopts.scala src/Pure/System/isabelle_charset.scala src/Pure/System/isabelle_fonts.scala src/Pure/System/isabelle_platform.scala src/Pure/System/isabelle_process.scala src/Pure/System/isabelle_system.scala src/Pure/System/isabelle_tool.scala src/Pure/System/java_statistics.scala src/Pure/System/linux.scala + src/Pure/System/mingw.scala src/Pure/System/numa.scala src/Pure/System/options.scala src/Pure/System/platform.scala src/Pure/System/posix_interrupt.scala src/Pure/System/process_result.scala src/Pure/System/progress.scala src/Pure/System/scala.scala src/Pure/System/system_channel.scala src/Pure/System/tty_loop.scala src/Pure/Thy/bibtex.scala src/Pure/Thy/export.scala src/Pure/Thy/export_theory.scala src/Pure/Thy/file_format.scala src/Pure/Thy/html.scala src/Pure/Thy/latex.scala src/Pure/Thy/present.scala src/Pure/Thy/sessions.scala src/Pure/Thy/thy_element.scala src/Pure/Thy/thy_header.scala src/Pure/Thy/thy_syntax.scala src/Pure/Tools/build.scala src/Pure/Tools/build_docker.scala src/Pure/Tools/check_keywords.scala src/Pure/Tools/debugger.scala src/Pure/Tools/doc.scala src/Pure/Tools/dump.scala src/Pure/Tools/fontforge.scala src/Pure/Tools/main.scala src/Pure/Tools/mkroot.scala src/Pure/Tools/phabricator.scala src/Pure/Tools/print_operation.scala src/Pure/Tools/profiling_report.scala src/Pure/Tools/scala_project.scala src/Pure/Tools/server.scala src/Pure/Tools/server_commands.scala src/Pure/Tools/simplifier_trace.scala src/Pure/Tools/spell_checker.scala src/Pure/Tools/task_statistics.scala src/Pure/Tools/update.scala src/Pure/Tools/update_cartouches.scala src/Pure/Tools/update_comments.scala src/Pure/Tools/update_header.scala src/Pure/Tools/update_then.scala src/Pure/Tools/update_theorems.scala src/Pure/library.scala src/Pure/pure_thy.scala src/Pure/term.scala src/Pure/term_xml.scala src/Pure/thm_name.scala src/Tools/Graphview/graph_file.scala src/Tools/Graphview/graph_panel.scala src/Tools/Graphview/graphview.scala src/Tools/Graphview/layout.scala src/Tools/Graphview/main_panel.scala src/Tools/Graphview/metrics.scala src/Tools/Graphview/model.scala src/Tools/Graphview/mutator.scala src/Tools/Graphview/mutator_dialog.scala src/Tools/Graphview/mutator_event.scala src/Tools/Graphview/popups.scala src/Tools/Graphview/shapes.scala src/Tools/Graphview/tree_panel.scala src/Tools/VSCode/src/build_vscode.scala src/Tools/VSCode/src/channel.scala src/Tools/VSCode/src/document_model.scala src/Tools/VSCode/src/dynamic_output.scala src/Tools/VSCode/src/grammar.scala src/Tools/VSCode/src/preview_panel.scala src/Tools/VSCode/src/protocol.scala src/Tools/VSCode/src/server.scala src/Tools/VSCode/src/state_panel.scala src/Tools/VSCode/src/vscode_rendering.scala src/Tools/VSCode/src/vscode_resources.scala src/Tools/VSCode/src/vscode_spell_checker.scala ) ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS]" echo echo " Options are:" echo " -f fresh build" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" ## process command line # options FRESH="" while getopts "f" OPT do case "$OPT" in f) FRESH=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && usage ## target TARGET_DIR="lib/classes" TARGET_JAR="$TARGET_DIR/Pure.jar" TARGET_SHASUM="$TARGET_DIR/Pure.shasum" function target_shasum() { shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null } function target_clean() { rm -rf "$TARGET_DIR" } [ -n "$FRESH" ] && target_clean ## build target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null if [ "$?" -ne 0 ]; then echo "### Building Isabelle/Scala ..." target_clean BUILD_DIR="$TARGET_DIR/build" mkdir -p "$BUILD_DIR" ( export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \ -d "$BUILD_DIR" "${SOURCES[@]}" ) || fail "Failed to compile sources" CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE" cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/." cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/." isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \ -C "$BUILD_DIR" META-INF \ -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR" rm -rf "$BUILD_DIR" target_shasum > "$TARGET_SHASUM" fi