[isabelle] Probelm with the "definition" command

[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-mar...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logro�o, Espa�a

[Tobias Nipkow]

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-mar...@unirioja.es ; web: http://www.unirioja.es/cu/jearansa

> Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España
>

[Makarius]

On Mon, 29 Apr 2013, Jesus Aransay wrote:

> when we try to input matrices of dimension over 250 * 250

> ...

> processing time gets really slow (of the order of minutes) until the
> editor crashes or we just give it up.

> Is there any way to improve this behavior?

I can say more when you show me the concrete example, to get a better idea
what is the usual "problem class" that you have here.


Generally, the default inner syntax of Isabelle (for terms and types) is
made as flexible and powerful as feasible, which also means it does not
scale to arbitrarily large input. There is no fundamental problem here,
since that is only the default to get terms into the system, and there are
many other ways. You have already figured out some regular Isabelle/ML
interfaces to do that.

An alternative is to apply some tricks to import "blobs" directly into the
term language, while staying on the surface end-user syntax. This could
work via your own syntax translations, e.g. like this:

term "BIG_THING ''...''"

where ''...'' is an inner string token that is somehow turned into a term.
You can then apply different parser technology to operate on the given
''...'' string. (Technically there is a limit of 64 MB size for such
strings.)

In principle you could also load a file into the term, although that would
pose some questions about file-system access and file versions within the
document model that is underlying the editor. (As first approximation one
would probably just use File.read and say it is "unmanaged" file-system
access, i.e. assuming you don't edit that file while working with the
Prover IDE.)


Makarius