*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] WG:AW: Abbreviation makes Isabelle/HOL very slow*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 23 Aug 2016 16:32:11 +0200

-------- Originalnachricht --------

Betreff: AW:[isabelle] Abbreviation makes Isabelle/HOL very slow

Von: Peter Lammich

An: Giuliano Losa

Cc:

Hi,

In the first example, it tries to fold the abbreviation infinitely often on pretty printing. In the second example, it's also infinite folding, as higher-order unification is very creative at finding unexpected unifiers if you have function variables

Peter

-------- Originalnachricht --------

Betreff: [isabelle] Abbreviation makes Isabelle/HOL very slow

Von: Giuliano Losa

An: isabelle-users at cl.cam.ac.uk

Cc:Hello,

in the following theory, the processing of the definition of x2 takes

minutes on my machine.

theory Test

imports Main

begin

abbreviation x1 where "x1 f â f"

definition x2 where "x2 â x"

end

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.

Giuliano

- Previous by Date: [isabelle] Abbreviation makes Isabelle/HOL very slow
- Next by Date: Re: [isabelle] Abbreviation makes Isabelle/HOL very slow
- Previous by Thread: Re: [isabelle] Abbreviation makes Isabelle/HOL very slow
- Next by Thread: [isabelle] New AFP entry: Simple Firewall
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list