Jason Gross (Apr 01 2021 at 12:09): Jason Gross (Apr 01 2021 at 12:09):I think every tactic step involves two more binds in the monad than it needs to. @Pierre-Marie Pédrot (or anyone else), do you have an estimate of the cost of this? The source of the binds is Ltac_debug.is_debug: https://github.com/coq/coq/blob/0fc82e9651ee1dbc429c9b328b90ad8ad1a3cb14/plugins/ltac/tactic_debug.ml#L238-L246
In most cases db will be DebugOff and we can skip the !breakpoint >>= bind. Furthermore, every use of is_debug looks like is_debug debug >>= fun db -> if db then do_stuff else return () and again we can skip this bind in the common case. I seem to recall (from the profiler) that the cost of having an extra bind everywhere is something like 1%, so this may be a relatively easy way to get a 1%--2% speedup across all tactic code?
Gaëtan Gilbert (Apr 01 2021 at 12:20):those aren't tactic monad binds, they're https://github.com/coq/coq/blob/1a64b1560ce88855a76e2faa14cec2864de2f37c/engine/logic_monad.ml#L67
Jason Gross (Apr 01 2021 at 12:23):Ah, I see, so the calls get inlined by the compiler and there's probably no cost?
Gaëtan Gilbert (Apr 01 2021 at 12:27):dunno
you can try benching with is_debug = constant false for a worst case estimate of its cost I guess
Emilio Jesús Gallego Arias (Apr 01 2021 at 12:46):I removed the nonlogical stuff entirely some time ago, impact was minimal so I didn't submit the PR
Last updated: Apr 19 2024 at 00:02 UTC