Re: [isabelle] Probelm with the "definition" command
- To: Jesus Aransay <jesus-maria.aransay at unirioja.es>
- Subject: Re: [isabelle] Probelm with the "definition" command
- From: Makarius <makarius at sketis.net>
- Date: Tue, 21 May 2013 15:29:07 +0200 (CEST)
- Cc: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- In-reply-to: <CAL0S8BfTvPkf+TFsG=DSFK0VaKj-SX6DHuCYBrNNPG1--c6g9Q@mail.gmail.com>
- References: <CAL0S8BfTvPkf+TFsG=DSFK0VaKj-SX6DHuCYBrNNPG1--c6g9Q@mail.gmail.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and