nix binary ignores interface files

[stites]

I am expecting that agda2hs will not recompile the interface files, but it looks like this is not the case for the binary on my system. Is this expected behavior? If it is, can someone help me get a nix derivation that can also load the standard-library?

First, I needed to ensure standard-library is compiled with `--local-interfaces` (which is different behavior compared to 1.7.x). See below:

{
  inputs = {
    nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
    agda2hs.url = "github:agda/agda2hs";
  };
  outputs = { nixpkgs, agda2hs, ... }: {
    devShells."x86_64-linux".default = let
      pkgs = nixpkgs.legacyPackages."x86_64-linux";
      inherit (agda2hs.packages."x86_64-linux") agda2hs-lib;
      inherit (pkgs.agdaPackages) standard-library;
      stdlib = standard-library.overrideAttrs(o: {
        buildPhase = ''
          runHook preBuild
          agda --local-interfaces -i. ./Everything.agda
          rm ./Everything.agda ./Everything.agdai
          runHook postBuild
        '';
      });
      agda-pkgs = { pkgs = [ stdlib agda2hs-lib ]; };
    in pkgs.mkShell {
      nativeBuildInputs = [
        (agda2hs.lib."x86_64-linux".withPackages agda-pkgs)
        (pkgs.agda.withPackages agda-pkgs)
      ];
    };
  };
}

I can see that the library files are correctly loaded in the `nix develop` shell:

$ cat $(cat $(which agda) | \grep --only-matching 'library-file=[^ ]*' | \sed 's/library-file=\([^ ]*\)/\1/')
/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/standard-library.agda-lib
/nix/store/87b7jrncfwmbsddznf7ajhvc5q4iisc4-agda2hs-1.3/agda2hs.agda-lib

$ cat $(cat $(which agda2hs) | \grep --only-matching 'library-file=[^ ]*' | \sed 's/library-file=\([^ ]*\)/\1/')
/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/standard-library.agda-lib
/nix/store/87b7jrncfwmbsddznf7ajhvc5q4iisc4-agda2hs-1.3/agda2hs.agda-lib

Now if I try to compile a trivial module, I get a permissions error as agda2hs attempts to compile Data/Unit/Base.agdai in the /nix/store:

$ cat Foo.agda
module Foo where
open import Data.Bool

$ agda2hs Foo.agda -o .
Checking Foo (/home/stites/stuff/Foo.agda).
 Checking Data.Bool (/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Bool.agda).
  Checking Data.Bool.Base (/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Bool/Base.agda).
   Checking Data.Unit.Base (/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Unit/Base.agda).
Failed to write interface /nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Unit/Base.agdai.
/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Bool/Base.agda:11,1-37
/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Unit/Base.agdai:
removeLink: permission denied (Read-only file system)

However, this interface file does not need to be recompiled:

$ ls /nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Unit/Base.agda*
/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Unit/Base.agda
/nix/store/mgplhlsvhiajq30klgr47brh9nyi05b4-standard-library-2.0/src/Data/Unit/Base.agdai

[jespercockx]

I'm not a Nix user so I'm afraid I'm not really able to provide any help here.

[anka-213]

Hmm, I'm unable to reproduce this on darwin. I'll see if I can reproduce it on a linux VM. Does agda itself have the same issue? You can also try compiling it with agda2hs Foo.agda -o . -v import.iface:100 to get some debug info on the importing part.

[anka-213]

Nope, I don't have any trouble if I build it on a linux machine either. See logs here.

Maybe something changed since you tried it? Can you include your lockfile?

Here's the self-contained `flake.nix`-file I used to reproduce using remote builds

```nix { inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; agda2hs.url = "github:agda/agda2hs"; }; outputs = { nixpkgs, agda2hs, ... }: let systems = [ "x86_64-linux" "x86_64-darwin" ]; # systems = [ "x86_64-darwin" ]; # forAllSystems = f: nixpkgs.lib.genAttrs systems (system: f system); forAllSystems = nixpkgs.lib.genAttrs systems; stuff = forAllSystems (system: rec { pkgs = nixpkgs.legacyPackages.${system}; inherit (agda2hs.packages.${system}) agda2hs-lib; inherit (pkgs.agdaPackages) standard-library; stdlib = standard-library.overrideAttrs (o: { buildPhase = '' runHook preBuild agda --local-interfaces -i. ./Everything.agda rm ./Everything.agda ./Everything.agdai runHook postBuild ''; }); agda-pkgs = { pkgs = [ stdlib agda2hs-lib ]; }; my-agda2hs = agda2hs.lib."${system}".withPackages agda-pkgs; my-agda = pkgs.agda.withPackages agda-pkgs; }); in { devShells = forAllSystems (system: { default = let inherit (stuff.${system}) pkgs agda-pkgs my-agda my-agda2hs; in pkgs.mkShell { nativeBuildInputs = [ my-agda2hs my-agda ]; }; }); packages = forAllSystems (system: let inherit (stuff.${system}) pkgs agda-pkgs my-agda my-agda2hs; Foo-agda = pkgs.writeText "Foo.agda" '' module Foo where open import Data.Bool ''; foo-agda-lib = pkgs.writeText "foo.agda-lib" '' name: foo depend: standard-library agda2hs include: . ''; in { foo-hs = nixpkgs.legacyPackages.${system}.runCommand "mkFoo" { } '' mkdir $out cp ${Foo-agda} Foo.agda cp ${foo-agda-lib} foo.agda-lib ${my-agda2hs}/bin/agda2hs Foo.agda -v 2 -o $out ''; }); }; } ```

And the corresponding `flake.lock`-file

```json { "nodes": { "agda2hs": { "inputs": { "flake-utils": "flake-utils", "nixpkgs": "nixpkgs" }, "locked": { "lastModified": 1726838279, "narHash": "sha256-qJEQY9dMAP/7CWs70ebaZgQrs/YbxZ061jhNGA/f1sE=", "owner": "agda", "repo": "agda2hs", "rev": "22f37f57fe5c17193147d90f548ecf327b5a694c", "type": "github" }, "original": { "owner": "agda", "repo": "agda2hs", "type": "github" } }, "flake-utils": { "inputs": { "systems": "systems" }, "locked": { "lastModified": 1726560853, "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", "owner": "numtide", "repo": "flake-utils", "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", "type": "github" }, "original": { "owner": "numtide", "repo": "flake-utils", "type": "github" } }, "nixpkgs": { "locked": { "lastModified": 1726757509, "narHash": "sha256-3/2rV78QyC/OPu+WzimbElmSdD3HsQq/P/TLcFQHjZQ=", "owner": "NixOS", "repo": "nixpkgs", "rev": "78fdf431cdf6bc4ba4af9c100aaeda65da7e4ed3", "type": "github" }, "original": { "owner": "NixOS", "repo": "nixpkgs", "type": "github" } }, "nixpkgs_2": { "locked": { "lastModified": 1726583932, "narHash": "sha256-zACxiQx8knB3F8+Ze+1BpiYrI+CbhxyWpcSID9kVhkQ=", "owner": "nixos", "repo": "nixpkgs", "rev": "658e7223191d2598641d50ee4e898126768fe847", "type": "github" }, "original": { "owner": "nixos", "ref": "nixpkgs-unstable", "repo": "nixpkgs", "type": "github" } }, "root": { "inputs": { "agda2hs": "agda2hs", "nixpkgs": "nixpkgs_2" } }, "systems": { "locked": { "lastModified": 1681028828, "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", "owner": "nix-systems", "repo": "default", "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", "type": "github" }, "original": { "owner": "nix-systems", "repo": "default", "type": "github" } } }, "root": "root", "version": 7 } ```

I used nix build --eval-store auto --store ssh-ng://eu.nixbuild.net .#packages.x86_64-linux.foo-hs -L --builders-use-substitutes to buil the above result on nixbuild.net.

[anka-213]

I'll close this for now! Please reopen it if it is still an issue for you.