agda-packages: add functional-linear-algebra library at v0.1 #100466
Conversation
pkgs/top-level/agda-packages.nix
Outdated
| @@ -26,5 +26,8 @@ let | |||
| cubical = callPackage ../development/libraries/agda/cubical { }; | |||
|
|
|||
| generic = callPackage ../development/libraries/agda/generic { }; | |||
|
|
|||
| fla = callPackage | |||
There was a problem hiding this comment.
Why not call it functional-linear-algebra?
There was a problem hiding this comment.
That makes more sense; I had been using FLA.* as imports inside the library because the name was too long but that doesn't really matter as much here since the name won't be part of a long identifier.
| @@ -0,0 +1,14 @@ | |||
| fetchFromGitHub: | |||
There was a problem hiding this comment.
Can you use a similar format to the other Agda libraries? Starting with { pkgs, usually. You can then inherit (pkgs) fetchFromGitHub I believe.
| sha256 = "09ri3jmgp9jjwi1mzv4c3w6rvcmyx6spa2qxpwlcn0f4bmfva6wm"; | ||
| }; | ||
|
|
||
| in import src |
There was a problem hiding this comment.
Alas that doesn't work in nixpkgs as far as I know :( I think it's not possible to import nix files from other repos. You will have to copy the agda derivation from there.
Probably that's what the build error is complaining about.
The good news is that once this is merged, you can probably import agda.packages.functional-linear-algebra and override its src to the local source.
There was a problem hiding this comment.
Shoot, I was hoping!
I copied over the default file from the repository and updated the src field.
Also reran the test with the new name:
nix-build -E "with import ./. {}; pkgs.agda.withPackages (p: with p; [ functional-linear-algebra ])"
ryanorendorff
changed the title
pkgs/top-level/agda-packages.nix
Outdated
| generic = callPackage ../development/libraries/agda/generic { }; | ||
|
|
There was a problem hiding this comment.
I guess that extra line is accidental 😅 can you remove it?
There was a problem hiding this comment.
Haha whoops! Fixed.
Adds the functional-linear-algebra library to the agda package set.
|
Rebased and squashed! |
|
This pull request has been mentioned on NixOS Discourse. There might be relevant details there: |
Adds the functional-linear-algebra library to the agda package set.
Tested using the following command from the root of the nixpkgs repo:
Addresses issue ryanorendorff/functional-linear-algebra#16 from the
flarepository.@turion Ready for your review!
Motivation for this change
Things done
sandboxinnix.confon non-NixOS linux)nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD"./result/bin/)nix path-info -Sbefore and after)