Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

agda-packages: add functional-linear-algebra library at v0.1 #100466

Merged
merged 1 commit into from Oct 15, 2020

Conversation

@ryanorendorff
Copy link
Contributor

@ryanorendorff ryanorendorff commented Oct 14, 2020

Adds the functional-linear-algebra library to the agda package set.

Tested using the following command from the root of the nixpkgs repo:

nix-build -E "with import ./. {}; pkgs.agda.withPackages (p: with p; [ functional-linear-algebra ])"

Addresses issue ryanorendorff/functional-linear-algebra#16 from the fla repository.

@turion Ready for your review!

Motivation for this change
Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
  • Built on platform(s)
    • NixOS
    • macOS
    • other Linux distributions
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Determined the impact on package closure size (by running nix path-info -S before and after)
  • Ensured that relevant documentation is up to date
  • Fits CONTRIBUTING.md.
@@ -26,5 +26,8 @@ let
cubical = callPackage ../development/libraries/agda/cubical { };

generic = callPackage ../development/libraries/agda/generic { };

fla = callPackage
Copy link
Contributor

@turion turion Oct 14, 2020

Why not call it functional-linear-algebra?

Copy link
Contributor Author

@ryanorendorff ryanorendorff Oct 14, 2020

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:
Copy link
Contributor

@turion turion Oct 14, 2020

Can you use a similar format to the other Agda libraries? Starting with { pkgs, usually. You can then inherit (pkgs) fetchFromGitHub I believe.

Copy link
Contributor Author

@ryanorendorff ryanorendorff Oct 14, 2020

Done!

sha256 = "09ri3jmgp9jjwi1mzv4c3w6rvcmyx6spa2qxpwlcn0f4bmfva6wm";
};

in import src
Copy link
Contributor

@turion turion Oct 14, 2020

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.

Copy link
Contributor Author

@ryanorendorff ryanorendorff Oct 14, 2020

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 ryanorendorff changed the title agda-packages: add fla library at v0.1 agda-packages: add functional-linear-algebra library at v0.1 Oct 14, 2020
Copy link
Contributor

@turion turion left a comment

The CI passes, I guess that means it's much happier about the inlined definition. Just a minor whitespace fix. Also, can you rebase and squash your commits at the end?

Builds for me.

generic = callPackage ../development/libraries/agda/generic { };

Copy link
Contributor

@turion turion Oct 15, 2020

I guess that extra line is accidental 😅 can you remove it?

Copy link
Contributor Author

@ryanorendorff ryanorendorff Oct 15, 2020

Haha whoops! Fixed.

Adds the functional-linear-algebra library to the agda package set.
@ryanorendorff ryanorendorff force-pushed the agda-functional-linear-algebra branch from 40a70c9 to c78dc9c Oct 15, 2020
@ryanorendorff
Copy link
Contributor Author

@ryanorendorff ryanorendorff commented Oct 15, 2020

Rebased and squashed!

turion
turion approved these changes Oct 15, 2020
Copy link
Contributor

@turion turion left a comment

Thanks a lot!

@nixos-discourse
Copy link

@nixos-discourse nixos-discourse commented Oct 15, 2020

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/prs-already-reviewed/2617/247

@Lassulus Lassulus merged commit 8b4d70c into NixOS:master Oct 15, 2020
17 checks passed
@ryanorendorff ryanorendorff deleted the agda-functional-linear-algebra branch Oct 15, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

4 participants