[Agda] Failure when importing stdlib file

[Chantal KELLER]

Nils Anders Danielsson a écrit :
> 
> On 2009-09-09 10:21, Chantal KELLER wrote:
>> Perhaps I am mistaking, but this is very weird that you have to be able
>> to write in the directories where the stdlib files are. Shouldn't they
>> be compiled once for all when installing?
> 
> The standard library is not yet packaged for Debian, as far as I am
> aware. When it is I assume that the interface files will be precompiled.

There is a package called "agda-stdlib", which installs the standard
library in /usr/share/agda-stdlib. But it seems to be experimental and
out of date (see "[Agda] Error in stdlib Relation/Binary/Core.agda").
-- 
Chantal KELLER