--- a/NEWS Wed Mar 13 17:17:33 2013 +0000
+++ b/NEWS Wed Mar 13 22:46:28 2013 +0100
@@ -6,6 +6,13 @@
*** General ***
+* Sessions may be organized via 'chapter' specifications in the ROOT
+file, which determines a two-level hierarchy of browser info. The old
+tree-like organization via implicit sub-session relation, with its
+tendency towards erratic fluctuation of URLs, has been discontinued.
+The default chapter is "Unsorted". Potential INCOMPATIBILITY for HTML
+presentation of theories.
+
* Discontinued obsolete 'uses' within theory header. Note that
commands like 'ML_file' work without separate declaration of file
dependencies. Minor INCOMPATIBILITY.
--- a/etc/options Wed Mar 13 17:17:33 2013 +0000
+++ b/etc/options Wed Mar 13 22:46:28 2013 +0100
@@ -51,8 +51,10 @@
-- "level of tracing information for multithreading"
option parallel_proofs : int = 2
-- "level of parallel proof checking: 0, 1, 2"
-option parallel_proofs_threshold : int = 100
- -- "threshold for sub-proof parallelization"
+option parallel_subproofs_saturation : int = 100
+ -- "upper bound for forks of nested proofs (multiplied by worker threads)"
+option parallel_subproofs_threshold : real = 0.01
+ -- "lower bound of timing estimate for forked nested proofs (seconds)"
option parallel_proofs_reuse_timing : bool = true
-- "reuse timing information from old log file for parallel proof scheduling"
--- a/lib/html/library_index_content.template Wed Mar 13 17:17:33 2013 +0000
+++ b/lib/html/library_index_content.template Wed Mar 13 22:46:28 2013 +0100
@@ -8,10 +8,6 @@
that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
</li>
</ul>
- <ul>
- <li>HOL with explicit <a href="HOL-Proofs/index.html">proof terms</a>.
- </li>
- </ul>
</li>
</ul>
--- a/src/Doc/System/Presentation.thy Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Doc/System/Presentation.thy Wed Mar 13 22:46:28 2013 +0100
@@ -57,9 +57,11 @@
theory browsing information, including HTML documents that show the
theory sources and the relationship with its ancestors and
descendants. Besides the HTML file that is generated for every
- theory, Isabelle stores links to all theories in an index
- file. These indexes are linked with other indexes to represent the
- overall tree structure of the sessions.
+ theory, Isabelle stores links to all theories of a session in an
+ index file. As a second hierarchy, groups of sessions are organized
+ as \emph{chapters}, with a separate index. Note that the implicit
+ tree structure of the session build hierarchy is \emph{not} relevant
+ for the presentation.
Isabelle also generates graph files that represent the theory
dependencies within a session. There is a graph browser Java applet
@@ -80,7 +82,7 @@
\end{ttbox}
The presentation output will appear in @{verbatim
- "$ISABELLE_BROWSER_INFO/FOL"} as reported by the above verbose
+ "$ISABELLE_BROWSER_INFO/FOL/FOL"} as reported by the above verbose
invocation of the build process.
Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file
@@ -99,11 +101,9 @@
\bigskip The theory browsing information is stored in a
sub-directory directory determined by the @{setting_ref
ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
- session identifier (according to the tree structure of sub-sessions
- by default). In order to present Isabelle applications on the web,
- the corresponding subdirectory from @{setting ISABELLE_BROWSER_INFO}
- can be put on a WWW server.
-*}
+ session chapter and identifier. In order to present Isabelle
+ applications on the web, the corresponding subdirectory from
+ @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server. *}
section {* Preparing session root directories \label{sec:tool-mkroot} *}
@@ -311,7 +311,7 @@
inspect {\LaTeX} runs in further detail, e.g.\ like this:
\begin{ttbox}
- cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
+ cd ~/.isabelle/IsabelleXXXX/browser_info/Unsorted/Test/document
isabelle latex -o pdf
\end{ttbox}
*}
--- a/src/Doc/System/Sessions.thy Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Doc/System/Sessions.thy Wed Mar 13 22:46:28 2013 +0100
@@ -38,15 +38,20 @@
\emph{outer syntax} of Isabelle/Isar, see also
\cite{isabelle-isar-ref}. This defines common forms like
identifiers, names, quoted strings, verbatim text, nested comments
- etc. The grammar for a single @{syntax session_entry} is given as
- syntax diagram below; each ROOT file may contain multiple session
- specifications like this.
+ etc. The grammar for @{syntax session_chapter} and @{syntax
+ session_entry} is given as syntax diagram below; each ROOT file may
+ contain multiple specifications like this. Chapters help to
+ organize browser info (\secref{sec:info}), but have no formal
+ meaning. The default chapter is ``@{text "Unsorted"}''.
Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
mode @{verbatim "isabelle-root"} for session ROOT files, which is
enabled by default for any file of that name.
@{rail "
+ @{syntax_def session_chapter}: @'chapter' @{syntax name}
+ ;
+
@{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
;
body: description? options? ( theories + ) files?
--- a/src/HOL/ROOT Wed Mar 13 17:17:33 2013 +0000
+++ b/src/HOL/ROOT Wed Mar 13 22:46:28 2013 +0100
@@ -1,7 +1,9 @@
chapter HOL
session HOL (main) = Pure +
- description {* Classical Higher-order Logic *}
+ description {*
+ Classical Higher-order Logic.
+ *}
options [document_graph]
theories Complex_Main
files
@@ -11,7 +13,9 @@
"document/root.tex"
session "HOL-Proofs" = Pure +
- description {* HOL-Main with explicit proof terms *}
+ description {*
+ HOL-Main with explicit proof terms.
+ *}
options [document = false, proofs = 2]
theories Main
files
@@ -19,7 +23,9 @@
"Tools/Quickcheck/PNF_Narrowing_Engine.hs"
session "HOL-Library" (main) in Library = HOL +
- description {* Classical Higher-order Logic -- batteries included *}
+ description {*
+ Classical Higher-order Logic -- batteries included.
+ *}
theories
Library
(*conflicting type class instantiations*)
@@ -204,7 +210,12 @@
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
options [document = false, document_graph = false, browser_info = false]
- theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char
+ theories
+ Generate
+ Generate_Binary_Nat
+ Generate_Target_Nat
+ Generate_Efficient_Datastructures
+ Generate_Pretty_Char
session "HOL-Metis_Examples" in Metis_Examples = HOL +
description {*
@@ -264,7 +275,9 @@
files "document/root.bib" "document/root.tex"
session "HOL-Auth" in Auth = HOL +
- description {* A new approach to verifying authentication protocols. *}
+ description {*
+ A new approach to verifying authentication protocols.
+ *}
options [document_graph]
theories
Auth_Shared
@@ -346,7 +359,9 @@
theories Hilbert_Classical
session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
- description {* Examples for program extraction in Higher-Order Logic *}
+ description {*
+ Examples for program extraction in Higher-Order Logic.
+ *}
options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
theories [document = false]
"~~/src/HOL/Library/Code_Target_Numeral"
@@ -471,7 +486,9 @@
files "document/root.tex"
session "HOL-ex" in ex = HOL +
- description {* Miscellaneous examples for Higher-Order Logic. *}
+ description {*
+ Miscellaneous examples for Higher-Order Logic.
+ *}
options [timeout = 3600, condition = ISABELLE_POLYML]
theories [document = false]
"~~/src/HOL/Library/State_Monad"
@@ -669,12 +686,16 @@
theories [quick_and_dirty] VC_Condition
session "HOL-Cardinals-Base" in Cardinals = HOL +
- description {* Ordinals and Cardinals, Base Theories *}
+ description {*
+ Ordinals and Cardinals, Base Theories.
+ *}
options [document = false]
theories Cardinal_Arithmetic
session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
- description {* Ordinals and Cardinals, Full Theories *}
+ description {*
+ Ordinals and Cardinals, Full Theories.
+ *}
options [document = false]
theories Cardinals
files
@@ -683,17 +704,23 @@
"document/root.bib"
session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
- description {* Bounded Natural Functors for Datatypes *}
+ description {*
+ Bounded Natural Functors for Datatypes.
+ *}
options [document = false]
theories BNF_LFP
session "HOL-BNF" in BNF = "HOL-Cardinals" +
- description {* Bounded Natural Functors for (Co)datatypes *}
+ description {*
+ Bounded Natural Functors for (Co)datatypes.
+ *}
options [document = false]
theories BNF
session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
- description {* Examples for Bounded Natural Functors *}
+ description {*
+ Examples for Bounded Natural Functors.
+ *}
options [document = false]
theories
Lambda_Term
@@ -720,7 +747,9 @@
files "document/root.tex"
session "HOL-NSA" in NSA = HOL +
- description {* Nonstandard analysis. *}
+ description {*
+ Nonstandard analysis.
+ *}
options [document_graph]
theories Hypercomplex
files "document/root.tex"
@@ -958,7 +987,9 @@
files "document/root.tex"
session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
- description {* Misc HOLCF examples *}
+ description {*
+ Miscellaneous examples for HOLCF.
+ *}
options [document = false]
theories
Dnat
@@ -1046,7 +1077,9 @@
TrivEx2
session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
- description {* Some rather large datatype examples (from John Harrison). *}
+ description {*
+ Some rather large datatype examples (from John Harrison).
+ *}
options [document = false]
theories [condition = ISABELLE_FULL_TEST, timing]
Brackin
@@ -1055,7 +1088,9 @@
Verilog
session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
- description {* Some benchmark on large record. *}
+ description {*
+ Some benchmark on large record.
+ *}
options [document = false]
theories [condition = ISABELLE_FULL_TEST, timing]
Record_Benchmark
--- a/src/Pure/Isar/toplevel.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Isar/toplevel.ML Wed Mar 13 22:46:28 2013 +0100
@@ -91,8 +91,8 @@
val status: transition -> Markup.T -> unit
val add_hook: (transition -> state -> state -> unit) -> unit
val approximative_id: transition -> {file: string, offset: int, name: string} option
- val get_timing: transition -> Time.time
- val put_timing: Time.time -> transition -> transition
+ val get_timing: transition -> Time.time option
+ val put_timing: Time.time option -> transition -> transition
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command_errors: bool -> transition -> state -> Runtime.error list * state option
val command_exception: bool -> transition -> state -> state
@@ -346,7 +346,7 @@
int_only: bool, (*interactive-only*)
print: bool, (*print result state*)
no_timing: bool, (*suppress timing*)
- timing: Time.time, (*prescient timing information*)
+ timing: Time.time option, (*prescient timing information*)
trans: trans list}; (*primitive transitions (union)*)
fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
@@ -356,7 +356,7 @@
fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
-val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
+val empty = make_transition ("", Position.none, false, false, false, NONE, []);
(* diagnostics *)
@@ -638,14 +638,12 @@
local
fun timing_message tr (t: Timing.timing) =
- if Timing.is_relevant_time (#elapsed t) then
- (case approximative_id tr of
- SOME id =>
- (Output.protocol_message
- (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
- handle Fail _ => ())
- | NONE => ())
- else ();
+ (case approximative_id tr of
+ SOME id =>
+ (Output.protocol_message
+ (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
+ handle Fail _ => ())
+ | NONE => ());
fun app int (tr as Transition {trans, print, no_timing, ...}) =
setmp_thread_position tr (fn state =>
@@ -727,29 +725,38 @@
val get_result = Result.get o Proof.context_of;
val put_result = Proof.map_context o Result.put;
-fun proof_future_enabled st =
+fun timing_estimate include_head elem =
+ let
+ val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
+ val timings = map get_timing trs;
+ in
+ if forall is_some timings then
+ SOME (fold (curry Time.+ o the) timings Time.zeroTime)
+ else NONE
+ end;
+
+fun priority NONE = ~1
+ | priority (SOME estimate) =
+ Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+
+fun proof_future_enabled estimate st =
(case try proof_of st of
NONE => false
| SOME state =>
not (Proof.is_relevant state) andalso
(if can (Proof.assert_bottom true) state
then Goal.future_enabled ()
- else Goal.future_enabled_nested 2));
-
-fun priority elem =
- let
- val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime;
- in
- if estimate = Time.zeroTime then ~1
- else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
- end;
+ else
+ (case estimate of
+ NONE => Goal.future_enabled_nested 2
+ | SOME t => Goal.future_enabled_timing t)));
fun atom_result tr st =
let
val st' =
if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
setmp_thread_position tr (fn () =>
- (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
+ (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr)))
(fn () => command tr st); st)) ()
else command tr st;
in (Result (tr, st'), st') end;
@@ -757,12 +764,13 @@
in
fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
- | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
+ | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
let
val (head_result, st') = atom_result head_tr st;
val (body_elems, end_tr) = element_rest;
+ val estimate = timing_estimate false elem;
in
- if not (proof_future_enabled st')
+ if not (proof_future_enabled estimate st')
then
let
val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
@@ -776,7 +784,7 @@
(fn state =>
setmp_thread_position head_tr (fn () =>
Goal.fork_name "Toplevel.future_proof"
- (priority (Thy_Syntax.Element (empty, SOME element_rest)))
+ (priority estimate)
(fn () =>
let
val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
--- a/src/Pure/System/isabelle_process.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/System/isabelle_process.ML Wed Mar 13 22:46:28 2013 +0100
@@ -243,7 +243,8 @@
if Multithreading.max_threads_value () < 2
then Multithreading.max_threads := 2 else ();
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
- Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
+ Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation";
+ Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold";
tracing_messages := Options.int options "editor_tracing_messages"
end);
--- a/src/Pure/System/session.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/System/session.ML Wed Mar 13 22:46:28 2013 +0100
@@ -94,7 +94,7 @@
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
name doc_dump rpath level timing verbose max_threads trace_threads
- parallel_proofs parallel_proofs_threshold =
+ parallel_proofs parallel_subproofs_saturation =
((fn () =>
let
val _ =
@@ -116,7 +116,7 @@
|> Unsynchronized.setmp Proofterm.proofs level
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
|> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
- |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
+ |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation
|> Unsynchronized.setmp Multithreading.trace trace_threads
|> Unsynchronized.setmp Multithreading.max_threads
(if Multithreading.available then max_threads
--- a/src/Pure/Thy/present.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/present.ML Wed Mar 13 22:46:28 2013 +0100
@@ -36,7 +36,6 @@
val html_path = html_ext o Path.basic;
val index_path = Path.basic "index.html";
val readme_html_path = Path.basic "README.html";
-val readme_path = Path.basic "README";
val documentN = "document";
val document_path = Path.basic documentN;
val doc_indexN = "session";
@@ -44,7 +43,7 @@
val graph_pdf_path = Path.basic "session_graph.pdf";
val graph_eps_path = Path.basic "session_graph.eps";
-fun show_path path = Path.implode (Path.append (File.pwd ()) path);
+fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
@@ -241,10 +240,7 @@
else (); [])
else doc_variants;
- val readme =
- if File.exists readme_html_path then SOME readme_html_path
- else if File.exists readme_path then SOME readme_path
- else NONE;
+ val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
val docs =
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
--- a/src/Pure/Thy/present.scala Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/present.scala Wed Mar 13 22:46:28 2013 +0100
@@ -19,8 +19,12 @@
private def read_sessions(dir: Path): List[(String, String)] =
{
- import XML.Decode._
- list(pair(string, string))(YXML.parse_body(File.read(dir + sessions_path)))
+ val path = dir + sessions_path
+ if (path.is_file) {
+ import XML.Decode._
+ list(pair(string, string))(YXML.parse_body(File.read(path)))
+ }
+ else Nil
}
private def write_sessions(dir: Path, sessions: List[(String, String)])
@@ -36,7 +40,7 @@
val sessions0 =
try { read_sessions(dir) }
- catch { case ERROR(_) => Nil case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
+ catch { case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
--- a/src/Pure/Thy/thy_info.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/thy_info.ML Wed Mar 13 22:46:28 2013 +0100
@@ -17,7 +17,7 @@
val loaded_files: string -> Path.T list
val remove_thy: string -> unit
val kill_thy: string -> unit
- val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} ->
+ val use_theories: {last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
(string * Position.T) list -> unit
val use_thys: (string * Position.T) list -> unit
val use_thy: string * Position.T -> unit
@@ -174,7 +174,7 @@
fun result_commit (Result {commit, ...}) = commit;
fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
-fun join_proofs (Result {theory, id, present, ...}) =
+fun join_proofs (Result {theory, id, ...}) =
let
val result1 = Exn.capture Thm.join_theory_proofs theory;
val results2 = Future.join_results (Goal.peek_futures id);
@@ -351,7 +351,7 @@
fun use_theories {last_timing, master_dir} imports =
schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
-val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current};
+val use_thys = use_theories {last_timing = K NONE, master_dir = Path.current};
val use_thy = use_thys o single;
@@ -361,7 +361,7 @@
let
val {name = (name, _), imports, ...} = header;
val _ = kill_thy name;
- val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports;
+ val _ = use_theories {last_timing = K NONE, master_dir = master_dir} imports;
val _ = Thy_Header.define_keywords header;
val parents = map (get_theory o base_name o fst) imports;
in Thy_Load.begin_theory master_dir header parents end;
--- a/src/Pure/Thy/thy_load.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/thy_load.ML Wed Mar 13 22:46:28 2013 +0100
@@ -22,7 +22,7 @@
val use_ml: Path.T -> unit
val exec_ml: Path.T -> generic_theory -> generic_theory
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
- val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
+ val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
Position.T -> string -> theory list -> theory * (unit -> unit) * int
val set_master_path: Path.T -> unit
val get_master_path: unit -> Path.T
--- a/src/Pure/Thy/thy_syntax.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/thy_syntax.ML Wed Mar 13 22:46:28 2013 +0100
@@ -17,7 +17,6 @@
val parse_spans: Token.T list -> span list
datatype 'a element = Element of 'a * ('a element list * 'a) option
val atom: 'a -> 'a element
- val fold_element: ('a -> 'b -> 'b) -> 'a element -> 'b -> 'b
val map_element: ('a -> 'b) -> 'a element -> 'b element
val flat_element: 'a element -> 'a list
val last_element: 'a element -> 'a
@@ -144,9 +143,6 @@
fun element (a, b) = Element (a, SOME b);
fun atom a = Element (a, NONE);
-fun fold_element f (Element (a, NONE)) = f a
- | fold_element f (Element (a, SOME (elems, b))) = f a #> (fold o fold_element) f elems #> f b;
-
fun map_element f (Element (a, NONE)) = Element (f a, NONE)
| map_element f (Element (a, SOME (elems, b))) =
Element (f a, SOME ((map o map_element) f elems, f b));
--- a/src/Pure/Tools/build.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Tools/build.ML Wed Mar 13 22:46:28 2013 +0100
@@ -50,8 +50,10 @@
|> 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 Goal.parallel_subproofs_saturation
+ (Options.int options "parallel_subproofs_saturation")
+ |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
+ (Options.real options "parallel_subproofs_threshold")
|> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
|> Unsynchronized.setmp Future.ML_statistics true
@@ -99,10 +101,10 @@
(case Symtab.lookup timings file of
SOME offsets =>
(case Inttab.lookup offsets offset of
- SOME (name', time) => if name = name' then time else Time.zeroTime
- | NONE => Time.zeroTime)
- | NONE => Time.zeroTime)
- | NONE => Time.zeroTime);
+ SOME (name', time) => if name = name' then SOME time else NONE
+ | NONE => NONE)
+ | NONE => NONE)
+ | NONE => NONE);
in
--- a/src/Pure/Tools/build.scala Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Tools/build.scala Wed Mar 13 22:46:28 2013 +0100
@@ -474,18 +474,6 @@
name: String, val info: Session_Info, output: Path, do_output: Boolean,
verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
{
- // global browser info dir
- if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
- {
- Isabelle_System.mkdirs(browser_info)
- File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
- browser_info + Path.explode("isabelle.gif"))
- File.write(browser_info + Path.explode("index.html"),
- File.read(Path.explode("~~/lib/html/library_index_header.template")) +
- File.read(Path.explode("~~/lib/html/library_index_content.template")) +
- File.read(Path.explode("~~/lib/html/library_index_footer.template")))
- }
-
def output_path: Option[Path] = if (do_output) Some(output) else None
private val parent = info.parent.getOrElse("")
@@ -867,12 +855,36 @@
}
else loop(queue, Map.empty, Map.empty)
- val session_entries =
- (for { (name, res) <- results.iterator; info = full_tree(name) }
- yield (info.chapter, (name, info.description))).toList.groupBy(_._1).map(
- { case (chapter, es) => (chapter, es.map(_._2)) })
- for ((chapter, entries) <- session_entries)
- Present.update_chapter_index(browser_info, chapter, entries)
+
+ /* global browser info */
+
+ if (!no_build) {
+ val browser_chapters =
+ (for {
+ (name, result) <- results.iterator
+ if result.rc == 0
+ info = full_tree(name)
+ if info.options.bool("browser_info")
+ } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
+ map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
+
+ for ((chapter, entries) <- browser_chapters)
+ Present.update_chapter_index(browser_info, chapter, entries)
+
+ if (!browser_chapters.isEmpty && !(browser_info + Path.explode("index.html")).is_file)
+ {
+ Isabelle_System.mkdirs(browser_info)
+ File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+ browser_info + Path.explode("isabelle.gif"))
+ File.write(browser_info + Path.explode("index.html"),
+ File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_footer.template")))
+ }
+ }
+
+
+ /* return code */
val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
if (rc != 0 && (verbose || !no_build)) {
--- a/src/Pure/goal.ML Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/goal.ML Wed Mar 13 22:46:28 2013 +0100
@@ -7,7 +7,8 @@
signature BASIC_GOAL =
sig
val parallel_proofs: int Unsynchronized.ref
- val parallel_proofs_threshold: int Unsynchronized.ref
+ val parallel_subproofs_saturation: int Unsynchronized.ref
+ val parallel_subproofs_threshold: real Unsynchronized.ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -32,6 +33,7 @@
val future_enabled_level: int -> bool
val future_enabled: unit -> bool
val future_enabled_nested: int -> bool
+ val future_enabled_timing: Time.time -> bool
val future_result: Proof.context -> thm future -> term -> thm
val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -191,7 +193,8 @@
(* scheduling parameters *)
val parallel_proofs = Unsynchronized.ref 1;
-val parallel_proofs_threshold = Unsynchronized.ref 100;
+val parallel_subproofs_saturation = Unsynchronized.ref 100;
+val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
fun future_enabled_level n =
Multithreading.enabled () andalso ! parallel_proofs >= n andalso
@@ -201,7 +204,10 @@
fun future_enabled_nested n =
future_enabled_level n andalso
- forked_count () < ! parallel_proofs_threshold * Multithreading.max_threads_value ();
+ forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value ();
+
+fun future_enabled_timing t =
+ future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold;
(* future_result *)
--- a/src/Tools/jEdit/src/isabelle_options.scala Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Tools/jEdit/src/isabelle_options.scala Wed Mar 13 22:46:28 2013 +0100
@@ -41,10 +41,10 @@
{
// FIXME avoid hard-wired stuff
private val relevant_options =
- Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
- "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
- "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
- "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay",
+ Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
+ "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale",
+ "jedit_tooltip_margin", "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
+ "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
"editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
"editor_update_delay", "editor_chart_delay")