diff options
Diffstat (limited to 'doc/changelog/04-tactics/11023-nativecompute-timing.rst')
| -rw-r--r-- | doc/changelog/04-tactics/11023-nativecompute-timing.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst new file mode 100644 index 0000000000..2afa3990ac --- /dev/null +++ b/doc/changelog/04-tactics/11023-nativecompute-timing.rst @@ -0,0 +1,7 @@ +- 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 + <https://github.com/coq/coq/pull/11023>`_, by Jason Gross). |