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

agdaPackages.standard-library: 1.3 -> 1.4 #98199

Merged
merged 3 commits into from Oct 22, 2020
Merged

Conversation

@turion
Copy link
Contributor

@turion turion commented Sep 18, 2020

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 wip"
  • 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.

CC: @alexarice @jwiegley

@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

@alexarice Do we have all agda libraries on CI? Or could it be that I accidentally break one this way?

@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

Indeed this broke the generic package. I'll try and update the agda test in a way that it would have caught this.

@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

This test now shows that generic doesn't build.

@ofborg ofborg bot added the 6.topic: nixos label Sep 18, 2020
@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

I don't understand why there is no CI failure. When I do nix-build nixos/tests/agda.nix, it fails with the error message described here:

effectfully/Generic#5

@alexarice
Copy link
Contributor

@alexarice alexarice commented Sep 18, 2020

CI doesn't run the tests by default. I'm also not sure building every agda package in the tests is a good idea.
Edit: Maybe CI has changed but it seems it is trying to run passthru.tests which we have not set I believe

Copy link
Contributor

@alexarice alexarice left a comment

I'd prefer not to modify the test here, and likely not in this way. I don't think anything else checks that all their packages build.

I think the three options here are:

  • Update standard library and mark everything broken
  • Don't update yet and wait for some things to catch up
  • Add a standard-library_1.3 package
@alexarice
Copy link
Contributor

@alexarice alexarice commented Sep 18, 2020

Given that my understanding is that it only breaks the one library, we could just go ahead

@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

I'd prefer not to modify the test here, and likely not in this way. I don't think anything else checks that all their packages build.

But we should add some test somewhere that builds all packages, do you agree? Where could such a test reside?

Don't update yet and wait for some things to catch up

I guess that's fine as well. As far as I could see, generic is the only package that failed, and it's probably fairly easy to fix.

Add a standard-library_1.3 package

I think that's a great option as well. I can make the standard library builder generic and call it twice, with both versions.

I'd go for first waiting a bit until all packages work with 1.4. It's an interesting experiment to see whether there is enough motivation in the community to stay coherent. If it works out fine, then great. If not, we can wonder about the other options.

@alexarice
Copy link
Contributor

@alexarice alexarice commented Sep 18, 2020

I'd prefer not to modify the test here, and likely not in this way. I don't think anything else checks that all their packages build.

But we should add some test somewhere that builds all packages, do you agree? Where could such a test reside?

I'm not sure it's usual to have a test like this, but if we did perhaps it should be a standard library test rather than an agda test

@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

I fixed generic here: effectfully/Generic#6

Maybe it gets released soon.

I'm not sure it's usual to have a test like this, but if we did perhaps it should be a standard library test rather than an agda test

I'm also not sure, but it doesn't seem wasteful to me. The packages need to be built anyways for the cache, and it would be nice to have some signal if something breaks. In Haskell, this is done by stackage. I'm imagining that nixpkgs could step in for the corresponding task in the Agda world. Given that it's just a handful curated packages, it seems feasible.

Anyways, I guess it's a separate issue. I opened one: #98209

@turion turion force-pushed the turion:dev_agda_stdlib_1.4 branch from e1e2d43 to 51bc6ec Sep 18, 2020
@umazalakain umazalakain mentioned this pull request Sep 18, 2020
3 of 10 tasks complete
@ofborg ofborg bot removed the 6.topic: nixos label Sep 18, 2020
@ofborg ofborg bot requested a review from alexarice Sep 18, 2020
@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

Indeed a pleasantly fast response, on generic. But agda-categories fails as well.

@alexarice
Copy link
Contributor

@alexarice alexarice commented Sep 18, 2020

This is unsurprising, and it took a bit of work to get a release last time

@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

Yes, they seem to have released it several times until they got it right. I think nixpkgs can help there because we can build one consistent package set.

@turion turion mentioned this pull request Sep 18, 2020
0 of 10 tasks complete
@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

With agda/agda-categories#207 merged all nonbroken packages should compile again.

@turion
Copy link
Contributor Author

@turion turion commented Sep 18, 2020

@alexarice Is it ok if the updated other packages (generic and agda-categories) don't have a release tag? Or should we only update them when they release a new version?

@ryanorendorff
Copy link
Contributor

@ryanorendorff ryanorendorff commented Oct 18, 2020

That's a good spot, is this change post 1.4?

Yes, it seems that starting at 1.5 and going forward they will have versioning in the package name.

@turion
Copy link
Contributor Author

@turion turion commented Oct 19, 2020

I think the name of the agda package here should not have a version number, i.e. it should be agdaPackages.agda-stdlib and not agdaPackages.agda-stdlib-1.4. The convention for the latter is that sometimes, old legacy versions or new preview versions are added. But the released, up-to-date version should not have a version number.

@alexarice
Copy link
Contributor

@alexarice alexarice commented Oct 19, 2020

We'll have to add libraryName = "${pname}-${version}" from next release onwards but I think this one is unaffected

@turion
Copy link
Contributor Author

@turion turion commented Oct 19, 2020

Let me re-evaluate which packages are broken, and mark them broken. Both agda-categories and Generic have released compatible versions, I'll update.

@turion turion force-pushed the turion:dev_agda_stdlib_1.4 branch from 0be69a1 to 7abe64b Oct 19, 2020
@turion
Copy link
Contributor Author

