From 054505fffac27409d6c0f613337f9cfd7e5c36ba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 29 Mar 2020 22:18:42 -0400 Subject: NativeCompute Timing: Use real, not user time User time is unreliable for `native_compute`. Also output time spent in conversion to native code, just in case that is ever slow. Note that this also removes spurious newlines in the output. Fixes #11962 --- doc/changelog/04-tactics/11023-nativecompute-timing.rst | 7 ------- doc/changelog/04-tactics/11025-nativecompute-timing.rst | 11 +++++++++++ doc/sphinx/proof-engine/tactics.rst | 6 ++++-- 3 files changed, 15 insertions(+), 9 deletions(-) delete mode 100644 doc/changelog/04-tactics/11023-nativecompute-timing.rst create mode 100644 doc/changelog/04-tactics/11025-nativecompute-timing.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst deleted file mode 100644 index e8cdfcca21..0000000000 --- a/doc/changelog/04-tactics/11023-nativecompute-timing.rst +++ /dev/null @@ -1,7 +0,0 @@ -- The :flag:`NativeCompute Timing` flag causes calls to - :tacn:`native_compute` (as well as kernel calls to the native - compiler) to emit separate timing information about compilation, - execution, and reification. It replaces the timing information - previously emitted when the `-debug` flag was set, and allows more - fine-grained timing of the native compiler (`#11023 - `_, by Jason Gross). diff --git a/doc/changelog/04-tactics/11025-nativecompute-timing.rst b/doc/changelog/04-tactics/11025-nativecompute-timing.rst new file mode 100644 index 0000000000..cb77457c31 --- /dev/null +++ b/doc/changelog/04-tactics/11025-nativecompute-timing.rst @@ -0,0 +1,11 @@ +- **Changed:** The :flag:`NativeCompute Timing` flag causes calls to + :tacn:`native_compute` (as well as kernel calls to the native + compiler) to emit separate timing information about conversion to + native code, compilation, execution, and reification. It replaces + the timing information previously emitted when the `-debug` flag was + set, and allows more fine-grained timing of the native compiler + (`#11025 `_, by Jason Gross). + Additionally, the timing information now uses real time rather than + user time (Fixes `#11962 + `_, `#11963 + `_, by Jason Gross) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6a280b74c2..7da453b7af 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3134,8 +3134,10 @@ the conversion in hypotheses :n:`{+ @ident}`. .. flag:: NativeCompute Timing This flag causes all calls to the native compiler to print - timing information for the compilation, execution, and - reification phases of native compilation. + timing information for the conversion to native code, + compilation, execution, and reification phases of native + compilation. Timing is printed in units of seconds of + wall-clock time. .. flag:: NativeCompute Profiling -- cgit v1.2.3