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?
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?
dunno
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: Oct 13 2024 at 01:02 UTC