support session groups;
authorwenzelm
Thu Jul 26 12:27:47 2012 +0200 (2012-07-26)
changeset 485094854ced3e9d7
parent 48508 5a59e4c03957
child 48510 8f3069015441
support session groups;
tuned signature;
doc-src/ROOT
lib/Tools/build
src/HOL/ROOT
src/Pure/System/build.scala
     1.1 --- a/doc-src/ROOT	Thu Jul 26 11:52:08 2012 +0200
     1.2 +++ b/doc-src/ROOT	Thu Jul 26 12:27:47 2012 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4 -session Classes! in "Classes/Thy" = HOL +
     1.5 +session Classes! (doc) in "Classes/Thy" = HOL +
     1.6    options [browser_info = false, document = false, document_dump = document, document_dump_only]
     1.7    theories [document = false] Setup
     1.8    theories Classes
     1.9  
    1.10 -session Codegen! in "Codegen/Thy" = "HOL-Library" +
    1.11 +session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
    1.12    options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.13      print_mode = "no_brackets,iff"]
    1.14    theories [document = false] Setup
    1.15 @@ -16,11 +16,11 @@
    1.16      Adaptation
    1.17      Further
    1.18  
    1.19 -session Functions! in "Functions/Thy" = HOL +
    1.20 +session Functions! (doc) in "Functions/Thy" = HOL +
    1.21    options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.22    theories Functions
    1.23  
    1.24 -session IsarImplementation! in "IsarImplementation/Thy" = HOL +
    1.25 +session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
    1.26    options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.27    theories
    1.28      Eq
    1.29 @@ -34,7 +34,7 @@
    1.30      Syntax
    1.31      Tactic
    1.32  
    1.33 -session IsarRef in "IsarRef/Thy" = HOL +
    1.34 +session IsarRef (doc) in "IsarRef/Thy" = HOL +
    1.35    options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.36      quick_and_dirty]
    1.37    theories
    1.38 @@ -54,17 +54,17 @@
    1.39      Symbols
    1.40      ML_Tactic
    1.41  
    1.42 -session IsarRef in "IsarRef/Thy" = HOLCF +
    1.43 +session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
    1.44    options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.45      quick_and_dirty]
    1.46    theories HOLCF_Specific
    1.47  
    1.48 -session IsarRef in "IsarRef/Thy" = ZF +
    1.49 +session IsarRef (doc) in "IsarRef/Thy" = ZF +
    1.50    options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.51      quick_and_dirty]
    1.52    theories ZF_Specific
    1.53  
    1.54 -session LaTeXsugar! in "LaTeXsugar/Sugar" = HOL +
    1.55 +session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
    1.56    options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.57      threads = 1]  (* FIXME *)
    1.58    theories [document_dump = ""]
    1.59 @@ -72,18 +72,18 @@
    1.60      "~~/src/HOL/Library/OptionalSugar"
    1.61    theories Sugar
    1.62  
    1.63 -session Locales! in "Locales/Locales" = HOL +
    1.64 +session Locales! (doc) in "Locales/Locales" = HOL +
    1.65    options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.66    theories
    1.67      Examples1
    1.68      Examples2
    1.69      Examples3
    1.70  
    1.71 -session Main! in "Main/Docs" = HOL +
    1.72 +session Main! (doc) in "Main/Docs" = HOL +
    1.73    options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.74    theories Main_Doc
    1.75  
    1.76 -session ProgProve! in "ProgProve/Thys" = HOL +
    1.77 +session ProgProve! (doc) in "ProgProve/Thys" = HOL +
    1.78    options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.79      show_question_marks = false]
    1.80    theories
    1.81 @@ -94,7 +94,7 @@
    1.82      Logic
    1.83      Isar
    1.84  
    1.85 -session System! in "System/Thy" = Pure +
    1.86 +session System! (doc) in "System/Thy" = Pure +
    1.87    options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.88    theories
    1.89      Basics
    1.90 @@ -103,9 +103,9 @@
    1.91      Presentation
    1.92      Misc
    1.93  
    1.94 -(* session Tutorial in "Tutorial" = HOL + FIXME *)
    1.95 +(* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
    1.96  
    1.97 -session examples in "ZF" = ZF +
    1.98 +session examples (doc) in "ZF" = ZF +
    1.99    options [browser_info = false, document = false, document_dump = document, document_dump_only,
   1.100      print_mode = "brackets"]
   1.101    theories
     2.1 --- a/lib/Tools/build	Thu Jul 26 11:52:08 2012 +0200
     2.2 +++ b/lib/Tools/build	Thu Jul 26 12:27:47 2012 +0200
     2.3 @@ -28,7 +28,8 @@
     2.4    echo "  Options are:"
     2.5    echo "    -a           all sessions"
     2.6    echo "    -b           build target images"
     2.7 -  echo "    -d DIR       additional session directory with ROOT file"
     2.8 +  echo "    -d DIR       include session directory with ROOT file"
     2.9 +  echo "    -g NAME      include session group NAME"
    2.10    echo "    -j INT       maximum number of jobs (default 1)"
    2.11    echo "    -n           no build -- test dependencies only"
    2.12    echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
    2.13 @@ -58,16 +59,16 @@
    2.14  
    2.15  ALL_SESSIONS=false
    2.16  BUILD_IMAGES=false
    2.17 +declare -a MORE_DIRS=()
    2.18 +declare -a SESSION_GROUPS=()
    2.19  MAX_JOBS=1
    2.20  NO_BUILD=false
    2.21 +eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    2.22  SYSTEM_MODE=false
    2.23  TIMING=false
    2.24  VERBOSE=false
    2.25  
    2.26 -declare -a MORE_DIRS=()
    2.27 -eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    2.28 -
    2.29 -while getopts "abd:j:no:stv" OPT
    2.30 +while getopts "abd:g:j:no:stv" OPT
    2.31  do
    2.32    case "$OPT" in
    2.33      a)
    2.34 @@ -79,6 +80,9 @@
    2.35      d)
    2.36        MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
    2.37        ;;
    2.38 +    g)
    2.39 +      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
    2.40 +      ;;
    2.41      j)
    2.42        check_number "$OPTARG"
    2.43        MAX_JOBS="$OPTARG"
    2.44 @@ -122,8 +126,8 @@
    2.45  fi
    2.46  
    2.47  "$ISABELLE_TOOL" java isabelle.Build \
    2.48 -  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \
    2.49 -  "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    2.50 +  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
    2.51 +  "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    2.52  RC="$?"
    2.53  
    2.54  if [ "$NO_BUILD" = false ]; then
     3.1 --- a/src/HOL/ROOT	Thu Jul 26 11:52:08 2012 +0200
     3.2 +++ b/src/HOL/ROOT	Thu Jul 26 12:27:47 2012 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -session HOL! in "." = Pure +
     3.5 +session HOL! (main) in "." = Pure +
     3.6    description {* Classical Higher-order Logic *}
     3.7    options [document_graph]
     3.8    theories Complex_Main
     3.9 @@ -19,8 +19,8 @@
    3.10    options [document = false]
    3.11    theories Main
    3.12  
    3.13 -session "HOL-Proofs"! in "." = Pure +
    3.14 -  description {* HOL-Main with proof terms *}
    3.15 +session "HOL-Proofs"! (main) in "." = Pure +
    3.16 +  description {* HOL-Main with explicit proof terms *}
    3.17    options [document = false, proofs = 2, parallel_proofs = 0]
    3.18    theories Main
    3.19  
    3.20 @@ -571,7 +571,7 @@
    3.21      "ex/Koepf_Duermuth_Countermeasure"
    3.22    files "document/root.tex"
    3.23  
    3.24 -session Nominal = HOL +
    3.25 +session Nominal (main) = HOL +
    3.26    options [document = false]
    3.27    theories Nominal
    3.28  
    3.29 @@ -760,7 +760,7 @@
    3.30      Predicate_Compile_Tests
    3.31      Specialisation_Examples
    3.32  
    3.33 -session HOLCF! = HOL +
    3.34 +session HOLCF! (main) = HOL +
    3.35    description {*
    3.36      Author:     Franz Regensburger
    3.37      Author:     Brian Huffman
     4.1 --- a/src/Pure/System/build.scala	Thu Jul 26 11:52:08 2012 +0200
     4.2 +++ b/src/Pure/System/build.scala	Thu Jul 26 12:27:47 2012 +0200
     4.3 @@ -25,6 +25,7 @@
     4.4  
     4.5      sealed case class Info(
     4.6        base_name: String,
     4.7 +      groups: List[String],
     4.8        dir: Path,
     4.9        parent: Option[String],
    4.10        parent_base_name: Option[String],
    4.11 @@ -65,8 +66,15 @@
    4.12  
    4.13        def - (name: String): Queue = new Queue(graph.del_node(name))
    4.14  
    4.15 -      def required(names: List[String]): Queue =
    4.16 -        new Queue(graph.restrict(graph.all_preds(names).toSet))
    4.17 +      def required(groups: List[String], names: List[String]): Queue =
    4.18 +      {
    4.19 +        val selected_group = groups.toSet
    4.20 +        val selected_name = names.toSet
    4.21 +        val selected =
    4.22 +          graph.keys.filter(name =>
    4.23 +            selected_name(name) || apply(name).groups.exists(selected_group)).toList
    4.24 +        new Queue(graph.restrict(graph.all_preds(selected).toSet))
    4.25 +      }
    4.26  
    4.27        def dequeue(skip: String => Boolean): Option[(String, Info)] =
    4.28        {
    4.29 @@ -87,6 +95,7 @@
    4.30    private case class Session_Entry(
    4.31      name: String,
    4.32      this_name: Boolean,
    4.33 +    groups: List[String],
    4.34      path: Option[String],
    4.35      parent: Option[String],
    4.36      description: String,
    4.37 @@ -121,13 +130,14 @@
    4.38  
    4.39        ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
    4.40          (keyword("!") ^^^ true | success(false)) ~
    4.41 +        (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
    4.42          (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
    4.43          (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
    4.44          (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
    4.45          (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
    4.46          rep(theories) ~
    4.47          (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
    4.48 -          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
    4.49 +          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
    4.50      }
    4.51  
    4.52      def parse_entries(root: JFile): List[Session_Entry] =
    4.53 @@ -186,7 +196,7 @@
    4.54          val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    4.55  
    4.56          val info =
    4.57 -          Session.Info(entry.name, dir + path, entry.parent, parent_base_name,
    4.58 +          Session.Info(entry.name, entry.groups, dir + path, entry.parent, parent_base_name,
    4.59              entry.description, session_options, theories, files, digest)
    4.60  
    4.61          queue1 + (full_name, info)
    4.62 @@ -224,8 +234,8 @@
    4.63        })
    4.64    }
    4.65  
    4.66 -  def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
    4.67 -    more_dirs: List[Path]): Session.Queue =
    4.68 +  def find_sessions(options: Options, more_dirs: List[Path],
    4.69 +    all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
    4.70    {
    4.71      var queue = Session.Queue.empty
    4.72  
    4.73 @@ -244,7 +254,7 @@
    4.74        case bad => error("Undefined session(s): " + commas_quote(bad))
    4.75      }
    4.76  
    4.77 -    if (all_sessions) queue else queue.required(sessions)
    4.78 +    if (all_sessions) queue else queue.required(session_groups, sessions)
    4.79    }
    4.80  
    4.81  
    4.82 @@ -419,12 +429,21 @@
    4.83  
    4.84    /* build */
    4.85  
    4.86 -  def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
    4.87 -    no_build: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean,
    4.88 -    more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
    4.89 +  def build(
    4.90 +    all_sessions: Boolean = false,
    4.91 +    build_images: Boolean = false,
    4.92 +    more_dirs: List[Path] = Nil,
    4.93 +    session_groups: List[String] = Nil,
    4.94 +    max_jobs: Int = 1,
    4.95 +    no_build: Boolean = false,
    4.96 +    build_options: List[String] = Nil,
    4.97 +    system_mode: Boolean = false,
    4.98 +    timing: Boolean = false,
    4.99 +    verbose: Boolean = false,
   4.100 +    sessions: List[String] = Nil): Int =
   4.101    {
   4.102 -    val options = (Options.init() /: more_options)(_.define_simple(_))
   4.103 -    val queue = find_sessions(options, all_sessions, sessions, more_dirs)
   4.104 +    val options = (Options.init() /: build_options)(_.define_simple(_))
   4.105 +    val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
   4.106      val deps = dependencies(verbose, queue)
   4.107  
   4.108      def make_stamp(name: String): String =
   4.109 @@ -534,9 +553,9 @@
   4.110            Properties.Value.Boolean(system_mode) ::
   4.111            Properties.Value.Boolean(timing) ::
   4.112            Properties.Value.Boolean(verbose) ::
   4.113 -          Command_Line.Chunks(more_dirs, options, sessions) =>
   4.114 -            build(all_sessions, build_images, max_jobs, no_build, system_mode, timing,
   4.115 -              verbose, more_dirs.map(Path.explode), options, sessions)
   4.116 +          Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
   4.117 +            build(all_sessions, build_images, more_dirs.map(Path.explode), session_groups,
   4.118 +              max_jobs, no_build, build_options, system_mode, timing, verbose, sessions)
   4.119          case _ => error("Bad arguments:\n" + cat_lines(args))
   4.120        }
   4.121      }