The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello,

I think this is a known bug of the reduction engine based on the
virtual machine. It happens on *very* large terms. Do you have a 32 or
64 bit system?

You can first try to replace all you "omega" tactics by "abstract
omega" and see if the bug is still there. Putting abstract on a
(final) tactic puts the corresponding term in an auxiliary lemma
instead of inlining it inside the current proof term. This way you
keep the current proof term a bit smaller.

If this is not enough you can try to put abstract on other (final)
expensive tactics.

Hope this helps,
Pierre Courtieu


2010/12/20 Yoriyuki Yamagata 
<yoriyuki.yamagata AT aist.go.jp>:
> Hi, list.
>
> I'm a completely beginner of Coq, and try to learn it by implementing
> AVL-tree.  I complete a definition (with a correctness proof) of  the
> balancing function, but unfortunately "Defined" command takes a long time
> then gives me a message "Anomaly: uncaught exception Invalid_argument
> "String.create". Please report." and fails.
>
> I guess that Coq try to allocate a too large string, but what is the cause
> of it and is there a way to avoid it?  I may use Qed but then I suppose that
> we cannot reason about the function later(?).  Also, I use omega tactic a
> lot in the proof.  Could this cause the problem?
> I can manually prove the equations but it would be very tedious.
>
> I attach my proof. (I know that my proof is really badly written.)
> --
> Yoriyuki　Yamagata
> yoriyuki.yamagata AT aist.go.jp
> http://staff.aist.go.jp/yoriyuki.yamagata/
>
>