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
Conversation
pkgs/development/haskell-modules/configuration-hackage2nix.yaml
Outdated
Show resolved
Hide resolved
@@ -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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
This works, although it is possible that Also, However, it appears that I imagine you probably want to fix this, so I'd suggest sending a PR to the |
|
It is set in nixpkgs, because I imagine you'll have to send a PR to |
I had a look, it seems to use a custom license and has |
I'm not sure I understand, if |
I believe that
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 |
I'm not sure I'm being clear:
|
Huh, sorry, it looks like I was wrong about this. I was under the impression that having However, you're completely right that $ 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 However, it definitely has "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 |
It seems like the vast majority of haskell packages have |
@alexarice In general, all packages that are marked broken will have As far as I know, a package that is not marked broken, but does have I'm not surprised that I was wondering if @peti would have some idea why this is happening. |
To add to the confusion, I believe Agda isn't cached on arm. |
@cdepillabout, I believe Agda is being built on Hydra because
|
@peti, oh good find, I had no idea that that |
|
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 |
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
I'm not sure there is a good way to do this. I guess you could always do something like |
In the future, it would be good to maintain multiple
agdaPackages
sets along side different versions, like howcoq-packages
is set up. To do this we would need access to different versions of Agda. As a start I have tried to fix version2.6.1
ofAgda
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 anAgda_2_6_1
package which is fixed on2.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.