mit-plv / engine-bench Goto Github PK

coq/coq#12600 was an issue with non-constant-time closedness checking, not evars, so we should add a requirement to be able to cache connotations that depend only on subterms (such as groundedness checking). This might be a thing that occurs off to the side rather than inside the proof engine though?

It would be nice if the Coq CI target would leave behind a clean git status so that one can easily detect that an automated refactor didn't touch this repository.

What about the following tail-recursive variants of biga, bigb?

(* tail-recursive biga, bigb *)
Fixpoint biga' (n : nat) (f : Prop -> Prop)
:= match n with
   | 0 => f True
   | S n => biga' n (fun x => forall a : Prop, f (a -> x)) 
   end.
Fixpoint bigb' (n : nat) (f : Prop -> Prop)
:= match n with
   | 0 => f True
   | S n => bigb' n (fun x => forall b : Prop, f (b -> x)) 
   end.

On my system:
original: (real: 7.15, user: 6.75, sys: 0.35, mem: 2544640 ko)
tail-recursive: (real: 0.13, user: 0.08, sys: 0.01, mem: 173364 ko)