.
(The original publication will be available at www.springerlink.com.)
.
(The original publication will be available at www.springerlink.com.)
Categoric.*: Semigroupoids, categories, ordered
categories with converse (OCCs), allegories, collagories, domain,
residuals, restricted residuals, division allegories.
Relation.Binary.Heterogeneous.*: Heterogeneous binary
relations, similar to
AoPA,
but universe-polymorphic and using standard library material where appropriate.
Data.Algebra.*: One view of parts of universal algebra.
It is strongly recommended to set a fixed heap for the Agda process, running, for example:
time agda +RTS -K64M -S -M12G -H12G -RTS -i . -i /var/tmp/AGDA/lib-0.5/src SomeTheory.lagda(The “
-K64M” flag increases also the stack size,
which is necessary for typechecking some of the theories.
“-S” prints run-time garbage collection and heap usage information.)
.agdai files, which are already compressed)
This is to be unpacked in the same place as RATH-Agda-1.0.tar.gz:
tar xzf ~/Downloads/RATH-Agda-1.0.tar.gz tar xf ~/Downloads/RATH-Agda-1.0_agdai.tarFor Agda-2.2.10, the
.agdai files need to be more
recent than the corresponding source files, otherwise it will
typecheck again.
In particular the theories in Data.Algebra.Generalised
require large working memory.
I would not expect to be able to typecheck all of them (even in
individual Agda runs) with less than 3GB heap space;
most recently the the smallest heap I tried (successfully) was 6GB.