如何在NixOS上编译Agda Hello World程序？

问题 #

在NixOS系统中尝试编译Agda官方文档的Hello World示例，工作目录包含以下文件：

1. hello-world.agda #

module hello-world where

open import IO

main = run (putStrLn "Hello, World!")

2. shell.nix #

{ pkgs ? import <nixpkgs> { } }:
with pkgs;
mkShell {
  buildInputs = [
    (agda.withPackages (ps: [
      ps.standard-library
    ]))
  ];
}

执行nix-shell shell.nix进入环境后，运行agda --compile hello-world.agda时出现错误：

$ agda --compile hello-world.agda
Checking hello-world (/home/matthew/backup/projects/agda-math/hello-world.agda).
/home/matthew/backup/projects/agda-math/hello-world.agda:3,1-15
Failed to find source of module IO in any of the following
locations:
  /home/matthew/backup/projects/agda-math/IO.agda
  /home/matthew/backup/projects/agda-math/IO.lagda
  /nix/store/7pg293b76ppv2rw2saf5lcbckn6kdy7z-Agda-2.6.2.2-data/share/ghc-9.0.2/x86_64-linux-ghc-9.0.2/Agda-2.6.2.2/lib/prim/IO.agda
  /nix/store/7pg293b76ppv2rw2saf5lcbckn6kdy7z-Agda-2.6.2.2-data/share/ghc-9.0.2/x86_64-linux-ghc-9.0.2/Agda-2.6.2.2/lib/prim/IO.lagda
when scope checking the declaration
  open import IO

已通过nix-shell引入standard-library，但系统仍找不到IO模块，求问题原因及解决办法。

原因分析 #

1. 版本差异：当前使用的Agda版本是2.6.2.2，但参考的文档对应2.6.0.1。标准库在新版本中调整了模块结构，顶层IO模块不再直接可用，需要导入其下属的子模块。
2. 库路径识别问题：尽管通过agda.withPackages添加了标准库，Agda可能未自动识别到库的位置，需要显式配置库依赖或路径。

解决办法 #

1. 修正模块导入路径（适配新版本） #

将hello-world.agda中的导入语句修改为适配当前标准库版本的写法：

module hello-world where

open import IO.Base
open import Data.String.Base

main = run (putStrLn "Hello, World!")

如果仍有问题，可以尝试导入Agda.Builtin.IO配合字符串模块，但优先使用标准库的IO.Base。

2. 添加.agda-lib配置文件 #

在工作目录创建hello-world.agda-lib文件，内容如下：

name: hello-world
depend: standard-library

Agda会自动读取该文件，识别依赖的标准库，无需手动指定路径。

3. 编译时显式指定库路径 #

在nix-shell中先查看标准库路径：

echo $AGDA_STDLIB

然后编译时加上路径参数：

agda --compile -i $(echo $AGDA_STDLIB)/src hello-world.agda

4. 锁定Agda版本与文档一致 #

修改shell.nix，指定使用Agda 2.6.0.1版本，确保和文档版本匹配：

{ pkgs ? import <nixpkgs> { } }:
with pkgs;
mkShell {
  buildInputs = [
    (agda.withPackages (ps: [
      ps.standard-library
    ])).overrideAttrs (old: {
      version = "2.6.0.1";
      src = fetchFromGitHub {
        owner = "agda";
        repo = "agda";
        rev = "v2.6.0.1";
        sha256 = "0xq0z6y4x4y9z8w7v6u5t4s3r2q1p0o9i8u7y6t5r4e3w2q1a0";
      };
    })
  ];
}

注意：需要替换sha256为正确值，可通过nix-prefetch-url --unpack https://github.com/agda/agda/archive/v2.6.0.1.tar.gz获取。

内容的提问来源于stack exchange，提问作者mherzl