coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report.

From: Yoriyuki Yamagata <yoriyuki.yamagata AT aist.go.jp>
To: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>, david.nowak AT aist.go.jp
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report.
Date: Tue, 21 Dec 2010 18:55:45 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=my5kpHkRO9VvXHwanEp+TInAzDM2b6NI3loWjXfCNcYTPr1TBNfk5djPu9igIwCSSS sDVfzfGeEki/5pmzFYqZClrPgPcb5MAllQ7kcb+u4vHFllQBb2PeRHc3PhqUMYzG2+K+ JgJ1PRM7wHtL79v4xfQwqxC1OpugBxaot0CKA=

Hi, Pierre and David.

Thank you for your help. Adding abstract tactic to omega makes Defined much faster. My bal function is defined without a problem now.

2010/12/20 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?

I think it is a 32-bit system, though I'm not sure. file command say coqtop.opt is a 32-bit binary, so I assume it is executed using the 32-bit environment but perhaps my knowledge is falling shortly here.

Best,
--

Yoriyuki　Yamagata
yoriyuki.yamagata AT aist.go.jp
http://staff.aist.go.jp/yoriyuki.yamagata/

[Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report., Yoriyuki Yamagata
- Re: [Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report., Pierre Courtieu
  - Re: [Coq-Club] Anomaly: uncaught exception Invalid_argument "String.create". Please report., Yoriyuki Yamagata