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: Fix haskell version 2.6.1 #90143

Merged
merged 1 commit into from Jun 12, 2020

Conversation

alexarice
Copy link
Contributor

In the future, it would be good to maintain multiple agdaPackages sets along side different versions, like how coq-packages is set up. To do this we would need access to different versions of Agda. As a start I have tried to fix version 2.6.1 of Agda so that the current package set can be fixed to this version and won't break when another version comes out.

My understanding is that this will make an Agda package which follows the latest version, and an Agda_2_6_1 package which is fixed on 2.6.1. Apologies if what I have done in this PR does not do this or if there is a better way to achieve this.

@@ -2537,6 +2537,7 @@ default-package-overrides:

extra-packages:
- aeson < 0.8 # newer versions don't work with GHC 7.6.x or earlier
- Agda == 2.6.1 # allows agdaPackages to depend on a fixed version
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cause still is not understandable, it is not reached in the explanation.

Contributors still do not know the cause. Maybe there was some particular quirk issue and because of it agda was fixed.

As you said in the Report text: "so that the current package set can be fixed to this version and won't break when another version comes out.", pretty good explanation.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was trying not to make it too long but I guess this doesn't matter

@cdepillabout
Copy link
Member

cdepillabout commented Jun 12, 2020

This works, although it is possible that Agda-2.6.1 will stop building due to updates to its dependent Haskell packages. You'll have to keep an eye on this in the future.

Also, Agda-2.6.1 is building for me, so I will merge this in.

However, it appears that cabal2nix can't figure out the license for Agda, so Hydra is not building Agda. This will be quite inconvenient for anyone who actually wants to use Agda from nixpkgs. (If you look at the output of cabal2nix cabal://Agda-2.6.1, you can see that hydraPlatforms is set to []. My guess is that this is because the license is set to unknown.)

I imagine you probably want to fix this, so I'd suggest sending a PR to the cabal2nix repo sorting out this licensing issue. I'm not sure whether you need upstream to specify the license correctly in the cabal file, or you need to teach cabal2nix about the nixpkgs license, or you need to add an additional license here in nixpkgs. If you can't figure out which of these is necessary, please ping me and I will help you look into it.

@cdepillabout cdepillabout merged commit 578d5ae into NixOS:haskell-updates Jun 12, 2020
@alexarice
Copy link
Contributor Author

cabal2nix cabal://Agda also has hydraPlatforms = stdenv.lib.platforms.none; so I expect this is set somewhere in nixpkgs. I'll have a look

@cdepillabout
Copy link
Member

I expect this is set somewhere in nixpkgs. I'll have a look

It is set in nixpkgs, because hackage2nix is used to generate the hackage-packages.nix (or whatever the name is) file, which internally uses cabal2nix.

I imagine you'll have to send a PR to cabal2nix to fix this. (Or maybe make sure a known license is used in the upstream Agda.cabal file?)

@alexarice
Copy link
Contributor Author

I had a look, it seems to use a custom license and has OtherLicense in its cabal file

@alexarice
Copy link
Contributor Author

I'm not sure I understand, if Agda has hydraPlatforms = [] then surely that isn't being fixed in cabal2nix.

@cdepillabout
Copy link
Member

I'm not sure I understand, if Agda has hydraPlatforms = [] then surely that isn't being fixed in cabal2nix.

I believe that cabal2nix is the codebase that has the logic that sets hydraPlatforms to [] if the license is OtherLicense.

I had a look, it seems to use a custom license and has OtherLicense in its cabal file

I believe the correct solution here is to add the license to the list of known licenses here in nixpkgs, and then send a PR to cabal2nix that adds a special case to to the Agda package to use that license.

@alexarice
Copy link
Contributor Author

I'm not sure I'm being clear:

  • Agda-2.6.1 has hydraPlatforms = []
  • Agda (as currently in nixpkgs) also has hydraPlatforms = [] set by cabal2nix
  • Agda is build by hydra
  • Why does something special need to be done for Agda-2.6.1?

@cdepillabout
Copy link
Member

Huh, sorry, it looks like I was wrong about this.

I was under the impression that having hydraPlatforms = [] would cause Hydra to not build your package.

However, you're completely right that Agda is being built by Hydra.

$ git clone ...nixpkgs...
$ cd nixpkgs
$ nix-store --query --outputs $(nix-instantiate -A haskellPackages.Agda)
/nix/store/hhmwwvhv6cc2wg6kcbcqnrqns8211vl9-Agda-2.6.1-data
/nix/store/5dxg14cbr1y56mplp2vw9yz3357hipsn-Agda-2.6.1-doc
/nix/store/hjzx97m5l9l3ba80335k0iycvm6d6hzs-Agda-2.6.1
$ nix path-info --json --store https://cache.nixos.org/ /nix/store/hjzx97m5l9l3ba80335k0iycvm6d6hzs-Agda-2.6.1 | jq
[
  {
    "path": "/nix/store/hjzx97m5l9l3ba80335k0iycvm6d6hzs-Agda-2.6.1",
    "narHash": "sha256:1rz0yzj7y3znwhm0p9dy6v98fqlc608lr2jgrh7fvm9fp918fqgq",
    "narSize": 1246969976,
    "references": [
      "/nix/store/06655sar8phm0i83j2j9yl9xidxhiiv7-regex-base-0.94.0.0",
      "/nix/store/0w4lcn6i0wn6i8c5gi80xl3gr6c24qz7-hashtables-1.2.3.4",
      ...
      "/nix/store/vrddk9p422y272i7k772ig8npii49h3l-STMonadTrans-0.4.4",
      "/nix/store/y18bhdg3snpwcwbxaah57sygpj4pj1hw-aeson-1.4.7.1"
    ],
    "deriver": "/nix/store/8ynwb2s0c8320syn26r203hanqwvq2y7-Agda-2.6.1.drv",
    "signatures": [
      "cache.nixos.org-1:wgy4gA463XRRX/SDlR1cSOTcUO5OF19/T2u9m1jxVbm+s6PXx5uUwM6tH4bVgfJsdjfIg6lPUMV1hh0uwt6ZAA=="
    ],
    "url": "nar/151w2jdmkq7jhg36xdrxkfnm6qaylbfs4xb4q1934166xbf4lg3l.nar.xz",
    "downloadHash": "sha256:151w2jdmkq7jhg36xdrxkfnm6qaylbfs4xb4q1934166xbf4lg3l",
    "downloadSize": 85050812
  }
]

So haskellPackages.Agda is definitely being built by Hydra.

However, it definitely has hydraPlatforms = []. The following is taken from hackage-packages.nix:

  "Agda" = callPackage
    ({ mkDerivation, aeson, alex, array, async, base, binary
     , blaze-html, boxes, bytestring, Cabal, containers, data-hash
     , deepseq, directory, edit-distance, emacs, equivalence, exceptions
     , filepath, geniplate-mirror, ghc-compact, gitrev, happy, hashable
     , hashtables, haskeline, ieee754, mtl, murmur-hash, pretty, process
     , regex-tdfa, split, stm, strict, template-haskell, text, time
     , transformers, unordered-containers, uri-encode, zlib
     }:
     mkDerivation {
       pname = "Agda";
       version = "2.6.1";
       sha256 = "0af1nyyscdc4gr4l0k3ayq3rn8qxqkx1b7rh4mw023gkz1m433v7";
       isLibrary = true;
       isExecutable = true;
       enableSeparateDataOutput = true;
       setupHaskellDepends = [ base Cabal directory filepath process ];
       libraryHaskellDepends = [
         aeson array async base binary blaze-html boxes bytestring
         containers data-hash deepseq directory edit-distance equivalence
         exceptions filepath geniplate-mirror ghc-compact gitrev hashable
         hashtables haskeline ieee754 mtl murmur-hash pretty process
         regex-tdfa split stm strict template-haskell text time transformers
         unordered-containers uri-encode zlib
       ];
       libraryToolDepends = [ alex happy ];
       executableHaskellDepends = [ base directory filepath process ];
       executableToolDepends = [ emacs ];
       postInstall = ''
         files=("$data/share/ghc-"*"/"*"-ghc-"*"/Agda-"*"/lib/prim/Agda/"{Primitive.agda,Builtin"/"*.agda})
         for f in "''${files[@]}" ; do
           $out/bin/agda $f
         done
         for f in "''${files[@]}" ; do
           $out/bin/agda -c --no-main $f
         done
         $out/bin/agda-mode compile
       '';
       description = "A dependently typed functional programming language and proof assistant";
       license = "unknown";
       hydraPlatforms = stdenv.lib.platforms.none;
       maintainers = with stdenv.lib.maintainers; [ abbradar ];
     }) {inherit (pkgs) emacs;};

@peti do you know why this would be happening? I was pretty sure that when hydraPlatforms = stdenv.lib.platforms.none, the package wouldn't built by Hydra.

@alexarice
Copy link
Contributor Author

It seems like the vast majority of haskell packages have hydraPlatforms = []

@cdepillabout
Copy link
Member

cdepillabout commented Jun 12, 2020

@alexarice In general, all packages that are marked broken will have hydraPlatforms = []. Packages that are not marked broken will have hydraPlatforms not specified (unless they can only be built on darwin or linux or something).

As far as I know, a package that is not marked broken, but does have hydraPlatforms = [], should not be built by Hydra.

I'm not surprised that Agda has hydraPlatforms = [], since its license is "unknown", but I am surprised that it is being built by Hydra.

I was wondering if @peti would have some idea why this is happening.

@alexarice
Copy link
Contributor Author

To add to the confusion, I believe Agda isn't cached on arm.

@peti
Copy link
Member

peti commented Jun 17, 2020

@cdepillabout, I believe Agda is being built on Hydra because pkgs/top-level/release.nix lists it explicitly:

agdaPackages = packagePlatforms pkgs.agdaPackages;

@cdepillabout
Copy link
Member

@peti, oh good find, I had no idea that that adgaPackages existed, or that it would force Hydra to build Agda.

@alexarice
Copy link
Contributor Author

agdaPackages is quite new, though Agda was definitely build by hydra before it's introduction

@alexarice
Copy link
Contributor Author

Sorry to resurrect this thread but I'm not sure where the best place to ask is. My understanding is that that this change would introduce a new Agda_2_6_1 attribute, though this doesn't seem to have happened. Is this because the current version is 2.6.1 so it doesn't make a duplicate? In any case, is there any way to get an alias for 2.6.1 which won't break when 2.6.2 comes out?

@cdepillabout
Copy link
Member

Is this because the current version is 2.6.1 so it doesn't make a duplicate?

I think this is what is happening. If you don't think this should be the case, then you can open an issue on the cabal2nix repo, which contains the program hackage2nix, which is responsible for this.

In any case, is there any way to get an alias for 2.6.1 which won't break when 2.6.2 comes out?

I'm not sure there is a good way to do this.

I guess you could always do something like haskellPackages.Agda_2_6_1 or haskellPackages.Agda.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants