[Agda] 5 sec performance gain on std-lib

Andreas Abel andreas.abel at ifi.lmu.de
Fri Oct 19 13:32:42 CEST 2012


Hi folks,

it seems that I have won 5 seconds on the library-test by some seemingly 
irrelevant optimizations in the termination checker.  Can someone verify?

Patch is upstream:

Fri Oct 19 09:36:45 CEST 2012  Andreas Abel <andreas.abel at ifi.lmu.de>
   * Some refactoring in the comparison of call arguments to formal 
parameters.
   Do not cut off order relations at this phase.

If that is the case, some more fumbling with the termination checker 
could pay off.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/


More information about the Agda mailing list