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



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




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