# HG changeset patch # User wenzelm # Date 1245251246 -7200 # Node ID f27cc190083b2d9ad6ade6d86bc71e2bb7163ff5 # Parent 0d2f700fe5e7c0652ca125563a1ebe17f45a373e usedir: internal timing option; diff -r 0d2f700fe5e7 -r f27cc190083b doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:07:26 2009 +0200 +++ b/doc-src/System/Thy/Presentation.thy Wed Jun 17 17:07:26 2009 +0200 @@ -299,8 +299,8 @@ \begin{center}\small \begin{tabular}{rcl} - @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\ - @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"} + @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\ + @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"} \end{tabular} \end{center} @@ -454,6 +454,7 @@ -p LEVEL set level of detail for proof objects -r reset session path -s NAME override session NAME + -t BOOL internal session timing (default false) -v BOOL be verbose (default false) Build object-logic or run examples. Also creates browsing @@ -563,6 +564,9 @@ for internal proof objects, see also the \emph{Isabelle Reference Manual}~\cite{isabelle-ref}. + \medskip The @{verbatim "-t"} option produces a more detailed + internal timing report of the session. + \medskip The @{verbatim "-v"} option causes additional information to be printed while running the session, notably the location of prepared documents. diff -r 0d2f700fe5e7 -r f27cc190083b doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 17:07:26 2009 +0200 +++ b/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 17:07:26 2009 +0200 @@ -323,8 +323,8 @@ \begin{center}\small \begin{tabular}{rcl} - \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\ - \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}} + \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}{\isacharplus}{\isachardoublequote}} \\ + \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}{\isacharasterisk}{\isachardoublequote}} \end{tabular} \end{center} @@ -480,6 +480,7 @@ -p LEVEL set level of detail for proof objects -r reset session path -s NAME override session NAME + -t BOOL internal session timing (default false) -v BOOL be verbose (default false) Build object-logic or run examples. Also creates browsing @@ -580,6 +581,9 @@ for internal proof objects, see also the \emph{Isabelle Reference Manual}~\cite{isabelle-ref}. + \medskip The \verb|-t| option produces a more detailed + internal timing report of the session. + \medskip The \verb|-v| option causes additional information to be printed while running the session, notably the location of prepared documents. diff -r 0d2f700fe5e7 -r f27cc190083b lib/Tools/usedir --- a/lib/Tools/usedir Wed Jun 17 17:07:26 2009 +0200 +++ b/lib/Tools/usedir Wed Jun 17 17:07:26 2009 +0200 @@ -31,6 +31,7 @@ echo " -p LEVEL set level of detail for proof objects" echo " -r reset session path" echo " -s NAME override session NAME" + echo " -t BOOL internal session timing (default false)" echo " -v BOOL be verbose (default false)" echo echo " Build object-logic or run examples. Also creates browsing" @@ -84,12 +85,13 @@ RESET=false SESSION="" PROOFS=0 +TIMING=false VERBOSE=false function getoptions() { OPTIND=1 - while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT + while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT do case "$OPT" in C) @@ -158,6 +160,10 @@ s) SESSION="$OPTARG" ;; + t) + check_bool "$OPTARG" + TIMING="$OPTARG" + ;; v) check_bool "$OPTARG" VERBOSE="$OPTARG" @@ -229,7 +235,7 @@ LOG="$LOGDIR/$ITEM" "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \ + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \ -q -w $LOGIC $NAME > "$LOG" RC="$?" else @@ -238,7 +244,7 @@ LOG="$LOGDIR/$ITEM" "$ISABELLE_PROCESS" \ - -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \ + -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \ -r -q "$LOGIC" > "$LOG" RC="$?" cd .. diff -r 0d2f700fe5e7 -r f27cc190083b src/Pure/System/session.ML --- a/src/Pure/System/session.ML Wed Jun 17 17:07:26 2009 +0200 +++ b/src/Pure/System/session.ML Wed Jun 17 17:07:26 2009 +0200 @@ -9,8 +9,9 @@ val id: unit -> string list val name: unit -> string val welcome: unit -> string - val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list -> - string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit + val use_dir: string -> string -> bool -> string list -> bool -> bool -> + string -> bool -> string list -> string -> string -> bool * string -> + string -> int -> bool -> bool -> int -> int -> bool -> unit val finish: unit -> unit end; @@ -72,8 +73,7 @@ (* finish *) fun finish () = - (Output.accumulated_time (); - ThyInfo.finish (); + (ThyInfo.finish (); Present.finish (); Future.shutdown (); session_finished := true); @@ -92,13 +92,20 @@ fun dumping (_, "") = NONE | dumping (cp, path) = SOME (cp, Path.explode path); -fun use_dir root build modes reset info doc doc_graph doc_versions - parent name dump rpath level verbose max_threads trace_threads parallel_proofs = +fun use_dir item root build modes reset info doc doc_graph doc_versions parent + name dump rpath level timing verbose max_threads trace_threads parallel_proofs = ((fn () => (init reset parent name; Present.init build info doc doc_graph doc_versions (path ()) name (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ())); - use root; + if timing then + let + val start = start_timing (); + val _ = use root; + val stop = end_timing start; + val _ = Output.std_error ("Timing " ^ item ^ " (" ^ #message stop ^ ")\n"); + in () end + else use root; finish ())) |> setmp_noncritical Proofterm.proofs level |> setmp_noncritical print_mode (modes @ print_mode_value ())