upgrade "isabelle build" to Isabelle/Scala;
authorwenzelm
Thu Mar 10 22:09:44 2016 +0100 (2016-03-10)
changeset 625900c837beeb5e7
parent 62589 b5783412bfed
child 62591 98122e719d19
upgrade "isabelle build" to Isabelle/Scala;
lib/Tools/build
src/Pure/Tools/build.scala
src/Pure/library.scala
     1.1 --- a/lib/Tools/build	Thu Mar 10 17:30:04 2016 +0100
     1.2 +++ b/lib/Tools/build	Thu Mar 10 22:09:44 2016 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4  #
     1.5  # DESCRIPTION: build and manage Isabelle sessions
     1.6  
     1.7 -## settings
     1.8 +isabelle_admin_build jars || exit $?
     1.9  
    1.10  case "$ISABELLE_JAVA_PLATFORM" in
    1.11    x86-*)
    1.12 @@ -15,174 +15,6 @@
    1.13      ;;
    1.14  esac
    1.15  
    1.16 -
    1.17 -## diagnostics
    1.18 -
    1.19 -PRG="$(basename "$0")"
    1.20 -
    1.21 -function show_settings()
    1.22 -{
    1.23 -  local PREFIX="$1"
    1.24 -  echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
    1.25 -  echo
    1.26 -  echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_OPTIONS\""
    1.27 -  echo
    1.28 -  echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
    1.29 -  echo "${PREFIX}ML_HOME=\"$ML_HOME\""
    1.30 -  echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
    1.31 -  echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
    1.32 -}
    1.33 -
    1.34 -function usage()
    1.35 -{
    1.36 -  echo
    1.37 -  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
    1.38 -  echo
    1.39 -  echo "  Options are:"
    1.40 -  echo "    -D DIR       include session directory and select its sessions"
    1.41 -  echo "    -R           operate on requirements of selected sessions"
    1.42 -  echo "    -X NAME      exclude sessions from group NAME and all descendants"
    1.43 -  echo "    -a           select all sessions"
    1.44 -  echo "    -b           build heap images"
    1.45 -  echo "    -c           clean build"
    1.46 -  echo "    -d DIR       include session directory"
    1.47 -  echo "    -g NAME      select session group NAME"
    1.48 -  echo "    -j INT       maximum number of parallel jobs (default 1)"
    1.49 -  echo "    -k KEYWORD   check theory sources for conflicts with proposed keywords"
    1.50 -  echo "    -l           list session source files"
    1.51 -  echo "    -n           no build -- test dependencies only"
    1.52 -  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    1.53 -  echo "    -s           system build mode: produce output in ISABELLE_HOME"
    1.54 -  echo "    -v           verbose"
    1.55 -  echo "    -x NAME      exclude session NAME and all descendants"
    1.56 -  echo
    1.57 -  echo "  Build and manage Isabelle sessions, depending on implicit"
    1.58 -  show_settings "  "
    1.59 -  echo
    1.60 -  exit 1
    1.61 -}
    1.62 -
    1.63 -function fail()
    1.64 -{
    1.65 -  echo "$1" >&2
    1.66 -  exit 2
    1.67 -}
    1.68 -
    1.69 -function check_number()
    1.70 -{
    1.71 -  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    1.72 -}
    1.73 -
    1.74 -
    1.75 -## process command line
    1.76 -
    1.77 -declare -a SELECT_DIRS=()
    1.78 -REQUIREMENTS=false
    1.79 -declare -a EXCLUDE_SESSION_GROUPS=()
    1.80 -ALL_SESSIONS=false
    1.81 -BUILD_HEAP=false
    1.82 -CLEAN_BUILD=false
    1.83 -declare -a INCLUDE_DIRS=()
    1.84 -declare -a SESSION_GROUPS=()
    1.85 -MAX_JOBS=1
    1.86 -declare -a CHECK_KEYWORDS=()
    1.87 -LIST_FILES=false
    1.88 -NO_BUILD=false
    1.89 -eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    1.90 -SYSTEM_MODE=false
    1.91 -VERBOSE=false
    1.92 -declare -a EXCLUDE_SESSIONS=()
    1.93 +eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
    1.94  
    1.95 -while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
    1.96 -do
    1.97 -  case "$OPT" in
    1.98 -    D)
    1.99 -      SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
   1.100 -      ;;
   1.101 -    R)
   1.102 -      REQUIREMENTS="true"
   1.103 -      ;;
   1.104 -    X)
   1.105 -      EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
   1.106 -      ;;
   1.107 -    a)
   1.108 -      ALL_SESSIONS="true"
   1.109 -      ;;
   1.110 -    b)
   1.111 -      BUILD_HEAP="true"
   1.112 -      ;;
   1.113 -    c)
   1.114 -      CLEAN_BUILD="true"
   1.115 -      ;;
   1.116 -    d)
   1.117 -      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
   1.118 -      ;;
   1.119 -    g)
   1.120 -      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
   1.121 -      ;;
   1.122 -    j)
   1.123 -      check_number "$OPTARG"
   1.124 -      MAX_JOBS="$OPTARG"
   1.125 -      ;;
   1.126 -    k)
   1.127 -      CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
   1.128 -      ;;
   1.129 -    l)
   1.130 -      LIST_FILES="true"
   1.131 -      ;;
   1.132 -    n)
   1.133 -      NO_BUILD="true"
   1.134 -      ;;
   1.135 -    o)
   1.136 -      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
   1.137 -      ;;
   1.138 -    s)
   1.139 -      SYSTEM_MODE="true"
   1.140 -      ;;
   1.141 -    v)
   1.142 -      VERBOSE="true"
   1.143 -      ;;
   1.144 -    x)
   1.145 -      EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
   1.146 -      ;;
   1.147 -    \?)
   1.148 -      usage
   1.149 -      ;;
   1.150 -  esac
   1.151 -done
   1.152 -
   1.153 -shift $(($OPTIND - 1))
   1.154 -
   1.155 -
   1.156 -## main
   1.157 -
   1.158 -isabelle_admin_build jars || exit $?
   1.159 -
   1.160 -if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   1.161 -  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   1.162 -
   1.163 -  show_settings ""
   1.164 -  echo
   1.165 -fi
   1.166 -
   1.167 -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
   1.168 -
   1.169 -. "$ISABELLE_HOME/lib/scripts/timestart.bash"
   1.170 -
   1.171 -isabelle java "${JAVA_ARGS[@]}" isabelle.Build \
   1.172 -  "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   1.173 -  "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   1.174 -  "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
   1.175 -  "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
   1.176 -  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
   1.177 -  "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
   1.178 -RC="$?"
   1.179 -
   1.180 -if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   1.181 -  echo -n "Finished at "; date
   1.182 -fi
   1.183 -
   1.184 -. "$ISABELLE_HOME/lib/scripts/timestop.bash"
   1.185 -echo "$TIMES_REPORT"
   1.186 -
   1.187 -exit "$RC"
   1.188 +exec isabelle java "${JAVA_ARGS[@]}" isabelle.Build "$@"
     2.1 --- a/src/Pure/Tools/build.scala	Thu Mar 10 17:30:04 2016 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Thu Mar 10 22:09:44 2016 +0100
     2.3 @@ -1027,29 +1027,113 @@
     2.4    def main(args: Array[String])
     2.5    {
     2.6      Command_Line.tool {
     2.7 -      args.toList match {
     2.8 -        case
     2.9 -          Properties.Value.Boolean(requirements) ::
    2.10 -          Properties.Value.Boolean(all_sessions) ::
    2.11 -          Properties.Value.Boolean(build_heap) ::
    2.12 -          Properties.Value.Boolean(clean_build) ::
    2.13 -          Properties.Value.Int(max_jobs) ::
    2.14 -          Properties.Value.Boolean(list_files) ::
    2.15 -          Properties.Value.Boolean(no_build) ::
    2.16 -          Properties.Value.Boolean(system_mode) ::
    2.17 -          Properties.Value.Boolean(verbose) ::
    2.18 -          Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
    2.19 -              build_options, exclude_session_groups, exclude_sessions, sessions) =>
    2.20 -            val options = (Options.init() /: build_options)(_ + _)
    2.21 -            val progress = new Console_Progress(verbose)
    2.22 -            progress.interrupt_handler {
    2.23 -              build(options, progress, requirements, all_sessions, build_heap, clean_build,
    2.24 -                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), exclude_session_groups,
    2.25 -                session_groups, max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
    2.26 -                verbose, exclude_sessions, sessions)
    2.27 -            }
    2.28 -        case _ => error("Bad arguments:\n" + cat_lines(args))
    2.29 +      def show_settings(): String =
    2.30 +        cat_lines(List(
    2.31 +          "ISABELLE_BUILD_OPTIONS=" +
    2.32 +            quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
    2.33 +          "",
    2.34 +          "ISABELLE_BUILD_JAVA_OPTIONS=" +
    2.35 +            quote(Isabelle_System.getenv("ISABELLE_BUILD_JAVA_OPTIONS")) +
    2.36 +          "",
    2.37 +          "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
    2.38 +          "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
    2.39 +          "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
    2.40 +          "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
    2.41 +
    2.42 +      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
    2.43 +
    2.44 +      var select_dirs: List[Path] = Nil
    2.45 +      var requirements = false
    2.46 +      var exclude_session_groups: List[String] = Nil
    2.47 +      var all_sessions = false
    2.48 +      var build_heap = false
    2.49 +      var clean_build = false
    2.50 +      var dirs: List[Path] = Nil
    2.51 +      var session_groups: List[String] = Nil
    2.52 +      var max_jobs = 1
    2.53 +      var check_keywords: Set[String] = Set.empty
    2.54 +      var list_files = false
    2.55 +      var no_build = false
    2.56 +      var options = (Options.init() /: build_options)(_ + _)
    2.57 +      var system_mode = false
    2.58 +      var verbose = false
    2.59 +      var exclude_sessions: List[String] = Nil
    2.60 +
    2.61 +      val getopts = Getopts("""
    2.62 +Usage: isabelle build [OPTIONS] [SESSIONS ...]
    2.63 +
    2.64 +  Options are:
    2.65 +    -D DIR       include session directory and select its sessions
    2.66 +    -R           operate on requirements of selected sessions
    2.67 +    -X NAME      exclude sessions from group NAME and all descendants
    2.68 +    -a           select all sessions
    2.69 +    -b           build heap images
    2.70 +    -c           clean build
    2.71 +    -d DIR       include session directory
    2.72 +    -g NAME      select session group NAME
    2.73 +    -j INT       maximum number of parallel jobs (default 1)
    2.74 +    -k KEYWORD   check theory sources for conflicts with proposed keywords
    2.75 +    -l           list session source files
    2.76 +    -n           no build -- test dependencies only
    2.77 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.78 +    -s           system build mode: produce output in ISABELLE_HOME
    2.79 +    -v           verbose
    2.80 +    -x NAME      exclude session NAME and all descendants
    2.81 +
    2.82 +  Build and manage Isabelle sessions, depending on implicit
    2.83 +""" + Library.prefix_lines("  ", show_settings()),
    2.84 +        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    2.85 +        "R" -> (_ => requirements = true),
    2.86 +        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    2.87 +        "a" -> (_ => all_sessions = true),
    2.88 +        "b" -> (_ => build_heap = true),
    2.89 +        "c" -> (_ => clean_build = true),
    2.90 +        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    2.91 +        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    2.92 +        "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
    2.93 +        "k:" -> (arg => check_keywords = check_keywords + arg),
    2.94 +        "l" -> (_ => list_files = true),
    2.95 +        "n" -> (_ => no_build = true),
    2.96 +        "o:" -> (arg => options = options + arg),
    2.97 +        "s" -> (_ => system_mode = true),
    2.98 +        "v" -> (_ => verbose = true),
    2.99 +        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   2.100 +
   2.101 +      val sessions = getopts(args)
   2.102 +
   2.103 +      val progress = new Console_Progress(verbose)
   2.104 +      val start_time = Time.now()
   2.105 +      val show_timing = !no_build && verbose
   2.106 +
   2.107 +      if (show_timing) {
   2.108 +        progress.echo(
   2.109 +          Library.trim_line(
   2.110 +            Isabelle_System.bash(
   2.111 +              """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out))
   2.112 +        progress.echo(show_settings())
   2.113        }
   2.114 +
   2.115 +      val results =
   2.116 +        progress.interrupt_handler {
   2.117 +          build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
   2.118 +            dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
   2.119 +            check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
   2.120 +        }
   2.121 +
   2.122 +      if (show_timing) {
   2.123 +        val elapsed_time = Time.now() - start_time
   2.124 +
   2.125 +        progress.echo(
   2.126 +          Library.trim_line(
   2.127 +            Isabelle_System.bash("""echo "Finished at "; date""").out))
   2.128 +
   2.129 +        val total_timing =
   2.130 +          (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   2.131 +            copy(elapsed = elapsed_time)
   2.132 +        progress.echo(total_timing.message_resources)
   2.133 +      }
   2.134 +
   2.135 +      results.rc
   2.136      }
   2.137    }
   2.138  
     3.1 --- a/src/Pure/library.scala	Thu Mar 10 17:30:04 2016 +0100
     3.2 +++ b/src/Pure/library.scala	Thu Mar 10 22:09:44 2016 +0100
     3.3 @@ -97,6 +97,10 @@
     3.4  
     3.5    def split_lines(str: String): List[String] = space_explode('\n', str)
     3.6  
     3.7 +  def prefix_lines(prfx: String, str: String): String =
     3.8 +    if (str == "") str
     3.9 +    else cat_lines(split_lines(str).map(s => prfx + s))
    3.10 +
    3.11    def first_line(source: CharSequence): String =
    3.12    {
    3.13      val lines = separated_chunks(_ == '\n', source)