agdaPackages.standard-library: 1.7.3 -> 2.0

[ncfavier]

https://github.com/agda/agda-stdlib/blob/v2.0/CHANGELOG.md

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:
  • NixOS test(s) (look inside nixos/tests)
  • and/or package tests
  • or, for functions and "core" functionality, tests in lib/tests or pkgs/test
  • made sure NixOS tests are linked to the relevant packages
• 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.05 Release Notes (or backporting 23.05 and 23.11 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.

[turion]

@ofborg build agdaPackages.standard-library.passthru.tests

EDIT(@ncfavier): retrigger

[alexarice]

We should add the --include-deprecated flag on the call to GenerateEverything.hs. This means that if you use a deprecated module the warnings actually show up instead of giving an error about things not being built

[turion]

It seems that this would break agda-categories. Can we give them some time & warning to update their library before merging?

[turion]

Upstream issue is agda/agda-categories#405, if there is no progress in, say, a week or so, I'm happy to merge. But if there is some promising progress, I think we should bump both libraries jointly.

[alexarice]

It's worth noting that this version is a large non backwards compatible change

[ncfavier]

Sure, I wasn't planning to merge this right away. agdarsec and functional-linear-algebra are also failing; opened gallais/agdarsec#33 and ryanorendorff/functional-linear-algebra#50.

[ryanorendorff]

Updated the functional-linear-algebra package to work with the 2.0 version of the library. Thanks for the heads up.

[ncfavier]

Can confirm HEAD builds. Are you planning to make a new release or should we bump to HEAD?

[ryanorendorff]

Just pushed tag v0.5.0 (which is HEAD), so if that could be used that would be great. Thanks!

[alexarice]

agda-categories has a new release, so we can probably go ahead with this update now

[ncfavier]

Bumped agda-categories. No response from agdarsec, so we might as well mark it broken.

---

I had to increase the maximum heap for building agda-categories after the update. Weirdly enough, this is the third Agda project I know of that has recently started exceeding the maximum heap size (the other two being agda-unimath and 1lab), but this doesn't seem to be correlated to the Agda 2.6.4.1 bump... Does anyone have an explanation, or is this just a funny coincidence?

[turion]

Does anyone have an explanation, or is this just a funny coincidence?

It might be worth checking whether this is due to the recent agda version bump, the agda-stdlib version bump, or the agda-categories version bump. I have no explanation, though.

[alexarice]

Could it also be a ghc change? I always remember agda being happy to consume way more than 4gb ram