Re: [isabelle] Abbreviation makes Isabelle/HOL very slow
The problem, of course, is that abbreviations are unfolded for term
parsing and folded for term printing. Unfolding these simple
abbreviations is no problem. But abbreviations as general as these could
be folded anywhere, making it impossible to print.
I think you might want to try abbreviation(input) rather than
abbreviation. You can define any of these abbreviations safely for input.
That will allow you to type "flip" wherever you like, but it will
disappear in output.
In general, I find abbreviation(input) a very useful mechanism, and I
use it by default rather than abbreviation.
On 24/08/16 00:00, Giuliano Losa wrote:
in the following theory, the processing of the definition of x2 takes
minutes on my machine.
abbreviation x1 where "x1 f â f"
definition x2 where "x2 â x"
If I remove the abbreviation, it becomes instantaneous.
I came across this problem because I made the following abbreviation:
abbreviation flip where "flip f â Î x y . f y x"
It rendered Isabelle unusable, as the processing of some commands (not
only definition, but also other commands) started to take minutes.
I fixed the problem by using a definition instead of an abbreviation,
but there might be something worth investigating going on here.
I observed this behavior using Isabelle-2016 and Isabelle_15-Aug-2016.
This archive was generated by a fusion of
Pipermail (Mailman edition) and