[Agda] running out of memory in formalization of category theory

[Nicolas Pouillard]

On Fri, 04 Jun 2010 13:49:53 +0100, Nils Anders Danielsson <nad at Cs.Nott.AC.UK> wrote:
> On 2010-06-04 02:28, Anton Setzer wrote:
> > Could it be that the poor performance of agda is due to the fact that
> > it always normalises two terms in order to compare whether they are
> > equal even if they are identical.
> 
> This hypothesis has been tested (on a very small sample of code). Only a
> small fraction of the equality tests were between equal terms, if I
> remember correctly.
> 
> > We sometimes proved those theorems, then postulated the proofs and
> > referred to the postulated proofs, just in order to avoid Agda
> > normalising the proofs.
> 
> You don't need to use postulates. Use abstract instead:
> 
>    abstract
> 
>      foo : Foo
>      foo = …
> 
>      bar : Bar
>      bar = …
> 
> Here foo and bar are transparent within the abstract block
> but opaque outside.

While abstract blocks improve type-checking time, AFAIK proofs do not get
GCed and then get serialized in .agdai files.

Throwing away these terms using an option may allow to significantly reduce
the memory needed to type-check big developments.

> (within all
> abstract blocks in the same module, I believe ①),

> ① I don't know how abstract blocks in submodules are treated.

This seems counter intuitive. I makes more sense and would fit nicely with
submodules to have each abstract block independent.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr