These theories are intended as interfaces for high-level programming; this current collection includes implementations in particular using concrete relations, and a number of constructions, including quotients by (abstractions of) partial equivalence relations.
RATH-Agda-2.0.* should work with Agda development versions of December 2013 and later, and corresponding versions of the standard library.
When working with RATH-Agda, it is strongly recommended to set a fixed heap for the Agda process, running, for example:
time agda +RTS -K64M -S -M6G -H6G -RTS -i . -i $STDLIB 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.)
.agdaifiles, which are already compressed)
This is to be unpacked from the same place as RATH-Agda-2.0.0.tar.gz
This builds on RATH-Agda-2.0.1.
MonCoAlg-0.1 can be checked from source without first checking all of RATH-Agda-2.0.1, using the following commands in the otherwise empty download directory:
$ STDLIB=YourInstallationDirectoryOfTheAgdaStdLibrary/src $ tar xzf RATH-Agda-2.0.1.tar.gz $ tar xzf MonCoAlg-0.1.tar.gz $ cd MonCoAlg-0.1/ $ time agda +RTS -H11G -M11G -K128M -RTS -i . -i ../RATH-Agda-2.0.1 -i $STDLIB MonCoAlg0All.lagdaThis will not work with much less than 10GB of heap. (Without contention for RAM, this may take around 40 minutes.)
recordassembly not yet checked by Agda; requires more than 52GB heap.)
This development works with the current stable version of Agda, i.e., 18.104.22.168, and a matching version of the Agda standard library.
It also works with Agda development versions at least of mid-July 2015.
(With these, in particular using
typechecking this development is much faster.)
On my machine, checking this whole development via the entry
AContext2.lagda from scratch using the development version of Agda
requires at least 8GB of heap, and takes about 14 minutes.
Using Agda-22.214.171.124 requires at least 10GB of heap, and takes about 27 minutes.
A first exploration of formalising the way contexts give rise to concept lattices in formal concept analysis (FCA).
This builds on RATH-Agda-2.0.0 and will also work with RATH-Agda-2.0.1.
AContext-1.0 can be checked from source without first checking all of RATH-Agda-2.0.0, using the following commands in the otherwise empty download directory:
$ STDLIB=YourInstallationDirectoryOfTheAgdaStdLibrary/src $ tar xzf RATH-Agda-2.0.0.tar.gz $ tar xzf AContext-1.0.tar.gz $ cd AContext-1.0/ $ time agda +RTS -H2G -M2G -K64M -RTS -i . -i ../RATH-Agda-2.0.0 -i $STDLIB Data/AContext/Category.lagda