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

Dear Makarius,

in the attached file you can find a simple example of a list of lists
representing a 250 * 250 matrix, which takes really long time to be
processed in Isabelle 2013 (also in the repository version); actually,
I gave up after a few minutes of processing without success.

We are using these kind of lists, usually with every list wrapped with
the IArray type constructor
( in
order to use IArrays to implement vectors and matrices.

Using ML definitions of this size or even greater takes almost no
time, so as an alternative solution we are directly executing the ML
code and definitions.

Thanks for any hint,


On Tue, May 21, 2013 at 3:29 PM, Makarius <makarius at> wrote:
> 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 and say it is "unmanaged" file-system
> access, i.e. assuming you don't edit that file while working with the Prover
> IDE.)
>         Makarius

Attachment: Random_Binary_Matrix.thy
Description: Binary data

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