@turion turion commented Oct 19, 2020

No other packages are broken. I updated agda-stdlib, agda-categories, generic to latest released versions.

I believe we should merge this as-is, and not bump the other packages. That should be a separate MR, if at all necessary.

@turion
Copy link
Contributor Author

@turion turion commented Oct 19, 2020

/marvin opt-in
/status needs_reviewer

@marvin-mk2 marvin-mk2 bot added the marvin label Oct 19, 2020
@marvin-mk2
Copy link

@marvin-mk2 marvin-mk2 bot commented Oct 19, 2020

Hi! I'm an experimental bot. My goal is to guide this PR through its stages, hopefully ending with a merge. You can read up on the usage here.

@marvin-mk2 marvin-mk2 bot added the needs_reviewer label Oct 19, 2020
@alexarice
Copy link
Contributor

@alexarice alexarice commented Oct 19, 2020

I think this could all just be one commit really

@ofborg ofborg bot requested a review from alexarice Oct 19, 2020
@turion
Copy link
Contributor Author

@turion turion commented Oct 19, 2020

I always thought that separate package updates should be separate commits. Otherwise we can't follow the commit message format in https://github.com/NixOS/nixpkgs/blob/master/.github/CONTRIBUTING.md.

@alexarice
Copy link
Contributor

@alexarice alexarice commented Oct 19, 2020

I think there is a precedent for package sets that mutually break eachother being updated in one commit. See haskellPackages, emacsPackages etc. I don't mind too much either way though

Edit: These are updated automatically though

@turion
Copy link
Contributor Author

@turion turion commented Oct 19, 2020

Ah I didn't know. I prefer committing each update separately, tbh.

@alexarice
Copy link
Contributor

@alexarice alexarice commented Oct 19, 2020

Sure, can we rebase out the fix whitespace commit in any case

@turion turion force-pushed the turion:dev_agda_stdlib_1.4 branch from 7abe64b to 3da3661 Oct 19, 2020
@turion
Copy link
Contributor Author

@turion turion commented Oct 19, 2020

Sure, can we rebase out the fix whitespace commit in any case

Done.

Copy link
Contributor

@alexarice alexarice left a comment

Diff looks good, though my laptop is playing funny with nix-review so I can't really test it atm

@ofborg ofborg bot requested a review from alexarice Oct 19, 2020
@marvin-mk2
Copy link

@marvin-mk2 marvin-mk2 bot commented Oct 22, 2020

Reminder: Please review!

This Pull Request is awaiting review. If you are the assigned reviewer, please have a look. Try to find another reviewer if necessary. If you can't, please say so. If the status is not accurate, please change it. If nothing happens, this PR will be put back in the needs_reviewer queue in one day.

@nixos-discourse
Copy link

@nixos-discourse nixos-discourse commented Oct 22, 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/255

@kevincox kevincox merged commit 6c9d44d into NixOS:master Oct 22, 2020
19 checks passed
19 checks passed
tests
Details
action
Details
agdaPackages.agda-categories, agdaPackages.agda-categories.passthru.tests, agdaPackages.generic, agdaPackages.generic.passthru.tests, agdaPackages.standard-library, agdaPackages.standard-library.passthru.tests on aarch64-linux Failure
Details
agdaPackages.agda-categories, agdaPackages.agda-categories.passthru.tests, agdaPackages.generic, agdaPackages.generic.passthru.tests, agdaPackages.standard-library, agdaPackages.standard-library.passthru.tests on x86_64-linux Unexpected error: command failed with exit code 1
Details
Evaluation Performance Report Evaluator Performance Report
Details
Wait for ofborg
Details
grahamcofborg-eval ^.^!
Details
grahamcofborg-eval-check-maintainers matching changed paths to changed attrs...
Details
grahamcofborg-eval-check-meta config.nix: checkMeta = true
Details
grahamcofborg-eval-darwin nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="3da3661"; rev="3da3661ad3615912738a4dcb769f1672f463f0dc"; } ./pkgs/t
Details
grahamcofborg-eval-lib-tests nix-build --arg pkgs import ./. {} ./lib/tests/release.nix
Details
grahamcofborg-eval-nixos nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="3da3661"; rev="3da3661ad3615912738a4dcb769f1672f463f0dc"; } ./nixos/
Details
grahamcofborg-eval-nixos-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="3da3661"; rev="3da3661ad3615912738a4dcb769f1672f463f0dc"; } ./nixos/
Details
grahamcofborg-eval-nixos-options nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="3da3661"; rev="3da3661ad3615912738a4dcb769f1672f463f0dc"; } ./nixos/
Details
grahamcofborg-eval-nixpkgs-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="3da3661"; rev="3da3661ad3615912738a4dcb769f1672f463f0dc"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-tarball nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="3da3661"; rev="3da3661ad3615912738a4dcb769f1672f463f0dc"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-unstable-jobset nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="3da3661"; rev="3da3661ad3615912738a4dcb769f1672f463f0dc"; } ./pkgs/t
Details
grahamcofborg-eval-package-list nix-env -qa --json --file .
Details
grahamcofborg-eval-package-list-no-aliases nix-env -qa --json --file . --arg config { allowAliases = false; }
Details
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

5 participants
You can’t perform that action at this time.