Ubuntu下Agda标准库配置缺失standard-library.agda-lib的问题咨询

Hey there, let's get your Agda standard library up and running properly. The issue you're facing is pretty common with the Ubuntu package version of agda-stdlib—it often doesn't include the required standard-library.agda-lib file out of the box. Here's how to fix it step by step:

Step 1: Locate the exact installation path of your stdlib #

First, let's confirm where Ubuntu installed the standard library files. Run this command in your terminal:

dpkg -L agda-stdlib

This will list all files installed by the package. Look for the directory that contains folders like Algebra, Data, and Relation—that's the root directory of your stdlib (it's usually something like /usr/share/agda-stdlib/ or /usr/lib/agda/std-lib/).

Step 2: Create the missing standard-library.agda-lib file #

Navigate to that stdlib root directory (you'll need sudo permissions to write here):

cd /path/to/your/stdlib/root
sudo nano standard-library.agda-lib

Paste the following content into the file:

name: standard-library
include: .

Save and exit the editor (in nano, that's Ctrl+O, then Enter, then Ctrl+X).

Step 3: Tell Agda where to find the library #

Now we need to configure Agda to recognize this library. First, make sure the ~/.agda directory exists (create it if not):

mkdir -p ~/.agda

Option A: Add the library to your global config #

Edit the libraries file in ~/.agda (create it if it doesn't exist):

nano ~/.agda/libraries

Add a line with the full path to the standard-library.agda-lib file you just created, like:

/usr/share/agda-stdlib/standard-library.agda-lib

Option B: Set the stdlib as a default library (optional) #

If you want to use the standard library in all your Agda files without adding a header option every time, edit the defaults file in ~/.agda:

nano ~/.agda/defaults

Add a line that says:

standard-library

Step 4: Verify the configuration works #

Create a simple test file called Test.agda with this content:

{-# OPTIONS --library standard-library #-}
open import Data.Nat
open import IO

main : IO Unit
main = print 42

Compile it with:

agda Test.agda

If everything works, you won't get any import errors—success!

Why this happens #

The Ubuntu agda-stdlib package is often a bit outdated compared to the latest Agda documentation, and sometimes the packagers forget to include the .agda-lib file that Agda's package system needs to recognize the library. Manually creating this file and pointing Agda to it fixes the gap.

内容的提问来源于stack exchange，提问作者J.Lili