[Agda] Devel: How to get back normalisation instead of simplification?

Wolfram Kahl kahl at cas.mcmaster.ca
Mon Jul 1 18:59:36 CEST 2013

On Sun, Jun 23, 2013 at 10:28:50PM -0400, Wolfram Kahl wrote:
> On Sat, Jun 22, 2013 at 08:27:20PM +0200, Andreas Abel wrote:
> > if you have some large terms in you developments and have not pulled 
> > Agda recently, it might be worth trying.  I have implemented some 
> > performance improvements that are probably noticeable if you use records 
> > a lot.  The relevant patches concern "issue 854".
> > 
> > James reported a reduction of memory consumption from 12GB to 3GB for 
> > one of his developments.
> > 
> > In case you see similar improvements, please reply to this message.
> Wonderful!

... so I switched to the current development version.

But now the following gets in the way:

 | Mon May 20 06:33:15 EDT 2013  Andreas Abel <andreas.abel at ifi.lmu.de>
 |   * Switched to simplification (instead of normalisation) in emacs interaction.
 |   This is for experimentation purposes.
 |   Key-bindings for full normalisation should also be added.

Since there is already a distinction achieved via C-u
in the display of goals and context (see
), perhaps it would be natural to expand on that,
making that distinction ternary instead of the current binary,
by adding simplified version via a special C-u prefix?

(In Emacs , C-u in general serves to pass a |just| argument of type
 |Maybe Integer| to the following command;
 just C-u without a numeric argument seems to pass |just 4|).

Otherwise, is there a simple way to switch back to full normalisation
as one of the options?


More information about the Agda mailing list