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
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?
those aren't tactic monad binds, they're https://github.com/coq/coq/blob/1a64b1560ce88855a76e2faa14cec2864de2f37c/engine/logic_monad.ml#L67
Ah, I see, so the calls get inlined by the compiler and there's probably no cost?
you can try benching with is_debug = constant false for a worst case estimate of its cost I guess
I removed the nonlogical stuff entirely some time ago, impact was minimal so I didn't submit the PR
Last updated: May 28 2023 at 16:30 UTC