How do I download and set up the standard library for Agda in Ubuntu?

Question

I have installed and been able to use Agda on my Ubuntu system via the emacs editor, and all seems good so far.

However, I am unable to install and set up the standard library for it.

Following this: https://agda.readthedocs.io/en/v2.6.1/getting-started/installation.html I have tried

apt-get install agda-stdlib

which worked, but then I tried following this: https://agda.readthedocs.io/en/latest/tools/package-system.html and the directory where apt-get seemed to install agda-stdlib does not contain a library file standard-library.agda-lib, only the following

Algebra Function IO.agda Relation Algebra.agda Function.agda IO.agdai Size.agda Algebra.agdai Function.agdai Level.agda Size.agdai Category index.agda Level.agdai Strict.agda Coinduction.agda Induction Record.agda Strict.agdai Coinduction.agdai Induction.agda Record.agdai Universe.agda Data Induction.agdai Reflection.agda Universe.agdai Foreign IO Reflection.agdai

What am I missing and how should I proceed?

Noguchi

What version of Ubuntu are you on? What is the output of agda --version? – Penetrance

I am using Ubuntu 18.04.2 and the Agda version 2.6.1. – Noguchi

Answer 1

The versions of both Agda and the standard library in the Ubuntu package manager are quite outdated. So you should not mix a version of Agda installed via Cabal or Stack with a version of the standard library installed via Ubuntu's package manager. Instead, you can find the right version of the standard library for your version of Agda on https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. Specifically, for Agda 2.6.1 you need the standard library version 1.3, which you can install from Github:

git clone https://github.com/agda/agda-stdlib.git
git checkout tags/v1.3

and then follow the instructions at https://agda.readthedocs.io/en/latest/tools/package-system.html to make sure Agda can find the installation.

Penetrance

Thank you, there was indeed a problem with the package from the ubuntu package manager. Installing according to this github.com/agda/agda-stdlib/blob/master/notes/… seemed to have solved the issue. – Noguchi

That doesn't answer the question about the missing standard-library.agda-lib file in the ubuntu package. Is that package broken? – Overgrowth