Agda: `agda compile hello-world-dep.agda` won't find installed standard-library `Failed to find source of module Data.Nat in any of the following`

starlit · December 17, 2024, 1:03pm

Agda: agda compile hello-world-dep.agda (GHC backend) won’t find installed standard-library Failed to find source of module Data.Nat in any of the following

module hello-world-dep where

open import Data.Nat using (ℕ; zero; suc)

data Vec (A : Set) : ℕ → Set where
  []   : Vec A zero
  _::_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infixr 5 _::_

REFERENCE: A Taste of Agda — Agda 2.7.0.1 documentation

OBSERVED BEHAVIOR

I have agda.wikiPackages installed with home-manager

home-manager.users.starlit = {
  home.packages = [
    (pkgs.agdaPackages.agda.withPackages (ps: [
      ps.standard-library
      ps.agda-categories
    ]))
  ];
};

which agda | tree $'(dirname (dirname $"(readlink --canonicalize ...$in.path)"))'
/nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1
└── bin
    ├── agda
    └── agda-mode -> /nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin/bin/agda-mode

BUT when I try to

agda --compile /home/starlit/dev/agda/taste/hello-world-dep.agda
Checking hello-world-dep (/home/starlit/dev/agda/taste/hello-world-dep.agda).
/home/starlit/dev/agda/taste/hello-world-dep.agda:9,1-42
Failed to find source of module Data.Nat in any of the following
locations:
  /home/starlit/dev/agda/taste/Data/Nat.agda
  /home/starlit/dev/agda/taste/Data/Nat.lagda
  /nix/store/p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/Agda-2.7.0.1/lib/prim/Data/Nat.agda
  /nix/store/p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/Agda-2.7.0.1/lib/prim/Data/Nat.lagda
when scope checking the declaration
  open import Data.Nat using (ℕ; zero; suc)

/nix/store/HASH-Agda-2.7.0.1-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/Agda-2.7.0.1/lib/prim DOESN’T have Agda standard-library, only Agda built-in.

tree /nix/store/p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/Agda-2.7.0.1/lib/prim
/nix/store/p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/Agda-2.7.0.1/lib/prim
├── Agda
│   ├── Builtin
│   │   ├── Bool.agda
│   │   ├── Char
│   │   │   └── Properties.agda
│   │   ├── Char.agda
│   │   ├── Coinduction.agda
│   │   ├── Cubical
│   │   │   ├── Equiv.agda
│   │   │   ├── Glue.agda
│   │   │   ├── HCompU.agda
│   │   │   ├── Id.agda
│   │   │   ├── Path.agda
│   │   │   └── Sub.agda
│   │   ├── Equality
│   │   │   ├── Erase.agda
│   │   │   └── Rewrite.agda
│   │   ├── Equality.agda
│   │   ├── Float
│   │   │   └── Properties.agda
│   │   ├── Float.agda
│   │   ├── FromNat.agda
│   │   ├── FromNeg.agda
│   │   ├── FromString.agda
│   │   ├── Int.agda
│   │   ├── IO.agda
│   │   ├── List.agda
│   │   ├── Maybe.agda
│   │   ├── Nat.agda
│   │   ├── Reflection
│   │   │   ├── External.agda
│   │   │   └── Properties.agda
│   │   ├── Reflection.agda
│   │   ├── Sigma.agda
│   │   ├── Size.agda
│   │   ├── Strict.agda
│   │   ├── String
│   │   │   └── Properties.agda
│   │   ├── String.agda
│   │   ├── TrustMe.agda
│   │   ├── Unit.agda
│   │   ├── Word
│   │   │   └── Properties.agda
│   │   └── Word.agda
│   ├── Primitive
│   │   └── Cubical.agda
│   └── Primitive.agda
├── agda-builtins.agda-lib
└── _build
    └── 2.7.0.1
        └── agda
            └── Agda
                ├── Builtin
                │   ├── Bool.agdai
                │   ├── Char
                │   │   └── Properties.agdai
                │   ├── Char.agdai
                │   ├── Coinduction.agdai
                │   ├── Cubical
                │   │   ├── Equiv.agdai
                │   │   ├── Glue.agdai
                │   │   ├── HCompU.agdai
                │   │   ├── Id.agdai
                │   │   ├── Path.agdai
                │   │   └── Sub.agdai
                │   ├── Equality
                │   │   ├── Erase.agdai
                │   │   └── Rewrite.agdai
                │   ├── Equality.agdai
                │   ├── Float
                │   │   └── Properties.agdai
                │   ├── Float.agdai
                │   ├── FromNat.agdai
                │   ├── FromNeg.agdai
                │   ├── FromString.agdai
                │   ├── Int.agdai
                │   ├── IO.agdai
                │   ├── List.agdai
                │   ├── Maybe.agdai
                │   ├── Nat.agdai
                │   ├── Reflection
                │   │   ├── External.agdai
                │   │   └── Properties.agdai
                │   ├── Reflection.agdai
                │   ├── Sigma.agdai
                │   ├── Size.agdai
                │   ├── Strict.agdai
                │   ├── String
                │   │   └── Properties.agdai
                │   ├── String.agdai
                │   ├── TrustMe.agdai
                │   ├── Unit.agdai
                │   ├── Word
                │   │   └── Properties.agdai
                │   └── Word.agdai
                ├── Primitive
                │   └── Cubical.agdai
                └── Primitive.agdai

EXPECTED BEHAVIOR

Agda finds standard-library with its modules such as Data on /nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1, see below.

BUT I have standard-library with Data, etc

nix-store --query --tree /nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1
/nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1
...
├───/nix/store/q7sqq18llwqsm7sqk6xpj377q440lyzj-libraries
│   ├───/nix/store/ixbhr7shi2l3k4bh20c43w1vmx2gvdgv-agda-categories-0.2.0
│   └───/nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1
...

ls -1 /nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/src/Data/
AVL
AVL.agda
Bool
Bool.agda
Bytestring
Char
Char.agda
Container
Container.agda
Default.agda
DifferenceList.agda
DifferenceNat.agda
DifferenceVec.agda
Digit
Digit.agda
Empty
Empty.agda
Erased.agda
Fin
Fin.agda
Float
Float.agda
Graph
Integer
Integer.agda
Irrelevant.agda
List
List.agda
Maybe
Maybe.agda
Nat
Nat.agda
Parity
Parity.agda
Product
Product.agda
Rational
Rational.agda
Record.agda
Refinement
Refinement.agda
Sign
Sign.agda
Star
String
String.agda
Sum
Sum.agda
These
These.agda
Tree
Trie
Trie.agda
Unit
Unit.agda
Universe
Universe.agda
Vec
Vec.agda
W
W.agda
Word
Word64
Word64.agda
Word8
Word.agda
Wrap.agda

ls -1 /nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/_build/2.7.0.1/agda/src/Data/
AVL
AVL.agdai
Bool
Bool.agdai
Bytestring
Char
Char.agdai
Container
Container.agdai
Default.agdai
DifferenceList.agdai
DifferenceNat.agdai
DifferenceVec.agdai
Digit
Digit.agdai
Empty
Empty.agdai
Erased.agdai
Fin
Fin.agdai
Float
Float.agdai
Graph
Integer
Integer.agdai
Irrelevant.agdai
List
List.agdai
Maybe
Maybe.agdai
Nat
Nat.agdai
Parity
Parity.agdai
Product
Product.agdai
Rational
Rational.agdai
Record.agdai
Refinement
Refinement.agdai
Sign
Sign.agdai
Star
String
String.agdai
Sum
Sum.agdai
These
These.agdai
Tree
Trie
Trie.agdai
Unit
Unit.agdai
Universe
Universe.agdai
Vec
Vec.agdai
W
W.agdai
Word
Word64
Word64.agdai
Word8
Word.agdai
Wrap.agdai

FULL output

nix-store --query --tree /nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1
/nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1
├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37
│   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36
│   │   ├───/nix/store/2d5spnl8j5r4n1s4bj1zmra7mwx0f1n8-xgcc-13.3.0-libgcc
│   │   ├───/nix/store/qwjjm4j652ck9izaid7bz63s4hd5bnha-libidn2-2.3.7
│   │   │   ├───/nix/store/6pqgj71r0850b0cd95yxx0d52zax016i-libunistring-1.2
│   │   │   │   └───/nix/store/6pqgj71r0850b0cd95yxx0d52zax016i-libunistring-1.2 [...]
│   │   │   └───/nix/store/qwjjm4j652ck9izaid7bz63s4hd5bnha-libidn2-2.3.7 [...]
│   │   └───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   └───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
├───/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages
│   ├───/nix/store/0d4h5nnbliwpqa5hcmq0lad6r2xfbpii-libffi-3.4.6
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   └───/nix/store/0d4h5nnbliwpqa5hcmq0lad6r2xfbpii-libffi-3.4.6 [...]
│   ├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib
│   │   ├───/nix/store/nhdjqagplar2fdrqnrxlab8vg9i36b3d-gcc-13.3.0-libgcc
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   └───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   └───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
│   ├───/nix/store/2hkazldwalm0k3hf2wh1knw1s66wlrvp-gmp-with-cxx-6.3.0-dev
│   │   ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
│   │   └───/nix/store/2hkazldwalm0k3hf2wh1knw1s66wlrvp-gmp-with-cxx-6.3.0-dev [...]
│   ├───/nix/store/7vs39d9phfvq4a95ydmq3zkpf518wlmb-libffi-3.4.6-dev
│   │   ├───/nix/store/0d4h5nnbliwpqa5hcmq0lad6r2xfbpii-libffi-3.4.6 [...]
│   │   └───/nix/store/7vs39d9phfvq4a95ydmq3zkpf518wlmb-libffi-3.4.6-dev [...]
│   ├───/nix/store/8s7f5jgn8bbvj552hb5glsgwfx881kfy-ncurses-6.4.20221231
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   └───/nix/store/8s7f5jgn8bbvj552hb5glsgwfx881kfy-ncurses-6.4.20221231 [...]
│   ├───/nix/store/mns770di6nbh52gq0nx07mmc422gm8fc-elfutils-0.191
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   ├───/nix/store/6avf0gmd2sl573bv6qhsqybgvf86wdq5-zstd-1.5.6
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   │   └───/nix/store/6avf0gmd2sl573bv6qhsqybgvf86wdq5-zstd-1.5.6 [...]
│   │   ├───/nix/store/g242a6wyvc429wlwp59iqyhpnjfcrkw3-bzip2-1.0.8
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   └───/nix/store/g242a6wyvc429wlwp59iqyhpnjfcrkw3-bzip2-1.0.8 [...]
│   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1
│   │   │   └───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   ├───/nix/store/lz8snrzdzwkcbdjccqxd2r4f792cnwsg-curl-8.11.0
│   │   │   ├───/nix/store/qwjjm4j652ck9izaid7bz63s4hd5bnha-libidn2-2.3.7 [...]
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   ├───/nix/store/5dlhinba4wbr5ijy0vcmyzh4i678z94w-openssl-3.3.2
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   └───/nix/store/5dlhinba4wbr5ijy0vcmyzh4i678z94w-openssl-3.3.2 [...]
│   │   │   ├───/nix/store/6avf0gmd2sl573bv6qhsqybgvf86wdq5-zstd-1.5.6 [...]
│   │   │   ├───/nix/store/78ndygrdpr8ghk256wm2g89v10gkk1ar-brotli-1.1.0-lib
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   └───/nix/store/78ndygrdpr8ghk256wm2g89v10gkk1ar-brotli-1.1.0-lib [...]
│   │   │   ├───/nix/store/ihn8kbc2bgqk780i3n74x98plsnfzfd6-libpsl-0.21.5
│   │   │   │   ├───/nix/store/6pqgj71r0850b0cd95yxx0d52zax016i-libunistring-1.2 [...]
│   │   │   │   ├───/nix/store/jcgrdvv9cc1b3r72zp4cq3vb3pka8wx4-publicsuffix-list-0-unstable-2024-10-25
│   │   │   │   ├───/nix/store/qwjjm4j652ck9izaid7bz63s4hd5bnha-libidn2-2.3.7 [...]
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   └───/nix/store/ihn8kbc2bgqk780i3n74x98plsnfzfd6-libpsl-0.21.5 [...]
│   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   ├───/nix/store/j391qgmh574rdjh89jl0bi5aw9nxglia-libssh2-1.11.1
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/5dlhinba4wbr5ijy0vcmyzh4i678z94w-openssl-3.3.2 [...]
│   │   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   │   └───/nix/store/j391qgmh574rdjh89jl0bi5aw9nxglia-libssh2-1.11.1 [...]
│   │   │   ├───/nix/store/pgkfyjsy4g3jm6sxp7m0ivfpnv59j7p6-nghttp2-1.64.0-lib
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   └───/nix/store/pgkfyjsy4g3jm6sxp7m0ivfpnv59j7p6-nghttp2-1.64.0-lib [...]
│   │   │   ├───/nix/store/xghyamhbjj0rfavxj76l52mv7zr7dfiw-krb5-1.21.3-lib
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   │   │   │   ├───/nix/store/5dlhinba4wbr5ijy0vcmyzh4i678z94w-openssl-3.3.2 [...]
│   │   │   │   ├───/nix/store/rlmyizjw96rfpi544511lqbsdqdjsrcb-keyutils-1.6.3-lib
│   │   │   │   │   └───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   └───/nix/store/xghyamhbjj0rfavxj76l52mv7zr7dfiw-krb5-1.21.3-lib [...]
│   │   │   └───/nix/store/lz8snrzdzwkcbdjccqxd2r4f792cnwsg-curl-8.11.0 [...]
│   │   ├───/nix/store/mmbcivd56qqijk877x2i5ra55sbbcmrl-xz-5.6.3
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   └───/nix/store/mmbcivd56qqijk877x2i5ra55sbbcmrl-xz-5.6.3 [...]
│   │   └───/nix/store/mns770di6nbh52gq0nx07mmc422gm8fc-elfutils-0.191 [...]
│   ├───/nix/store/c3mgiawvdsf0vp336z7qybx04i6hx8dh-elfutils-0.191-dev
│   │   ├───/nix/store/i73yxhp1mq2f7a2rm792l0spmm0wsmqb-setup-debug-info-dirs-hook
│   │   ├───/nix/store/mns770di6nbh52gq0nx07mmc422gm8fc-elfutils-0.191 [...]
│   │   ├───/nix/store/kahv64cppdy0jskvpvzvhv1pffma3pkr-elfutils-0.191-bin
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   ├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   │   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   │   ├───/nix/store/ck3rjhfyxwbi84cwzm0ckqjc37sxijq8-libmicrohttpd-1.0.1
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/jc4hlry02rgfqms75hf8kzqnf6hp3nz1-gnutls-3.8.6
│   │   │   │   │   ├───/nix/store/6pqgj71r0850b0cd95yxx0d52zax016i-libunistring-1.2 [...]
│   │   │   │   │   ├───/nix/store/qwjjm4j652ck9izaid7bz63s4hd5bnha-libidn2-2.3.7 [...]
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   │   │   │   ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
│   │   │   │   │   ├───/nix/store/h7qbizpkwfv1vb4r0hzm3b74jrfmgfqf-nettle-3.10
│   │   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   │   ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
│   │   │   │   │   │   └───/nix/store/h7qbizpkwfv1vb4r0hzm3b74jrfmgfqf-nettle-3.10 [...]
│   │   │   │   │   ├───/nix/store/ixip8d2kh46q5rpjkzlxj7sqq9amjv6k-dns-root-data-2024-06-20
│   │   │   │   │   ├───/nix/store/lszlcr0lhi7p784c8wrh7iabfixyjcdn-unbound-1.21.1-lib
│   │   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   │   ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
│   │   │   │   │   │   ├───/nix/store/h7qbizpkwfv1vb4r0hzm3b74jrfmgfqf-nettle-3.10 [...]
│   │   │   │   │   │   ├───/nix/store/jmwibaq22mdf1maarn008qrrjnbi2sgr-libevent-2.1.12
│   │   │   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   │   │   └───/nix/store/jmwibaq22mdf1maarn008qrrjnbi2sgr-libevent-2.1.12 [...]
│   │   │   │   │   │   └───/nix/store/lszlcr0lhi7p784c8wrh7iabfixyjcdn-unbound-1.21.1-lib [...]
│   │   │   │   │   ├───/nix/store/xa0j95gv6a29g62cichnby52d79az6cv-libtasn1-4.19.0
│   │   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   │   └───/nix/store/xa0j95gv6a29g62cichnby52d79az6cv-libtasn1-4.19.0 [...]
│   │   │   │   │   ├───/nix/store/r6n7prsa8khgfj2g54406w2wcp5gdx6y-p11-kit-0.25.5
│   │   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   │   ├───/nix/store/0d4h5nnbliwpqa5hcmq0lad6r2xfbpii-libffi-3.4.6 [...]
│   │   │   │   │   │   ├───/nix/store/xa0j95gv6a29g62cichnby52d79az6cv-libtasn1-4.19.0 [...]
│   │   │   │   │   │   └───/nix/store/r6n7prsa8khgfj2g54406w2wcp5gdx6y-p11-kit-0.25.5 [...]
│   │   │   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   │   │   └───/nix/store/jc4hlry02rgfqms75hf8kzqnf6hp3nz1-gnutls-3.8.6 [...]
│   │   │   │   └───/nix/store/ck3rjhfyxwbi84cwzm0ckqjc37sxijq8-libmicrohttpd-1.0.1 [...]
│   │   │   ├───/nix/store/fnjlamc0x1hx245px1s3rbazxfngffi0-libarchive-3.7.7-lib
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/067800yh33y5m156i6rhmzhsn8wxbbnh-libxml2-2.13.4
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   └───/nix/store/067800yh33y5m156i6rhmzhsn8wxbbnh-libxml2-2.13.4 [...]
│   │   │   │   ├───/nix/store/5dlhinba4wbr5ijy0vcmyzh4i678z94w-openssl-3.3.2 [...]
│   │   │   │   ├───/nix/store/5z4ghjjxyg0r33w0hfr4crhlz6fqfzd2-acl-2.3.2
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   ├───/nix/store/vzh3vvwcj1pma09dgial605zkb0qh7gl-attr-2.5.2
│   │   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   │   └───/nix/store/vzh3vvwcj1pma09dgial605zkb0qh7gl-attr-2.5.2 [...]
│   │   │   │   │   └───/nix/store/5z4ghjjxyg0r33w0hfr4crhlz6fqfzd2-acl-2.3.2 [...]
│   │   │   │   ├───/nix/store/6avf0gmd2sl573bv6qhsqybgvf86wdq5-zstd-1.5.6 [...]
│   │   │   │   ├───/nix/store/g242a6wyvc429wlwp59iqyhpnjfcrkw3-bzip2-1.0.8 [...]
│   │   │   │   ├───/nix/store/mmbcivd56qqijk877x2i5ra55sbbcmrl-xz-5.6.3 [...]
│   │   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   │   └───/nix/store/fnjlamc0x1hx245px1s3rbazxfngffi0-libarchive-3.7.7-lib [...]
│   │   │   ├───/nix/store/mns770di6nbh52gq0nx07mmc422gm8fc-elfutils-0.191 [...]
│   │   │   ├───/nix/store/yjm4j9n85bcp42v5nkz2xifrp4a9s63k-sqlite-3.46.1
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   │   └───/nix/store/yjm4j9n85bcp42v5nkz2xifrp4a9s63k-sqlite-3.46.1 [...]
│   │   │   └───/nix/store/kahv64cppdy0jskvpvzvhv1pffma3pkr-elfutils-0.191-bin [...]
│   │   └───/nix/store/c3mgiawvdsf0vp336z7qybx04i6hx8dh-elfutils-0.191-dev [...]
│   ├───/nix/store/hh783czjqlddq96zxhzijcqv92rb132r-ghc-9.6.6-doc
│   │   └───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   ├───/nix/store/inpspwqhgpld2zdk89hra7xjh3nxll2x-ncurses-6.4.20221231-dev
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   ├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   │   ├───/nix/store/8s7f5jgn8bbvj552hb5glsgwfx881kfy-ncurses-6.4.20221231 [...]
│   │   ├───/nix/store/cnpph76j4bim61hddgqjv485rwxfn39g-ncurses-6.4.20221231-man
│   │   └───/nix/store/inpspwqhgpld2zdk89hra7xjh3nxll2x-ncurses-6.4.20221231-dev [...]
│   ├───/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   ├───/nix/store/0d4h5nnbliwpqa5hcmq0lad6r2xfbpii-libffi-3.4.6 [...]
│   │   ├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
│   │   ├───/nix/store/2hkazldwalm0k3hf2wh1knw1s66wlrvp-gmp-with-cxx-6.3.0-dev [...]
│   │   ├───/nix/store/aax0hx68i2ikhpf27hdm6a2a209d4s6p-glibc-2.40-36-dev
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   ├───/nix/store/26dy2y29fhissya64ygahwpidpvs3bm3-glibc-2.40-36-bin
│   │   │   │   ├───/nix/store/2d5spnl8j5r4n1s4bj1zmra7mwx0f1n8-xgcc-13.3.0-libgcc [...]
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   └───/nix/store/26dy2y29fhissya64ygahwpidpvs3bm3-glibc-2.40-36-bin [...]
│   │   │   └───/nix/store/dvsai0ym9czjl5mcsarcdwccb70615n4-linux-headers-6.10
│   │   ├───/nix/store/9bacph866qhmr2zfib1h49jixq5hhd01-binutils-wrapper-2.43.1
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   ├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   │   │   ├───/nix/store/26dy2y29fhissya64ygahwpidpvs3bm3-glibc-2.40-36-bin [...]
│   │   │   ├───/nix/store/aax0hx68i2ikhpf27hdm6a2a209d4s6p-glibc-2.40-36-dev [...]
│   │   │   ├───/nix/store/k48bha2fjqzarg52picsdfwlqx75aqbb-coreutils-9.5
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/vzh3vvwcj1pma09dgial605zkb0qh7gl-attr-2.5.2 [...]
│   │   │   │   ├───/nix/store/5z4ghjjxyg0r33w0hfr4crhlz6fqfzd2-acl-2.3.2 [...]
│   │   │   │   ├───/nix/store/d6wqw30y25ib5dkbbdp16frb1la6125w-gmp-with-cxx-6.3.0
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   │   │   │   └───/nix/store/d6wqw30y25ib5dkbbdp16frb1la6125w-gmp-with-cxx-6.3.0 [...]
│   │   │   │   └───/nix/store/k48bha2fjqzarg52picsdfwlqx75aqbb-coreutils-9.5 [...]
│   │   │   ├───/nix/store/swvs52wx5a5j9mv91mingbak5pn4h1i0-expand-response-params
│   │   │   │   └───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   ├───/nix/store/va7kw1i822h95im4jacci19v0cqajfyf-binutils-2.43.1
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   │   ├───/nix/store/mkgxzw8bdg0974njrhq29kgwmgk35wid-binutils-2.43.1-lib
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   │   │   └───/nix/store/mkgxzw8bdg0974njrhq29kgwmgk35wid-binutils-2.43.1-lib [...]
│   │   │   │   └───/nix/store/va7kw1i822h95im4jacci19v0cqajfyf-binutils-2.43.1 [...]
│   │   │   └───/nix/store/9bacph866qhmr2zfib1h49jixq5hhd01-binutils-wrapper-2.43.1 [...]
│   │   ├───/nix/store/3ix5h74n7ar9950vwzp4dxmil70pmx0k-gcc-wrapper-13.3.0
│   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   ├───/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37 [...]
│   │   │   ├───/nix/store/14aswfz6pm8zvyyy927xzmi8x4rnvlc8-gnugrep-3.11
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/xs9jwc3if4dp77ga0q9cjcspwp7r9yvf-pcre2-10.44
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   └───/nix/store/xs9jwc3if4dp77ga0q9cjcspwp7r9yvf-pcre2-10.44 [...]
│   │   │   │   └───/nix/store/14aswfz6pm8zvyyy927xzmi8x4rnvlc8-gnugrep-3.11 [...]
│   │   │   ├───/nix/store/26dy2y29fhissya64ygahwpidpvs3bm3-glibc-2.40-36-bin [...]
│   │   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   │   ├───/nix/store/aax0hx68i2ikhpf27hdm6a2a209d4s6p-glibc-2.40-36-dev [...]
│   │   │   ├───/nix/store/k48bha2fjqzarg52picsdfwlqx75aqbb-coreutils-9.5 [...]
│   │   │   ├───/nix/store/swvs52wx5a5j9mv91mingbak5pn4h1i0-expand-response-params [...]
│   │   │   ├───/nix/store/9bacph866qhmr2zfib1h49jixq5hhd01-binutils-wrapper-2.43.1 [...]
│   │   │   ├───/nix/store/xzfmarrq8x8s4ivpya24rrndqsq2ndiz-gcc-13.3.0
│   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   ├───/nix/store/617chz8a4p5kz09ij8s9ns05iafzbpcc-gmp-6.3.0
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   └───/nix/store/617chz8a4p5kz09ij8s9ns05iafzbpcc-gmp-6.3.0 [...]
│   │   │   │   ├───/nix/store/93ph6f74wihfir4vyz2sj88d2vn2vq7y-mpfr-4.2.1
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   ├───/nix/store/617chz8a4p5kz09ij8s9ns05iafzbpcc-gmp-6.3.0 [...]
│   │   │   │   │   └───/nix/store/93ph6f74wihfir4vyz2sj88d2vn2vq7y-mpfr-4.2.1 [...]
│   │   │   │   ├───/nix/store/97f3gw9vpyxvwjv2i673isvg92q65mwn-gcc-13.3.0-lib [...]
│   │   │   │   ├───/nix/store/aax0hx68i2ikhpf27hdm6a2a209d4s6p-glibc-2.40-36-dev [...]
│   │   │   │   ├───/nix/store/h82a48wb6i6g42fbpxl7z7s40pw93g0n-libmpc-1.3.1
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   ├───/nix/store/617chz8a4p5kz09ij8s9ns05iafzbpcc-gmp-6.3.0 [...]
│   │   │   │   │   ├───/nix/store/93ph6f74wihfir4vyz2sj88d2vn2vq7y-mpfr-4.2.1 [...]
│   │   │   │   │   └───/nix/store/h82a48wb6i6g42fbpxl7z7s40pw93g0n-libmpc-1.3.1 [...]
│   │   │   │   ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
│   │   │   │   ├───/nix/store/zj93rq650fz6v25qw39sm025ya4k8plp-isl-0.20
│   │   │   │   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   │   │   │   ├───/nix/store/617chz8a4p5kz09ij8s9ns05iafzbpcc-gmp-6.3.0 [...]
│   │   │   │   │   └───/nix/store/zj93rq650fz6v25qw39sm025ya4k8plp-isl-0.20 [...]
│   │   │   │   └───/nix/store/xzfmarrq8x8s4ivpya24rrndqsq2ndiz-gcc-13.3.0 [...]
│   │   │   └───/nix/store/3ix5h74n7ar9950vwzp4dxmil70pmx0k-gcc-wrapper-13.3.0 [...]
│   │   ├───/nix/store/7vs39d9phfvq4a95ydmq3zkpf518wlmb-libffi-3.4.6-dev [...]
│   │   ├───/nix/store/8s7f5jgn8bbvj552hb5glsgwfx881kfy-ncurses-6.4.20221231 [...]
│   │   ├───/nix/store/mns770di6nbh52gq0nx07mmc422gm8fc-elfutils-0.191 [...]
│   │   ├───/nix/store/c3mgiawvdsf0vp336z7qybx04i6hx8dh-elfutils-0.191-dev [...]
│   │   ├───/nix/store/hh783czjqlddq96zxhzijcqv92rb132r-ghc-9.6.6-doc [...]
│   │   ├───/nix/store/inpspwqhgpld2zdk89hra7xjh3nxll2x-ncurses-6.4.20221231-dev [...]
│   │   └───/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6 [...]
│   ├───/nix/store/gc4i9g6yjb85x6r895xzs45v7b5a4vn3-ieee754-0.8.0-doc
│   │   └───/nix/store/hh783czjqlddq96zxhzijcqv92rb132r-ghc-9.6.6-doc [...]
│   ├───/nix/store/0qryjgyp44ylnlhpvrfhdadsbqlwnvvl-ieee754-0.8.0
│   │   ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
│   │   ├───/nix/store/0d4h5nnbliwpqa5hcmq0lad6r2xfbpii-libffi-3.4.6 [...]
│   │   ├───/nix/store/8s7f5jgn8bbvj552hb5glsgwfx881kfy-ncurses-6.4.20221231 [...]
│   │   ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
│   │   ├───/nix/store/mns770di6nbh52gq0nx07mmc422gm8fc-elfutils-0.191 [...]
│   │   ├───/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6 [...]
│   │   ├───/nix/store/gc4i9g6yjb85x6r895xzs45v7b5a4vn3-ieee754-0.8.0-doc [...]
│   │   └───/nix/store/0qryjgyp44ylnlhpvrfhdadsbqlwnvvl-ieee754-0.8.0 [...]
│   └───/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages [...]
├───/nix/store/q7sqq18llwqsm7sqk6xpj377q440lyzj-libraries
│   ├───/nix/store/ixbhr7shi2l3k4bh20c43w1vmx2gvdgv-agda-categories-0.2.0
│   └───/nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1
└───/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin
    ├───/nix/store/pacbfvpzqz2mksby36awvbcn051zcji3-glibc-2.40-36 [...]
    ├───/nix/store/0d4h5nnbliwpqa5hcmq0lad6r2xfbpii-libffi-3.4.6 [...]
    ├───/nix/store/8s7f5jgn8bbvj552hb5glsgwfx881kfy-ncurses-6.4.20221231 [...]
    ├───/nix/store/l4wqc044x1c7anj11m5zcmd6wf2mjpn3-gmp-with-cxx-6.3.0 [...]
    ├───/nix/store/y6bcc1vzg315zzzpir608zkhnmvp49kc-zlib-1.3.1 [...]
    ├───/nix/store/mns770di6nbh52gq0nx07mmc422gm8fc-elfutils-0.191 [...]
    └───/nix/store/p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data

SYSTEM INFORMATION

OS: NixOS
Nixpkgs:

    nixpkgs = {
      type = "github";
      owner = "nixos";
      repo = "nixpkgs";
      rev = "23e89b7da85c3640bbc2173fe04f4bd114342367";
    };

agda: version 2.7.0.1 | Built with flags (cabal -f) | optimise-heavily: extra optimisations | debug: enable debug printing (‘-v’ verbosity flags)
agda: standard-library-2.1.1

MORE

https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary

starlit · December 17, 2024, 1:30pm

Tranquil Ity @ity:itycodes.org

Welcome to Agda
Research langs tend to have broken compilers
If we remember right the nix package is broken, too
You will need to debug the module loader

You're invited to talk on Matrix

Honestly, we wouldn’t dare to try Agda on Nix.
To be honest, there’s also the possibility that your code is wrong, Agda has at least 4 incompatible versions with their hello world docs that are hard to distinguish, and the error it prints is about failing to find module
Agda piggybacks off of GHC
And its module loading
Nix wraps GHC probably

You're invited to talk on Matrix

starlit · December 17, 2024, 3:22pm

DEBUGGING

fd agda nixpkgs/pkgs/ 
pkgs/top-level/agda-packages.nix
pkgs/build-support/agda/
pkgs/applications/science/logic/cedille/Fix-to-string.agda-to-compile-with-Agda-2.6.1.patch
pkgs/applications/editors/emacs/elisp-packages/manual-packages/agda2-mode/
pkgs/development/libraries/agda/
pkgs/development/libraries/agda/agdarsec/
pkgs/development/libraries/agda/agda-prelude/
pkgs/development/libraries/agda/agda-categories/

nixpkgs/pkgs/build-support/agda/default.nix

        mkdir -p $out/bin
        makeWrapper ${Agda.bin}/bin/agda $out/bin/agda \
          --add-flags "--with-compiler=${ghc}/bin/ghc" \
          --add-flags "--library-file=${library-file}"
        ln -s ${Agda.bin}/bin/agda-mode $out/bin/agda-mode

cat /nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1/bin/agda
#! /nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37/bin/bash -e
exec "/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin/bin/agda"  --with-compiler=/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/bin/ghc --library-file=/nix/store/q7sqq18llwqsm7sqk6xpj377q440lyzj-libraries "$@"

cat /nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/bin/ghc
#! /nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37/bin/bash -e
export NIX_GHC='/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/bin/ghc'
export NIX_GHCPKG='/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/bin/ghc-pkg'
export NIX_GHC_DOCDIR='/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/share/doc/ghc/html'
export NIX_GHC_LIBDIR='/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/lib/ghc-9.6.6/lib'
exec "/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6/bin/ghc"  "-B$NIX_GHC_LIBDIR" "$@"

cat /nix/store/q7sqq18llwqsm7sqk6xpj377q440lyzj-libraries
/nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/standard-library.agda-lib
/nix/store/ixbhr7shi2l3k4bh20c43w1vmx2gvdgv-agda-categories-0.2.0/agda-categories.agda-lib

cat /nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/standard-library.agda-lib
name: standard-library-2.1.1
include: src
flags:
  --warning=noUnsupportedIndexedMatch

fd --ignore-case agda /nix/store | xargs rg 'p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data'
/nix/store/s1gi9hf5qpzrrzlwlmq1g2q8v2bryl81-home-manager-path/bin/agda-mode: binary file matches (found "\0" byte around offset 7)

/nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1/bin/agda-mode: binary file matches (found "\0" byte around offset 7)

/nix/store/1gvl2wdfiqafwkf4p57y959c9icrm266-user-environment/bin/agda-mode: binary file matches (found "\0" byte around offset 7)

/nix/store/3kgw0a86dlrjx9ssld0p9fbf2mx3g9yc-home-manager-path/bin/agda-mode: binary file matches (found "\0" byte around offset 7)

/nix/store/vbdahrf4zyny44nvxz56phrmyh290kzl-home-manager-path/bin/agda-mode: binary file matches (found "\0" byte around offset 7)

/nix/store/7j4fla076ka3d0r2hdzwyyqm3821zrbh-user-environment/bin/agda-mode: binary file matches (found "\0" byte around offset 7)
/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin/bin/agda-mode: binary file matches (found "\0" byte around offset 7)

/nix/store/3azvrpwmicd7ahprdwbm94k292bpq3hd-agdaWithPackages-2.7.0.1/bin/agda-mode: binary file matches (found "\0" byte around offset 7)

/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin/bin/agda: binary file matches (found "\0" byte around offset 7)
/nix/store/qw7b5bk5ws83dyl96nvdkp899cmpygmx-Agda-2.7.0.1.drv
1:Derive([("bin","/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin","",""),("data","/nix/store/p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data","",""),("doc","/nix/store/ywl5znlymcl8ldvma0lapxl0n2jh8xjc-Agda-2.7.0.1-doc","",""),("out","/nix/store/sg4d70bp9b42xx0y1p6hybpxrxi0crp9-Agda-2.7.0.1","","")],[("/nix/store/0zyzfyxfms220mkvw5cjjgk89abhisaw-blaze-html-0.9.2.0.drv",["out"]),("/nix/store/231r1g6y43bbnps5hd3nmvyps9y9b3a0-dlist-1.0.drv",["out"]),("/nix/store/2wi1j79w1axxq7isrvd8sbi32rlhd638-gitrev-1.3.1.drv",["out"]),("/nix/store/3bzfgljxhqx3iq2yc21gy47b6wn9q3w0-remove-references-to.drv",["out"]),("/nix/store/46fpwwwc3j4l78ckshhghqcyiijfcwcq-strict-0.5.drv",["out"]),("/nix/store/553zdcr1bccrmc2gpjc4iamjmlcjg820-monad-control-1.0.3.1.drv",["out"]),("/nix/store/55gffvg21ybp07pc35p4xfiywrlj5cr8-boxes-0.1.5.drv",["out"]),("/nix/store/5c34kl793sfhn7qp49542bbxaj044dca-ghc-9.6.6.drv",["out"]),("/nix/store/5yvfkplaqb1slhdvcvs3qnkrnfv77fif-pqueue-1.5.0.0.drv",["out"]),("/nix/store/6kid6nw0qg3hxbsgr3j9xcs0dv1wxmp9-vector-hashtables-0.1.2.0.drv",["out"]),("/nix/store/8nndns2ly8pl31jw4yp6646c81dad17r-STMonadTrans-0.4.8.drv",["out"]),("/nix/store/bhiqrvb2fyb0nvqcpx545pywn9h21xnx-async-2.2.5.drv",["out"]),("/nix/store/bxy33sp8cwg0c8lpvv0b6g3ys6ilqwsm-happy-1.20.1.1.drv",["out"]),("/nix/store/c7340lpp5vzlch968wq499805xg7v4nr-haskell-generic-builder-test-wrapper.sh.drv",["out"]),("/nix/store/cb3msdvf2q70s7wd2hyhiwsk0yj4hhgc-regex-tdfa-1.3.2.2.drv",["out"]),("/nix/store/din32dgdwdvqpbkhzdslp9j145lsvgii-alex-3.4.0.1.drv",["out"]),("/nix/store/gjz1z2qk71rxh3f449drdxn6fnd5909h-hscolour-1.25.drv",["out"]),("/nix/store/gk6as4in5fphr7ds30l9cyn70icxr54a-coreutils-9.5.drv",["out"]),("/nix/store/gzlzaavil7r2lpq8b3hyplgfgidf5jw4-stdenv-linux.drv",["out"]),("/nix/store/imfrl49rpk9nkscjs0vvg7mbm21lcmn0-ansi-terminal-1.0.2.drv",["out"]),("/nix/store/jjr9c2xszmlxs5bdv8mxcsqgmxdf3800-murmur-hash-0.1.0.10.drv",["out"]),("/nix/store/jph00w7yhblsk7r7vxwwqbiwx2vz5gfn-data-hash-0.2.0.1.drv",["out"]),("/nix/store/kl3la2k4lsydnfkykigrqca7jch0yxq0-unordered-containers-0.2.20.drv",["out"]),("/nix/store/kl42k18whdr6pjxycs0mxxbnc4ba54kl-equivalence-0.4.1.drv",["out"]),("/nix/store/kxys3mcd3zb59crc9pgil15aq7503q0f-glibc-locales-2.40-36.drv",["out"]),("/nix/store/l95vx068ryhs4ws6i9n1331gpqgzmh2h-vector-0.13.1.0.drv",["out"]),("/nix/store/lwijvl7mk7c9wbn6jvshsafpmsgc3kb9-split-0.2.5.drv",["out"]),("/nix/store/n8kpgc67aqa7h59x7x1qnp95ci21m6jm-aeson-2.1.2.1.drv",["out"]),("/nix/store/sh85zkyp8l5ny38kv0qhp93fai135qpk-uri-encode-1.5.0.7.drv",["out"]),("/nix/store/v3m8jncv3laxiwblps2b3giwncbi9chh-parallel-3.2.2.0.drv",["out"]),("/nix/store/vjznlmanjkps53l7hw2krvpzwqcd5m3d-bash-5.2p37.drv",["out"]),("/nix/store/w1q0dssc3nn0zv0zvh7kn3rkx56x6yrc-zlib-0.6.3.0.drv",["out"]),("/nix/store/w9ilbh9idxd2bqafla7hybnc9cylriw2-Agda-2.7.0.1.tar.gz.drv",["out"]),("/nix/store/x2xg956l38xp288klpa4nbi1yfzwr7zf-edit-distance-0.2.2.1.drv",["out"]),("/nix/store/yhvzqj2cwjsxidys82m7qz81i3a2wnmn-case-insensitive-1.2.1.0.drv",["out"]),("/nix/store/yk0fsshbfnd1yxsv33naa2wmb4h2p43z-hashable-1.4.4.0.drv",["out"]),("/nix/store/z0350d5jzym28hwynag6xncr65ajmb9x-gnugrep-3.11.drv",["out"]),("/nix/store/z19nabhg4qimrc0wg7iq7vfhbx65vkvj-emacs-29.4.drv",["out"]),("/nix/store/z9vqv6q3mk0p7gnfybalkkdm1sqiqjif-peano-0.1.0.2.drv",["out"])],["/nix/store/4mdp8nhyfddh7bllbi7xszz7k9955n79-Setup.hs","/nix/store/907d7wf2d113vlv8dlhi1i3d683gc1rs-unpretty-cabal-conf.awk","/nix/store/v6x3cs394jgqfbi0a42pam708flxaphh-default-builder.sh"],"x86_64-linux","/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37/bin/bash",["-e","/nix/store/v6x3cs394jgqfbi0a42pam708flxaphh-default-builder.sh"],[("LANG","en_US.UTF-8"),("LOCALE_ARCHIVE","/nix/store/7hivmh39qsl8abz86cfwc02lyqqbdw44-glibc-locales-2.40-36/lib/locale/locale-archive"),("NIX_HARDENING_ENABLE","bindnow format fortify fortify3 pic relro stackprotector strictoverflow zerocallusedregs"),("__structuredAttrs",""),("bin","/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin"),("buildInputs",""),("buildPhase","runHook preBuild\n./Setup build \nrunHook postBuild\n"),("builder","/nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37/bin/bash"),("checkPhase","runHook preCheck\ncheckFlagsArray+=(\n  \"--show-details=streaming\"\n  \"--test-wrapper=/nix/store/wf3yqga7gdmjkmp1rr1mjsff8l1jr6pg-haskell-generic-builder-test-wrapper.sh\"\n  \n)\nexport NIX_GHC_PACKAGE_PATH_FOR_TEST=\"${NIX_GHC_PACKAGE_PATH_FOR_TEST:-$packageConfDir:}\"\n./Setup test  $checkFlags ${checkFlagsArray:+\"${checkFlagsArray[@]}\"}\nrunHook postCheck\n"),("cmakeFlags",""),("compileBuildDriverPhase","runHook preCompileBuildDriver\n\nfor i in Setup.hs Setup.lhs /nix/store/4mdp8nhyfddh7bllbi7xszz7k9955n79-Setup.hs; do\n  test -f $i && break\ndone\n\necho setupCompileFlags: $setupCompileFlags\nghc $setupCompileFlags --make -o Setup -odir $builddir -hidir $builddir $i\n\nrunHook postCompileBuildDriver\n"),("configureFlags","-foptimise-heavily -fdebug"),("configurePhase","runHook preConfigure\n\necho configureFlags: $configureFlags\n./Setup configure $configureFlags 2>&1 | /nix/store/k48bha2fjqzarg52picsdfwlqx75aqbb-coreutils-9.5/bin/tee \"$NIX_BUILD_TOP/cabal-configure.log\"\nif /nix/store/14aswfz6pm8zvyyy927xzmi8x4rnvlc8-gnugrep-3.11/bin/egrep -q -z 'Warning:.*depends on multiple versions' \"$NIX_BUILD_TOP/cabal-configure.log\"; then\n  echo >&2 \"*** abort because of serious configure-time warning from Cabal\"\n  exit 1\nfi\n\n\nrunHook postConfigure\n"),("configurePlatforms",""),("data","/nix/store/p3pgifmn30jbgfviadrlcrrg8qz1jivd-Agda-2.7.0.1-data"),("depsBuildBuild","/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6"),("depsBuildBuildPropagated",""),("depsBuildTarget",""),("depsBuildTargetPropagated",""),("depsHostHost",""),("depsHostHostPropagated",""),("depsTargetTarget",""),("depsTargetTargetPropagated",""),("doCheck","1"),("doInstallCheck",""),("doc","/nix/store/ywl5znlymcl8ldvma0lapxl0n2jh8xjc-Agda-2.7.0.1-doc"),("haddockPhase","runHook preHaddock\n./Setup haddock --html \\\n  --hoogle \\\n  --quickjump \\\n  --hyperlink-source \\\n  \n\nrunHook postHaddock\n"),("hardeningDisable","pie"),("installPhase","runHook preInstall\n\n./Setup copy \nlocal packageConfDir=\"$out/lib/ghc-9.6.6/lib/package.conf.d\"\nlocal packageConfFile=\"$packageConfDir/Agda-2.7.0.1.conf\"\nmkdir -p \"$packageConfDir\"\n./Setup register --gen-pkg-config=$packageConfFile\nif [ -d \"$packageConfFile\" ]; then\n  mv \"$packageConfFile/\"* \"$packageConfDir\"\n  rmdir \"$packageConfFile\"\nfi\nfor packageConfFile in \"$packageConfDir/\"*; do\n  local pkgId=$(gawk -f /nix/store/907d7wf2d113vlv8dlhi1i3d683gc1rs-unpretty-cabal-conf.awk \"$packageConfFile\" \\\n    | grep '^id:' | cut -d' ' -f2)\n  mv \"$packageConfFile\" \"$packageConfDir/$pkgId.conf\"\ndone\n\n# delete confdir if there are no libraries\nfind $packageConfDir -maxdepth 0 -empty -delete;\n\n\n\n\nfor x in $doc/share/doc/Agda-2.7.0.1\"/html/src/\"*.html; do\n  remove-references-to -t $out $x\ndone\nmkdir -p $doc\n\nmkdir -p $data\n\nrunHook postInstall\n"),("mesonFlags",""),("name","Agda-2.7.0.1"),("nativeBuildInputs","/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6 /nix/store/0ccdm7sdyza2pybmbyblmxxhn68pq49h-remove-references-to      /nix/store/i11jh38m8bz65i1dlzdy7lc0mf0y34bf-alex-3.4.0.1 /nix/store/f86cjjcrqnlzg7agnfq4jwjwxb1vi7q4-happy-1.20.1.1 /nix/store/a3kfh7mx5ssar7z835vsiq7gmf7df2mg-emacs-29.4"),("out","/nix/store/sg4d70bp9b42xx0y1p6hybpxrxi0crp9-Agda-2.7.0.1"),("outputs","out data doc bin"),("patches",""),("pname","Agda"),("postPatch",""),("preConfigurePhases","compileBuildDriverPhase"),("preInstallPhases","haddockPhase"),("prePatch",""),("prePhases","setupCompilerEnvironmentPhase"),("propagatedBuildInputs","/nix/store/mmimpcfx4p975rscc5nkh25izj87r3cc-aeson-2.1.2.1 /nix/store/idha1b684mwgxh314jaq0xlmvcr8hvb0-ansi-terminal-1.0.2  /nix/store/ahbjxr284n9mr06w2cgsj1v4msa2rqja-async-2.2.5   /nix/store/5gbsvg8b5sqbimbrfdwm2rkq67a2nnbr-blaze-html-0.9.2.0 /nix/store/pbj00y1yzcq60jajyhghv9mxrki4ac28-boxes-0.1.5  /nix/store/myqnd0z2ci5q2cq97wjgd7jj36xsr14s-case-insensitive-1.2.1.0  /nix/store/ahmf0d27kwgknsgzhj43rh7qfw5qaqis-data-hash-0.2.0.1   /nix/store/599y74vymh1vsf9iw49avs3h06aa49p1-dlist-1.0 /nix/store/ws3zh5z960nw3s3rdqx04kkvpvsssxi4-edit-distance-0.2.2.1 /nix/store/46ssx2c526c09mf8a79vdaa31p833kqs-equivalence-0.4.1    /nix/store/ql2xkpads3pgphkb5ahkkaca4zi782xh-gitrev-1.3.1 /nix/store/1rwmfb7a5k4lj01msxw1r0wkcips5fww-hashable-1.4.4.0  /nix/store/k4r5nfnw4rda2238z02izrgd298747rm-monad-control-1.0.3.1  /nix/store/8m5a80g97s0lhxk29im7ww3z040vsyx4-murmur-hash-0.1.0.10 /nix/store/pi9icma27y97yfn4gzfd2yxkz7bwwi36-parallel-3.2.2.0 /nix/store/m123p4gi0rqihm598h4wapxl4266wjpf-peano-0.1.0.2 /nix/store/zxnb6bk51rdwfqam77lg10nwi2dl1q7h-pqueue-1.5.0.0   /nix/store/4wplhalki2psaw7iggxb5bdhy5fn3x8x-regex-tdfa-1.3.2.2 /nix/store/y6k5bra9m99hg6rwqglz4q462jfg313i-split-0.2.5  /nix/store/7svb3sn34jlymw6dhwiixfargy4fhp90-STMonadTrans-0.4.8 /nix/store/078gqn1rr4rh9laxaxyl38yawh4a4wqd-strict-0.5    /nix/store/4i5bckymgx1h6dlm6l0prbrbqbha45my-unordered-containers-0.2.20 /nix/store/yn6sx97qzajj696jkv9rc9bsr3ymh55n-uri-encode-1.5.0.7 /nix/store/vngsg12jaf3r5z3dvr887sl0j24vgl0k-vector-0.13.1.0 /nix/store/n42qlp6zwwnni44n371xryg0z01p6z6y-vector-hashtables-0.1.2.0 /nix/store/a9pzl67blbykhc03hb74adnnrdvijbnw-zlib-0.6.3.0    "),("propagatedNativeBuildInputs",""),("setOutputFlags",""),("setupCompilerEnvironmentPhase","NIX_BUILD_CORES=$(( NIX_BUILD_CORES < 16 ? NIX_BUILD_CORES : 16 ))\nrunHook preSetupCompilerEnvironment\n\necho \"Build with /nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6.\"\nexport PATH=/nix/store/26wgv2q51bkmjn9iqmqscbv8a1zpksi0-hscolour-1.25/bin:$PATH\n\nbuilddir=\"$(mktemp -d)\"\nsetupPackageConfDir=\"$builddir/setup-package.conf.d\"\nmkdir -p $setupPackageConfDir\npackageConfDir=\"$builddir/package.conf.d\"\nmkdir -p $packageConfDir\n\nsetupCompileFlags=\"-package-db=$setupPackageConfDir -threaded\"\nconfigureFlags=\"--verbose --prefix=$out --libdir=\\$prefix/lib/\\$compiler/lib --libsubdir=\\$abi/\\$libname --datadir=$data/share/ghc-9.6.6 --docdir=$doc/share/doc/Agda-2.7.0.1 --with-gcc=$CC --package-db=$packageConfDir   --ghc-option=-j$NIX_BUILD_CORES --ghc-option=+RTS --ghc-option=-A64M --ghc-option=-RTS  --enable-library-profiling --profiling-detail=exported-functions --disable-profiling --enable-shared --disable-coverage --enable-static --disable-executable-dynamic --enable-tests --disable-benchmarks --enable-library-vanilla --disable-library-for-ghci --enable-split-sections --enable-library-stripping --enable-executable-stripping --bindir=$bin/bin --ghc-option=-haddock $configureFlags\"\nfor p in \"${pkgsBuildBuild[@]}\" \"${pkgsBuildHost[@]}\" \"${pkgsBuildTarget[@]}\"; do\n  # If this dependency has a package database, then copy the contents of it,\n# unless it is one of our GHCs. These can appear in our dependencies when\n# we are doing native builds, and they have package databases in them, but\n# we do not want to copy them over.\n#\n# We don't need to, since those packages will be provided by the GHC when\n# we compile with it, and doing so can result in having multiple copies of\n# e.g. Cabal in the database with the same name and version, which is\n# ambiguous.\nif [ -d \"$p/lib/ghc-9.6.6/lib/package.conf.d\" ] && [ \"$p\" != \"/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6\" ] && [ \"$p\" != \"/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6\" ]; then\n  cp -f \"$p/lib/ghc-9.6.6/lib/package.conf.d/\"*.conf $setupPackageConfDir/\n  continue\nfi\n\ndone\nghc-pkg --package-db=\"$setupPackageConfDir\" recache\nfor p in \"${pkgsHostHost[@]}\" \"${pkgsHostTarget[@]}\"; do\n  # If this dependency has a package database, then copy the contents of it,\n# unless it is one of our GHCs. These can appear in our dependencies when\n# we are doing native builds, and they have package databases in them, but\n# we do not want to copy them over.\n#\n# We don't need to, since those packages will be provided by the GHC when\n# we compile with it, and doing so can result in having multiple copies of\n# e.g. Cabal in the database with the same name and version, which is\n# ambiguous.\nif [ -d \"$p/lib/ghc-9.6.6/lib/package.conf.d\" ] && [ \"$p\" != \"/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6\" ] && [ \"$p\" != \"/nix/store/4b0ycfpi0fi7za3nhd407dgv6pnk0q3j-ghc-9.6.6\" ]; then\n  cp -f \"$p/lib/ghc-9.6.6/lib/package.conf.d/\"*.conf $packageConfDir/\n  continue\nfi\n\n  if [ -d \"$p/include\" ]; then\n    configureFlags+=\" --extra-include-dirs=$p/include\"\n  fi\n  if [ -d \"$p/lib\" ]; then\n    configureFlags+=\" --extra-lib-dirs=$p/lib\"\n  fi\n  if [[ -d \"$p/Library/Frameworks\" ]]; then\n    configureFlags+=\" --extra-framework-dirs=$p/Library/Frameworks\"\n  fi\ndone\nghc-pkg --package-db=\"$packageConfDir\" recache\n\nrunHook postSetupCompilerEnvironment\n"),("src","/nix/store/7ga6l29mlfcls91vj1qwah13dxg1wr1l-Agda-2.7.0.1.tar.gz"),("stdenv","/nix/store/gw0swsnbfk9l8d1il70psm8b3r5m33jv-stdenv-linux"),("strictDeps",""),("system","x86_64-linux"),("version","2.7.0.1")])

fd --ignore-case agda ~/dev/nixpkgs/pkgs/ | xargs rg 'mode'
/home/starlit/dev/nixpkgs/pkgs/build-support/agda/default.nix
71:        ln -s ${Agda.bin}/bin/agda-mode $out/bin/agda-mode

/home/starlit/dev/nixpkgs/pkgs/applications/editors/emacs/elisp-packages/manual-packages/agda2-mode/package.nix
6:  pname = "agda2-mode";
9:  files = ''("src/data/emacs-mode/*.el")'';
13:    description = "Agda2-mode for Emacs extracted from Agda package";

rhendric · December 18, 2024, 2:29am

To depend on any libraries, including standard-library, you need either to specify them on the command line or, preferably, to create a *.agda-lib file in your project directory that lists them. This is the error you get when you have forgotten to do this. See this section, and the very last section of the standard-library installation guide. (withPackages takes care of all the earlier machine-wide stuff for you, but you need to do the final step in your project yourself.)

starlit · December 18, 2024, 11:37am

@rhendric: Thanks for the insights! Could you give me an example of a --library-file=standard-library.agda-lib file and the steps to successfully compilation of a Agda file that uses the standard library?

For example, I tried this

hello-world-dep.agda

module hello-world-dep where

open import Data.Nat using (ℕ; zero; suc)

data Vec (A : Set) : ℕ → Set where
  []   : Vec A zero
  _::_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infixr 5 _::_

standard-library.agda-lib

name: standard-library-2.1.1
include: /nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/src/
flags:
  --warning=noUnsupportedIndexedMatch

Then

sh -c "/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin/bin/agda --with-compiler=/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/bin/ghc --library-file=standard-library.agda-lib hello-world-dep.agda"
standard-library.agda-lib:1:
Failed to read library file name: standard-library-2.1.1.
Reason: name: standard-library-2.1.1: openBinaryFile: does not exist (No such file or directory)
standard-library.agda-lib:2:
Failed to read library file include: /nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/src/.
Reason: include: /nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/src/: openBinaryFile: does not exist (No such file or directory)
standard-library.agda-lib:3:
Failed to read library file flags:.
Reason: flags:: openBinaryFile: does not exist (No such file or directory)
standard-library.agda-lib:4:
Failed to read library file --warning=noUnsupportedIndexedMatch.
Reason: --warning=noUnsupportedIndexedMatch: openBinaryFile: does not exist (No such file or directory)

(yes, these paths in the nix store exist, i checked)

Anyway, isn’t Agda on Nix a wrapped bash script that includes --library-file=FILE with the withPackages such as standard library for that purpose already? See the debugging:

starlit:

nixpkgs/pkgs/build-support/agda/default.nix

        mkdir -p $out/bin
        makeWrapper ${Agda.bin}/bin/agda $out/bin/agda \
          --add-flags "--with-compiler=${ghc}/bin/ghc" \
          --add-flags "--library-file=${library-file}"
        ln -s ${Agda.bin}/bin/agda-mode $out/bin/agda-mode

cat /nix/store/zc1i63a0b3kq2v03fbccvp21midpvnkv-agdaWithPackages-2.7.0.1/bin/agda
#! /nix/store/0irlcqx2n3qm6b1pc9rsd2i8qpvcccaj-bash-5.2p37/bin/bash -e
exec "/nix/store/vc3cd3kqx6ha065pgv6w8rz106w1b92s-Agda-2.7.0.1-bin/bin/agda"  --with-compiler=/nix/store/lw4ayqc5g7sagm4pl3bybh3viby29vsr-ghc-9.6.6-with-packages/bin/ghc --library-file=/nix/store/q7sqq18llwqsm7sqk6xpj377q440lyzj-libraries "$@"

cat /nix/store/q7sqq18llwqsm7sqk6xpj377q440lyzj-libraries
/nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/standard-library.agda-lib
/nix/store/ixbhr7shi2l3k4bh20c43w1vmx2gvdgv-agda-categories-0.2.0/agda-categories.agda-lib

cat /nix/store/zdl2bawyiwwx964z7ybm10p955yb4dcz-standard-library-2.1.1/standard-library.agda-lib
name: standard-library-2.1.1
include: src
flags:
  --warning=noUnsupportedIndexedMatch

rhendric · December 18, 2024, 11:41am

Option 1: command line arguments

% nix-shell -p 'agdaPackages.agda.withPackages (ps: [ ps.standard-library ])'

$ cat hello-world-dep.agda
module hello-world-dep where

open import Data.Nat using (ℕ; zero; suc)

data Vec (A : Set) : ℕ → Set where
  []   : Vec A zero
  _::_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infixr 5 _::_

$ agda -l standard-library -i. --compile hello-world-dep.agda
Calling: /nix/store/qqprbg04sz2a3ij2b0rcnsv9wn72mvgx-ghc-9.6.6-with-packages/bin/ghc -O -Werror -i/tmp/agda-help /tmp/agda-help/MAlonzo/Code/QhelloZ45ZworldZ45Zdep.hs --make -fwarn-incomplete-patterns
warning: -W[no]NoMain
No main function defined in hello-world-dep.
Use option --no-main to suppress this warning.

$

Option 2: an .agda-lib file

% nix-shell -p 'agdaPackages.agda.withPackages (ps: [ ps.standard-library ])'

$ cat hello-world-dep.agda
module hello-world-dep where

open import Data.Nat using (ℕ; zero; suc)

data Vec (A : Set) : ℕ → Set where
  []   : Vec A zero
  _::_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infixr 5 _::_

$ cat project.agda-lib 
depend: standard-library
include: .

$ agda --compile hello-world-dep.agda
Calling: /nix/store/qqprbg04sz2a3ij2b0rcnsv9wn72mvgx-ghc-9.6.6-with-packages/bin/ghc -O -Werror -i/tmp/agda-help /tmp/agda-help/MAlonzo/Code/QhelloZ45ZworldZ45Zdep.hs --make -fwarn-incomplete-patterns
warning: -W[no]NoMain
No main function defined in hello-world-dep.
Use option --no-main to suppress this warning.

$

starlit · December 19, 2024, 2:18pm

Thank you very much! Just in case, here are the nix3 pure equivalent of that (thanks @lily:lily.flowers)

nix develop "$(nix eval --raw nixpkgs#agdaPackages.agda --apply 'agda: (agda.withPackages (ps: [ ps.standard-library ])).drvPath')"

nix shell "$(nix eval --raw nixpkgs#agdaPackages.agda --apply 'agda: (agda.withPackages (ps: [ ps.standard-library ])).drvPath')^*"

(~~something something without warranty express or implied something something not liable if it causes your computer to eat your files in response to running such unholy commands~~)
—@lily:lily.flowers

starlit · December 19, 2024, 2:20pm

Also, a good example of an Agda+Nix project: GitHub - conal/felix: Agda category theory library for denotational design