The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

There's the printing effects plugin and Set Debug Cbv which will let you do rudimentary debugging in cbv.  You can also extract your code to OCaml and debug it there.

On Thu, Dec 17, 2020, 11:20 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

My bad.  There is something else going on in the recursive function.
It passes the recursive call as a continuation, which is being called
more often than I thought, and is running until out of fuel in some
cases even though the outer recursion doesn't.

I wish there was an easy way to debug Gallina code.

Thanks anyway to Jason and Clément for the suggestions.

On Wed, 16 Dec 2020 21:41:36 -0500
Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

> On 12/16/20 8:31 PM, jonikelee AT gmail.com wrote:
> > I have a recursive Gallina function that uses a nat-typed fuel arg
> > to guarantee termination.  In cases where the function terminates
> > prior to running out of fuel, I've found that larger than necessary
> > fuel args are very costly. For example, with a fuel value of 100,
> > the function takes 30 times longer than if the fuel value is 10
> > (neither runs out of fuel, all other args are the same). 
>
> What if you pass much larger fuel values, like 10000?
>
> > I guess this is probably due to the overhead of nats in Gallina.
> > But it is still surprising to me, considering that if I wrote a
> > function to traverse the first 8 links in a list, I wouldn't expect
> > it to take 30 times longer with a 100-element list than a 10-element
> > list. 
>
> The 30x factor is surprising, but a small difference wouldn't be
> entirely unexpected for large constants, since they have to be
> constructed.  Try replacing 100 with (Nat.of_uint 100%uint), or
> passing 10000 as the fuel (which will automatically get interpreted
> as (Nat.of_uint 10000%uint)):
>
> Fixpoint collatz (fuel: nat) (start: positive) :=
>   match fuel with
>   | O => false
>   | S fuel =>
>     match start with
>     | xO x => collatz fuel x
>     | xI _ => collatz fuel (start * 3 + 1)
>     | xH => true
>     end
>   end.
>
> Require Import Decimal.
>
> Time Compute (collatz 50 150).    0s
> Time Compute (collatz 2000 150).  0.006s
> Time Compute (collatz 5000 150).  0.021s
> Time Compute (collatz 10000 150). 0s (w/ warning)
>
>
>