Skip to content

agda: 2.6.4.3 -> 2.7.0 (WIP)#335824

Closed
iblech wants to merge 1 commit intoNixOS:haskell-updatesfrom
iblech:patch-agda2.7.0
Closed

agda: 2.6.4.3 -> 2.7.0 (WIP)#335824
iblech wants to merge 1 commit intoNixOS:haskell-updatesfrom
iblech:patch-agda2.7.0

Conversation

@iblech
Copy link
Contributor

@iblech iblech commented Aug 19, 2024

Description of changes

Agda 2.7.0 has been released a couple of days ago. This pull request regenerates our Haskell package dataset to make Agda 2.7.0 available. Additionally to simply regenerating, this pull request comprises the following changes:

  • There is a version bump in configuration-common.nix so that the maintainer update scripts work.
  • agda-prelude and _1lab are marked as broken, as they fail compilation with Agda 2.7.0 ("No instance of type Prelude.Monad.Indexed.IMonad _M_211 was found in scope." and "Definition !=< Quantity → Definition when checking that the expression data-cons has type ...", respectively).
  • We cherry pick two commits from the experimental branch of the standard-library to render it compatible with Agda 2.7.0.

Merging this pull request should probably be hold off until a compatibility release 2.1.1 of the standard library has been published (thereby rendering the cherry picking superfluous).

You can test this pull request with:

$ nix-shell -I nixpkgs=https://github.com/iblech/nixpkgs/archive/patch-agda2.7.0.zip -p "agda.withPackages (p: [ p.standard-library p.functional-linear-algebra p.agda-categories p.generics p.cubical ])

Things done

  • Built on platform(s)
    • x86_64-linux
    • aarch64-linux
    • x86_64-darwin
    • aarch64-darwin
  • For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
    • sandbox = relaxed
    • sandbox = true
  • Tested, as applicable:
  • Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
  • Tested basic functionality of all binary files (usually in ./result/bin/)
  • 24.11 Release Notes (or backporting 23.11 and 24.05 Release notes)
    • (Package updates) Added a release notes entry if the change is major or breaking
    • (Module updates) Added a release notes entry if the change is significant
    • (Module addition) Added a release notes entry if adding a new NixOS module
  • Fits CONTRIBUTING.md.

Add a 👍 reaction to pull requests you find important.

@github-actions github-actions bot added 6.topic: haskell General-purpose, statically typed, purely functional programming language 6.topic: agda A dependently typed programming language / interactive theorem prover labels Aug 19, 2024
@iblech iblech changed the title agda: 2.6.4.1 -> 2.7.0 (WIP) agda: 2.6.4.3 -> 2.7.0 (WIP) Aug 19, 2024
@ofborg ofborg bot added 8.has: clean-up This PR removes packages or removes other cruft 8.has: package (new) This PR adds a new package 10.rebuild-darwin: 501+ This PR causes many rebuilds on Darwin and should normally target the staging branches. 10.rebuild-darwin: 2501-5000 This PR causes many rebuilds on Darwin and should target the staging branches. 10.rebuild-linux: 501+ This PR causes many rebuilds on Linux and should normally target the staging branches. 10.rebuild-linux: 2501-5000 This PR causes many rebuilds on Linux and should target the staging branches. labels Aug 19, 2024
@ncfavier
Copy link
Member

Merging this pull request should probably be hold off until a compatibility release 2.1.1 of the standard library has been published (thereby rendering the cherry picking superfluous).

Agda will update when #335932 is merged anyway, as always. I don't think we should hold up the Haskell merge cycle. Ideally, Agda updates would be handled separately from Hackage, but this has still not been implemented.

@ncfavier
Copy link
Member

1lab is handled by #336027, so AFAICT all that is left here is the changes to pkgs/development/libraries/agda/agda-prelude/default.nix and pkgs/development/libraries/agda/standard-library/default.nix.

@iblech
Copy link
Contributor Author

iblech commented Aug 21, 2024

Thank you for pointing to #335932! I agree that the new version of Agda should not hold up the Haskell merge cycle.

I'm closing this draft of a pull request in favor of the new #336351. Thank you for your review and your work on #336027 :-)

@iblech iblech closed this Aug 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

6.topic: agda A dependently typed programming language / interactive theorem prover 6.topic: haskell General-purpose, statically typed, purely functional programming language 8.has: clean-up This PR removes packages or removes other cruft 8.has: package (new) This PR adds a new package 10.rebuild-darwin: 501+ This PR causes many rebuilds on Darwin and should normally target the staging branches. 10.rebuild-darwin: 2501-5000 This PR causes many rebuilds on Darwin and should target the staging branches. 10.rebuild-linux: 501+ This PR causes many rebuilds on Linux and should normally target the staging branches. 10.rebuild-linux: 2501-5000 This PR causes many rebuilds on Linux and should target the staging branches.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants