--- a/etc/options Mon Jul 23 22:35:10 2012 +0200
+++ b/etc/options Tue Jul 24 00:29:36 2012 +0200
@@ -6,6 +6,7 @@
declare document_format : string = pdf
declare document_variants : string = document
declare document_graph : bool = false
+declare document_dump : string = ""
declare threads_limit : int = 1
declare threads_trace : int = 0
@@ -18,7 +19,6 @@
declare quick_and_dirty : bool = false
declare timing : bool = false
-declare verbose : bool = false
declare condition : string = ""
--- a/src/Pure/General/path.scala Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/General/path.scala Tue Jul 24 00:29:36 2012 +0200
@@ -98,6 +98,11 @@
def split(str: String): List[Path] =
space_explode(':', str).filterNot(_.isEmpty).map(explode)
+
+
+ /* encode */
+
+ val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
}
--- a/src/Pure/System/build.ML Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/build.ML Tue Jul 24 00:29:36 2012 +0200
@@ -12,14 +12,43 @@
structure Build: BUILD =
struct
+fun use_theories name options =
+ Thy_Info.use_thys
+ |> Session.with_timing name (Options.bool options "timing")
+ |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
+ |> Unsynchronized.setmp print_mode
+ (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+ |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+ |> Unsynchronized.setmp Goal.parallel_proofs_threshold
+ (Options.int options "parallel_proofs_threshold")
+ |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+ |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads_limit");
+
fun build args_file =
let
- val (save, (parent, (name, theories))) =
+ val (save, (options, (verbose, (browser_info, (parent, (name, (base_name, theories))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
- let open XML.Decode in pair bool (pair string (pair string (list string))) end;
+ let open XML.Decode in
+ pair bool (pair Options.decode (pair bool (pair string (pair string
+ (pair string (pair string ((list (pair Options.decode (list string))))))))))
+ end;
- val _ = Session.init false parent name; (* FIXME reset!? *)
- val _ = Thy_Info.use_thys theories;
+ val _ =
+ Session.init
+ save
+ false (* FIXME reset!? *)
+ (Options.bool options "browser_info") browser_info
+ (Options.string options "document_format") (* FIXME dependent on "document" (!?) *)
+ (Options.bool options "document_graph")
+ (space_explode "," (Options.string options "document_variants"))
+ parent
+ base_name
+ (true (* FIXME copy document/ files on Scala side!? *),
+ Options.string options "document_dump")
+ ""
+ verbose;
+
+ val _ = List.app (uncurry (use_theories name)) theories;
val _ = Session.finish ();
val _ = if save then () else quit ();
--- a/src/Pure/System/build.scala Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/build.scala Tue Jul 24 00:29:36 2012 +0200
@@ -42,6 +42,7 @@
/* Info */
sealed case class Info(
+ base_name: String,
dir: Path,
parent: Option[String],
description: String,
@@ -214,7 +215,7 @@
val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
val info =
- Session.Info(dir + path, entry.parent,
+ Session.Info(entry.name, dir + path, entry.parent,
entry.description, options ++ entry.options, theories, files, digest)
queue1 + (key, info)
@@ -340,7 +341,8 @@
def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
}
- private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
+ private def start_job(name: String, info: Session.Info, output: Option[String],
+ options: Options, verbose: Boolean, browser_info: Path): Job =
{
val parent = info.parent.getOrElse("")
@@ -371,8 +373,10 @@
val args_xml =
{
import XML.Encode._
- pair(bool, pair(string, pair(string, list(string))))(
- output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
+ pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
+ pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+ (output.isDefined, (options, (verbose, (browser_info, (parent,
+ (name, (info.base_name, info.theories))))))))
}
new Job(cwd, env, script, YXML.string_of_body(args_xml))
}
@@ -454,7 +458,7 @@
Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
else None
echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
- val job = start_job(name, info, output)
+ val job = start_job(name, info, output, options, verbose, browser_info)
loop(pending, running + (name -> job), results)
}
else {
--- a/src/Pure/System/options.scala Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/options.scala Tue Jul 24 00:29:36 2012 +0200
@@ -79,6 +79,11 @@
}
options
}
+
+
+ /* encode */
+
+ val encode: XML.Encode.T[Options] = (options => options.encode)
}
--- a/src/Pure/System/session.ML Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/System/session.ML Tue Jul 24 00:29:36 2012 +0200
@@ -9,11 +9,13 @@
val id: unit -> string list
val name: unit -> string
val welcome: unit -> string
- val init: bool -> string -> string -> unit
+ val finish: unit -> unit
+ val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
+ string -> string -> bool * string -> string -> bool -> unit
+ val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
string -> bool -> string list -> string -> string -> bool * string ->
string -> int -> bool -> bool -> int -> int -> int -> int -> unit
- val finish: unit -> unit
end;
structure Session: SESSION =
@@ -63,9 +65,9 @@
end;
-(* init *)
+(* init_name *)
-fun init reset parent name =
+fun init_name reset parent name =
if not (member (op =) (! session) parent) orelse not (! session_finished) then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
else (add_path reset name; session_finished := false);
@@ -94,26 +96,31 @@
fun dumping (_, "") = NONE
| dumping (cp, path) = SOME (cp, Path.explode path);
+fun with_timing _ false f x = f x
+ | with_timing item true f x =
+ let
+ val start = Timing.start ();
+ val y = f x;
+ val timing = Timing.result start;
+ val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
+ |> Real.fmt (StringCvt.FIX (SOME 2));
+ val _ =
+ Output.physical_stderr ("Timing " ^ item ^ " (" ^
+ string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
+ Timing.message timing ^ ", factor " ^ factor ^ ")\n");
+ in y end;
+
+fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose =
+ (init_name reset parent name;
+ Present.init build info info_path doc doc_graph doc_variants (path ()) name
+ (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ())));
+
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
name dump rpath level timing verbose max_threads trace_threads
parallel_proofs parallel_proofs_threshold =
((fn () =>
- (init reset parent name;
- Present.init build info info_path doc doc_graph doc_variants (path ()) name
- (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
- if timing then
- let
- val start = Timing.start ();
- val _ = use root;
- val timing = Timing.result start;
- val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
- |> Real.fmt (StringCvt.FIX (SOME 2));
- val _ =
- Output.physical_stderr ("Timing " ^ item ^ " (" ^
- string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
- Timing.message timing ^ ", factor " ^ factor ^ ")\n");
- in () end
- else use root;
+ (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose;
+ with_timing item timing use root;
finish ()))
|> Unsynchronized.setmp Proofterm.proofs level
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ())