src/Pure/build-jars

added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);

#!/usr/bin/env bash
#
# Author: Makarius
#
# build-jars - build Isabelle/Scala
#
# Requires proper Isabelle settings environment.

## sources

declare -a SOURCES=(
  Admin/afp.scala
  Admin/build_cygwin.scala
  Admin/build_doc.scala
  Admin/build_fonts.scala
  Admin/build_history.scala
  Admin/build_jdk.scala
  Admin/build_log.scala
  Admin/build_polyml.scala
  Admin/build_release.scala
  Admin/build_status.scala
  Admin/check_sources.scala
  Admin/ci_profile.scala
  Admin/components.scala
  Admin/isabelle_cronjob.scala
  Admin/isabelle_devel.scala
  Admin/jenkins.scala
  Admin/other_isabelle.scala
  Concurrent/consumer_thread.scala
  Concurrent/counter.scala
  Concurrent/event_timer.scala
  Concurrent/future.scala
  Concurrent/mailbox.scala
  Concurrent/par_list.scala
  Concurrent/standard_thread.scala
  Concurrent/synchronized.scala
  GUI/color_value.scala
  GUI/gui.scala
  GUI/gui_thread.scala
  GUI/popup.scala
  GUI/wrap_panel.scala
  General/antiquote.scala
  General/bytes.scala
  General/cache.scala
  General/codepoint.scala
  General/comment.scala
  General/completion.scala
  General/csv.scala
  General/date.scala
  General/exn.scala
  General/file.scala
  General/file_watcher.scala
  General/graph.scala
  General/graph_display.scala
  General/graphics_file.scala
  General/http.scala
  General/json.scala
  General/linear_set.scala
  General/logger.scala
  General/long_name.scala
  General/mercurial.scala
  General/multi_map.scala
  General/output.scala
  General/path.scala
  General/position.scala
  General/pretty.scala
  General/properties.scala
  General/rdf.scala
  General/scan.scala
  General/sha1.scala
  General/sql.scala
  General/ssh.scala
  General/symbol.scala
  General/time.scala
  General/timing.scala
  General/untyped.scala
  General/url.scala
  General/utf8.scala
  General/uuid.scala
  General/value.scala
  General/word.scala
  General/xz.scala
  Isar/document_structure.scala
  Isar/keyword.scala
  Isar/line_structure.scala
  Isar/outer_syntax.scala
  Isar/parse.scala
  Isar/token.scala
  ML/ml_console.scala
  ML/ml_lex.scala
  ML/ml_process.scala
  ML/ml_statistics.scala
  ML/ml_syntax.scala
  PIDE/byte_message.scala
  PIDE/command.scala
  PIDE/command_span.scala
  PIDE/document.scala
  PIDE/document_id.scala
  PIDE/document_status.scala
  PIDE/editor.scala
  PIDE/headless.scala
  PIDE/line.scala
  PIDE/markup.scala
  PIDE/markup_tree.scala
  PIDE/protocol.scala
  PIDE/protocol_handlers.scala
  PIDE/protocol_message.scala
  PIDE/prover.scala
  PIDE/query_operation.scala
  PIDE/rendering.scala
  PIDE/resources.scala
  PIDE/session.scala
  PIDE/text.scala
  PIDE/xml.scala
  PIDE/yxml.scala
  ROOT.scala
  System/bash.scala
  System/command_line.scala
  System/cygwin.scala
  System/distribution.scala
  System/getopts.scala
  System/invoke_scala.scala
  System/isabelle_charset.scala
  System/isabelle_fonts.scala
  System/isabelle_process.scala
  System/isabelle_system.scala
  System/isabelle_tool.scala
  System/numa.scala
  System/options.scala
  System/platform.scala
  System/posix_interrupt.scala
  System/process_result.scala
  System/progress.scala
  System/system_channel.scala
  System/tty_loop.scala
  Thy/bibtex.scala
  Thy/export.scala
  Thy/export_theory.scala
  Thy/file_format.scala
  Thy/html.scala
  Thy/latex.scala
  Thy/present.scala
  Thy/sessions.scala
  Thy/thy_element.scala
  Thy/thy_header.scala
  Thy/thy_syntax.scala
  Tools/build.scala
  Tools/build_docker.scala
  Tools/check_keywords.scala
  Tools/debugger.scala
  Tools/doc.scala
  Tools/dump.scala
  Tools/fontforge.scala
  Tools/imports.scala
  Tools/main.scala
  Tools/mkroot.scala
  Tools/print_operation.scala
  Tools/profiling_report.scala
  Tools/server.scala
  Tools/server_commands.scala
  Tools/simplifier_trace.scala
  Tools/spell_checker.scala
  Tools/task_statistics.scala
  Tools/update.scala
  Tools/update_cartouches.scala
  Tools/update_comments.scala
  Tools/update_header.scala
  Tools/update_then.scala
  Tools/update_theorems.scala
  library.scala
  pure_thy.scala
  term.scala
  term_xml.scala
  thm_name.scala
  ../Tools/Graphview/graph_file.scala
  ../Tools/Graphview/graph_panel.scala
  ../Tools/Graphview/graphview.scala
  ../Tools/Graphview/layout.scala
  ../Tools/Graphview/main_panel.scala
  ../Tools/Graphview/metrics.scala
  ../Tools/Graphview/model.scala
  ../Tools/Graphview/mutator.scala
  ../Tools/Graphview/mutator_dialog.scala
  ../Tools/Graphview/mutator_event.scala
  ../Tools/Graphview/popups.scala
  ../Tools/Graphview/shapes.scala
  ../Tools/Graphview/tree_panel.scala
  ../Tools/VSCode/src/build_vscode.scala
  ../Tools/VSCode/src/channel.scala
  ../Tools/VSCode/src/document_model.scala
  ../Tools/VSCode/src/dynamic_output.scala
  ../Tools/VSCode/src/grammar.scala
  ../Tools/VSCode/src/preview_panel.scala
  ../Tools/VSCode/src/protocol.scala
  ../Tools/VSCode/src/server.scala
  ../Tools/VSCode/src/state_panel.scala
  ../Tools/VSCode/src/vscode_javascript.scala
  ../Tools/VSCode/src/vscode_rendering.scala
  ../Tools/VSCode/src/vscode_resources.scala
  ../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


## build

TARGET_DIR="$ISABELLE_HOME/lib/classes"
TARGET="$TARGET_DIR/Pure.jar"

declare -a UPDATED=()

if [ -n "$FRESH" ]; then
  OUTDATED=true
else
  OUTDATED=false
  if [ ! -e "$TARGET" ]; then
    OUTDATED=true
  else
    for DEP in "${SOURCES[@]}"
    do
      [ ! -e "$DEP" ] && fail "Missing file: $DEP"
      [ "$DEP" -nt "$TARGET" ] && {
        OUTDATED=true
        UPDATED["${#UPDATED[@]}"]="$DEP"
      }
    done
  fi
fi

if [ "$OUTDATED" = true ]
then
  echo "### Building Isabelle/Scala ..."

  [ "${#UPDATED[@]}" -gt 0 ] && {
    echo "Changed files:"
    for FILE in "${UPDATED[@]}"
    do
      echo "  $FILE"
    done
  }

  rm -f "$TARGET"
  rm -rf classes && mkdir classes

  SCALAC_OPTIONS="$ISABELLE_SCALAC_OPTIONS -d classes"

  (
    classpath classes
    export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"

    isabelle_scala scalac $SCALAC_OPTIONS "${SOURCES[@]}" || \
      fail "Failed to compile sources"
  ) || exit "$?"

  mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"

  pushd classes >/dev/null

  CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
  mkdir -p "$(dirname "$CHARSET_SERVICE")"
  echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"

  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/.
  cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/.

  isabelle_jdk jar cfe "$(platform_path "$TARGET")" isabelle.Main META-INF isabelle || \
    fail "Failed to produce $TARGET"

  popd >/dev/null

  rm -rf classes
fi