We have Timeout command to constraint the execution time.
Is there a similar tool for memory usage?
With coq-reduction-effects installed, the following code exhausted my memory:
(* Testing the printing side effect *) From Coq Require Import NArith Streams. From ReductionEffect Require Import PrintingEffect. Open Scope N_scope. CoFixpoint fib1 (a b : N) : Stream N := let t := fib1 b (a + b) in let _ := print t in Cons a t. Eval cbv in (Str_nth 10 (fib1 0 1)). (* Works fine *) CoFixpoint fib2 (a b : N) : Stream N := let t := fib2 b (a + b) in let _ := print (hd t) in Cons a t. Eval cbv in (Str_nth 10 (fib2 0 1)). (* Stack overflow *)
and I hope to capture this failure.