Re: [isabelle] Probelm with the "definition" command



Jesus, this is a known problem. If you are OK with inputting the matrix on the
ML level, just stick with it. Alternatively you can look at
http://afp.sourceforge.net/browser_info/current/HOL/HOL-Library/Flyspeck-Tame/Arch.html
where some constants are defined at the ML level (in "Archives/*.ML") but
imported into Isabelle (as Tri, Quad etc). This way you may not need to edit any
generated ML code by hand.

Tobias

Am 29/04/2013 18:01, schrieb Jesus Aransay:
> Dear all,
> 
> as a different but related issue to my previous mail, when we try to
> input matrices of dimension over 250 * 250 (approx) as elements of
> type "iarray" (the IArray constructor is applied to lists,
> http://isabelle.in.tum.de/library/HOL/HOL-Library/IArray.html) in
> Isabelle (Isabelle/JEdit 2013), by means of the "definition" command,
> processing time gets really slow (of the order of minutes) until the
> editor crashes or we just give it up. Inputting the matrices directly
> in the generated SML code works well.
> 
> Is there any way to improve this behavior?
> 
> Thanks for any hints,
> 
> Jesus
> 
> --
> Jesús María Aransay Azofra
> Universidad de La Rioja
> Dpto. de Matemáticas y Computación
> tlf.: (+34) 941299438 fax: (+34) 941299460
> mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
> Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.