diff options
| author | Paul Steckler | 2017-08-15 10:31:09 -0400 |
|---|---|---|
| committer | Paul Steckler | 2017-08-17 11:40:26 -0400 |
| commit | 51d4d83316f91abb25ea331bfdc1dcba17362dc8 (patch) | |
| tree | 25eb115f4faeb87d6ae0d3db687f3111fdcf1886 /vernac | |
| parent | 63da901edc3ab5b69098499cdc01ab50ed9b3353 (diff) | |
Add native compute profiling, BZ#5170
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f63ed6f48..8738e58e82 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1457,6 +1457,22 @@ let _ = optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } +let _ = + declare_string_option + { optdepr = false; + optname = "native_compute profiler output"; + optkey = ["NativeCompute"; "Profile"; "Filename"]; + optread = Nativenorm.get_profile_filename; + optwrite = Nativenorm.set_profile_filename } + +let _ = + declare_bool_option + { optdepr = false; + optname = "enable native compute profiling"; + optkey = ["NativeCompute"; "Profiling"]; + optread = Nativenorm.get_profiling_enabled; + optwrite = Nativenorm.set_profiling_enabled } + let vernac_set_strategy locality l = let local = make_locality locality in let glob_ref r = |