nix binary ignores interface files
stites opened this issue · 5 comments
stites commented
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 commented
I'm not a Nix user so I'm afraid I'm not really able to provide any help here.
anka-213 commented
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 commented
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
{
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
{
"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 commented
I'll close this for now! Please reopen it if it is still an issue for you.