pass build options to ML;
authorwenzelm
Tue Jul 24 00:29:36 2012 +0200 (2012-07-24)
changeset 48457fd9e28d5a143
parent 48456 d8ff14f44a40
child 48458 09710d6fc3d1
pass build options to ML;
some imitation of usedir Session.init;
etc/options
src/Pure/General/path.scala
src/Pure/System/build.ML
src/Pure/System/build.scala
src/Pure/System/options.scala
src/Pure/System/session.ML
     1.1 --- a/etc/options	Mon Jul 23 22:35:10 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 00:29:36 2012 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  declare document_format : string = pdf
     1.5  declare document_variants : string = document
     1.6  declare document_graph : bool = false
     1.7 +declare document_dump : string = ""
     1.8  
     1.9  declare threads_limit : int = 1
    1.10  declare threads_trace : int = 0
    1.11 @@ -18,7 +19,6 @@
    1.12  declare quick_and_dirty : bool = false
    1.13  
    1.14  declare timing : bool = false
    1.15 -declare verbose : bool = false
    1.16  
    1.17  declare condition : string = ""
    1.18  
     2.1 --- a/src/Pure/General/path.scala	Mon Jul 23 22:35:10 2012 +0200
     2.2 +++ b/src/Pure/General/path.scala	Tue Jul 24 00:29:36 2012 +0200
     2.3 @@ -98,6 +98,11 @@
     2.4  
     2.5    def split(str: String): List[Path] =
     2.6      space_explode(':', str).filterNot(_.isEmpty).map(explode)
     2.7 +
     2.8 +
     2.9 +  /* encode */
    2.10 +
    2.11 +  val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
    2.12  }
    2.13  
    2.14  
     3.1 --- a/src/Pure/System/build.ML	Mon Jul 23 22:35:10 2012 +0200
     3.2 +++ b/src/Pure/System/build.ML	Tue Jul 24 00:29:36 2012 +0200
     3.3 @@ -12,14 +12,43 @@
     3.4  structure Build: BUILD =
     3.5  struct
     3.6  
     3.7 +fun use_theories name options =
     3.8 +  Thy_Info.use_thys
     3.9 +    |> Session.with_timing name (Options.bool options "timing")
    3.10 +    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    3.11 +    |> Unsynchronized.setmp print_mode
    3.12 +        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    3.13 +    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    3.14 +    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    3.15 +        (Options.int options "parallel_proofs_threshold")
    3.16 +    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    3.17 +    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit");
    3.18 +
    3.19  fun build args_file =
    3.20    let
    3.21 -    val (save, (parent, (name, theories))) =
    3.22 +    val (save, (options, (verbose, (browser_info, (parent, (name, (base_name, theories))))))) =
    3.23        File.read (Path.explode args_file) |> YXML.parse_body |>
    3.24 -        let open XML.Decode in pair bool (pair string (pair string (list string))) end;
    3.25 +        let open XML.Decode in
    3.26 +          pair bool (pair Options.decode (pair bool (pair string (pair string
    3.27 +            (pair string (pair string ((list (pair Options.decode (list string))))))))))
    3.28 +        end;
    3.29  
    3.30 -    val _ = Session.init false parent name;  (* FIXME reset!? *)
    3.31 -    val _ = Thy_Info.use_thys theories;
    3.32 +    val _ =
    3.33 +      Session.init
    3.34 +        save
    3.35 +        false (* FIXME reset!? *)
    3.36 +        (Options.bool options "browser_info") browser_info
    3.37 +        (Options.string options "document_format")   (* FIXME dependent on "document" (!?) *)
    3.38 +        (Options.bool options "document_graph")
    3.39 +        (space_explode "," (Options.string options "document_variants"))
    3.40 +        parent
    3.41 +        base_name
    3.42 +        (true (* FIXME copy document/ files on Scala side!? *),
    3.43 +          Options.string options "document_dump")
    3.44 +        ""
    3.45 +        verbose;
    3.46 +
    3.47 +    val _ = List.app (uncurry (use_theories name)) theories;
    3.48      val _ = Session.finish ();
    3.49  
    3.50      val _ = if save then () else quit ();
     4.1 --- a/src/Pure/System/build.scala	Mon Jul 23 22:35:10 2012 +0200
     4.2 +++ b/src/Pure/System/build.scala	Tue Jul 24 00:29:36 2012 +0200
     4.3 @@ -42,6 +42,7 @@
     4.4      /* Info */
     4.5  
     4.6      sealed case class Info(
     4.7 +      base_name: String,
     4.8        dir: Path,
     4.9        parent: Option[String],
    4.10        description: String,
    4.11 @@ -214,7 +215,7 @@
    4.12          val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    4.13  
    4.14          val info =
    4.15 -          Session.Info(dir + path, entry.parent,
    4.16 +          Session.Info(entry.name, dir + path, entry.parent,
    4.17              entry.description, options ++ entry.options, theories, files, digest)
    4.18  
    4.19          queue1 + (key, info)
    4.20 @@ -340,7 +341,8 @@
    4.21      def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
    4.22    }
    4.23  
    4.24 -  private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
    4.25 +  private def start_job(name: String, info: Session.Info, output: Option[String],
    4.26 +    options: Options, verbose: Boolean, browser_info: Path): Job =
    4.27    {
    4.28      val parent = info.parent.getOrElse("")
    4.29  
    4.30 @@ -371,8 +373,10 @@
    4.31      val args_xml =
    4.32      {
    4.33        import XML.Encode._
    4.34 -      pair(bool, pair(string, pair(string, list(string))))(
    4.35 -        output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
    4.36 +          pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
    4.37 +            pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
    4.38 +          (output.isDefined, (options, (verbose, (browser_info, (parent,
    4.39 +            (name, (info.base_name, info.theories))))))))
    4.40      }
    4.41      new Job(cwd, env, script, YXML.string_of_body(args_xml))
    4.42    }
    4.43 @@ -454,7 +458,7 @@
    4.44                    Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
    4.45                  else None
    4.46                echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
    4.47 -              val job = start_job(name, info, output)
    4.48 +              val job = start_job(name, info, output, options, verbose, browser_info)
    4.49                loop(pending, running + (name -> job), results)
    4.50              }
    4.51              else {
     5.1 --- a/src/Pure/System/options.scala	Mon Jul 23 22:35:10 2012 +0200
     5.2 +++ b/src/Pure/System/options.scala	Tue Jul 24 00:29:36 2012 +0200
     5.3 @@ -79,6 +79,11 @@
     5.4      }
     5.5      options
     5.6    }
     5.7 +
     5.8 +
     5.9 +  /* encode */
    5.10 +
    5.11 +  val encode: XML.Encode.T[Options] = (options => options.encode)
    5.12  }
    5.13  
    5.14  
     6.1 --- a/src/Pure/System/session.ML	Mon Jul 23 22:35:10 2012 +0200
     6.2 +++ b/src/Pure/System/session.ML	Tue Jul 24 00:29:36 2012 +0200
     6.3 @@ -9,11 +9,13 @@
     6.4    val id: unit -> string list
     6.5    val name: unit -> string
     6.6    val welcome: unit -> string
     6.7 -  val init: bool -> string -> string -> unit
     6.8 +  val finish: unit -> unit
     6.9 +  val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
    6.10 +    string -> string -> bool * string -> string -> bool -> unit
    6.11 +  val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    6.12    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    6.13      string -> bool -> string list -> string -> string -> bool * string ->
    6.14      string -> int -> bool -> bool -> int -> int -> int -> int -> unit
    6.15 -  val finish: unit -> unit
    6.16  end;
    6.17  
    6.18  structure Session: SESSION =
    6.19 @@ -63,9 +65,9 @@
    6.20    end;
    6.21  
    6.22  
    6.23 -(* init *)
    6.24 +(* init_name *)
    6.25  
    6.26 -fun init reset parent name =
    6.27 +fun init_name reset parent name =
    6.28    if not (member (op =) (! session) parent) orelse not (! session_finished) then
    6.29      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    6.30    else (add_path reset name; session_finished := false);
    6.31 @@ -94,26 +96,31 @@
    6.32  fun dumping (_, "") = NONE
    6.33    | dumping (cp, path) = SOME (cp, Path.explode path);
    6.34  
    6.35 +fun with_timing _ false f x = f x
    6.36 +  | with_timing item true f x =
    6.37 +      let
    6.38 +        val start = Timing.start ();
    6.39 +        val y = f x;
    6.40 +        val timing = Timing.result start;
    6.41 +        val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    6.42 +          |> Real.fmt (StringCvt.FIX (SOME 2));
    6.43 +        val _ =
    6.44 +          Output.physical_stderr ("Timing " ^ item ^ " (" ^
    6.45 +            string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
    6.46 +            Timing.message timing ^ ", factor " ^ factor ^ ")\n");
    6.47 +      in y end;
    6.48 +
    6.49 +fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose =
    6.50 + (init_name reset parent name;
    6.51 +  Present.init build info info_path doc doc_graph doc_variants (path ()) name
    6.52 +    (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ())));
    6.53 +
    6.54  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
    6.55      name dump rpath level timing verbose max_threads trace_threads
    6.56      parallel_proofs parallel_proofs_threshold =
    6.57    ((fn () =>
    6.58 -     (init reset parent name;
    6.59 -      Present.init build info info_path doc doc_graph doc_variants (path ()) name
    6.60 -        (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
    6.61 -      if timing then
    6.62 -        let
    6.63 -          val start = Timing.start ();
    6.64 -          val _ = use root;
    6.65 -          val timing = Timing.result start;
    6.66 -          val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    6.67 -            |> Real.fmt (StringCvt.FIX (SOME 2));
    6.68 -          val _ =
    6.69 -            Output.physical_stderr ("Timing " ^ item ^ " (" ^
    6.70 -              string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
    6.71 -              Timing.message timing ^ ", factor " ^ factor ^ ")\n");
    6.72 -        in () end
    6.73 -      else use root;
    6.74 +     (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose;
    6.75 +      with_timing item timing use root;
    6.76        finish ()))
    6.77      |> Unsynchronized.setmp Proofterm.proofs level
    6.78      |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())