Stream: Coq devs & plugin devs

Topic: Minor Perf Issues in Ltac Debug


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Oct 15 2021 at 21:02 UTC