LtacProf makes multi-success tactics very slow

[andres-erbsen]

Description of the problem

LtacProf makes multi-success tactics very slow.

Moderate test case: https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2Examples/swap.v#L61 (hundreds of milliseconds).
Large case: https://github.com/mit-plv/fiat-crypto/blob/c68a80bace827202d962815eda3522fae83f0108/src/Bedrock/End2End/X25519/GarageDoor.v#L251 (longer than I was willing to wait)

Is this issue well-known, or would it be worth minimizing the Bedrock2 example?

Coq Version

8.15.0

[JasonGross]

Would it be possible to make an artificial test-case that displays performance slowdown as a function of number of backtracks? The overhead should be a function of the number of backtracks, the size of the callstack, and the size of the difference in the callstack between the backtracking point and the multisuccess tactic.

The relevant bit of algorithmic implemention is at

coq/plugins/ltac/profile_ltac.ml

Lines 343 to 378 in 97f9c65

	let rec tclWRAPFINALLY before tac finally =
	let open Proofview in
	let open Proofview.Notations in
	before >>= fun v -> tclCASE tac >>= function
	| Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
	| Next (ret, tac') -> tclOR
	(finally v >>= fun () -> tclUNIT ret)
	(fun e -> tclWRAPFINALLY before (tac' e) finally)
	let do_profile s call_trace ?(count_call=true) tac =
	let open Proofview.Notations in
	(* We do an early check to [is_profiling] so that we save the
	overhead of [tclWRAPFINALLY] when profiling is not set
	*)
	Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function
	| false -> tac
	| true ->
	tclWRAPFINALLY
	(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
	match call_trace, Local.(!stack) with
	| (_, c) :: _, parent :: rest ->
	let name = string_of_call c in
	let node = get_child name parent in
	Local.(stack := node :: parent :: rest);
	Some (time ())
	| _ :: _, [] -> assert false
	| _ -> None
	)))
	tac
	(function
	| Some start_time ->
	(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
	(match call_trace with
	| (_, c) :: _ -> exit_tactic ~count_call start_time c
	| [] -> ()))))
	| None -> Proofview.tclUNIT ())

[andres-erbsen]

Hmm. I'd guess the first example backtracks 0 times. There may be some backtracks in the second example, but still I wouldn't expect many.

[JasonGross]

What's the significance of "multisuccess" if there's no backtracking? (I'd be extremely surprised if LtacProf impacted performance of match vs multimatch differently when the multimatch never made it to the second success.)