Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: TestQuotedLogOutputs.java Sprache: PVS

Original von: Isabelle^©

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

## sources

declare -a SOURCES=(
  src/HOL/SPARK/Tools/spark.scala
  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/build_vampire.scala
  src/Pure/Admin/build_verit.scala
  src/Pure/Admin/build_zipperposition.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/desktop_app.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/mailman.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/executable.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/presentation.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/build_job.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/java_monitor.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/dynamic_output.scala
  src/Tools/VSCode/src/language_server.scala
  src/Tools/VSCode/src/lsp.scala
  src/Tools/VSCode/src/preview_panel.scala
  src/Tools/VSCode/src/state_panel.scala
  src/Tools/VSCode/src/textmate_grammar.scala
  src/Tools/VSCode/src/vscode_model.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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.