The Coq mailing list

[Jesper Bengtson <jebe AT itu.dk>]

Greetings everyone.

My name is Jesper Bengtson, and I am currently working on a tool for 
verifying Java programs inside Coq. We're at a stage where we try to create 
some tactics of our own to increase performance and to make life easier for 
the user. The tactics do proofs by reflection, but we're running into some 
performance problems with Ltac.

Whenever we build large data-structures in Ltac we take a performance hit. It 
seems like whenever the constr:(...)-operator is used, the whole Galina-term 
is re-type-checked. For instance, the following Ltac-function (that adds the 
number n to m) seems to be quadratic when we time it:

Ltac count_ltac n m := 
  match n with
    | 0 => m
    | S ?n => let m := constr:(S m) in count_ltac n m
  end.

Is there any way to lazily build the term and then type check it at the end? 
Calling this function with n=4000 took nearly 40 seconds on my machine. Are 
we missing something? Is there a way around this problem?

Best regards.

Jesper Bengtson