Agda 2.6.4 migration #256
Agda 2.6.4 migration #256
Conversation
|
Yeah, the thing about the hashes is an anti-feature of nix. If nix finds something that has the hash you've provided, it doesn't actually check anything else - it just assumes it's the right thing (even if, for example, you change the version number which is literally right next to the hash). To get a proper error message, you can just change a few characters of the hash and it'll tell you what the correct one would be. Getting Agda 2.6.4 is slightly more complicated, because nixpkgs gets its Agda from Hackage, which means you can't just tell it what hash to use. I've done it before, so I'll just add a commit on top of your PR. |
|
Turns out that for some reason even the most recent Hackage update I could find in nixpkgs doesn't have Agda 2.6.4 (which is weird, they have a script for that and it ran less than a day ago). It also took a bit when we updated to 2.6.3. I think for now the strategy is to just wait, it shouldn't take too long. This is the one I found: NixOS/nixpkgs@dd81de3, the one that updates Agda will look similar to this one. |
|
I think this only fails because Agda isn't cached yet & takes forever to build. We were looking into getting the github action fetch from the IOG cache which gets populated by hydra, which should solve this problem. |
|
Apparently Agda 2.6.4 still isn't in unstable nixpkgs. I tried adding the IOG cache to our build, let's see if that'll fetch it. |
|
Looks good, I think in this case I'd let CI finish just to be sure |
WhatisRT
force-pushed
the
agda-2.6.4-migration
branch
from
992dbb3 to
39f7636
Compare
| @@ -79,7 +79,7 @@ module _ (let open Tx; open TxBody) where | |||
| outs tx = mapKeys (tx .txid ,_) (tx .txouts) | |||
|
|
|||
| balance : UTxO → Value | |||
| balance utxo = Σᵐᵛ[ x ← utxo ᶠᵐ ] getValue x | |||
| balance utxo = indexedSumᵐᵛ ⦃ Value-CommutativeMonoid ⦄ getValue (utxo ᶠᵐ) | |||
|
|
|||
| cbalance : UTxO → Coin | |||
| cbalance utxo = coin (balance utxo) | |||
There was a problem hiding this comment.
Did instance resolution become less useful in Agda 2.6.4, or is there another reason for these changes?
There was a problem hiding this comment.
This might be your fault 😂
agda/agda#6364
There was a problem hiding this comment.
The real problem is of course that using bundled monoids as a typeclass was a bad idea from the start. I think we should switch this to an unbundled version and then I'd expect this to work again.
There was a problem hiding this comment.
Yes, that's the very issue. I think switching to unbundled representations is the way to go.
| rev = "bdfab77b179c937856c49d72321ca26e2a27d568"; | ||
| sha256 = "+PMZjmMK5xz+3Va7RN1ErtQghzpUlzsc9JBUoL+iasc="; | ||
| rev = "cb72ba52dfbd4f83d1034e352eb88550a3e1f681"; | ||
| sha256 = "+OByLIWv+pdHvWt41hniE4oeo2DJZewRyYYmNXvCix0="; |
There was a problem hiding this comment.
Wouldn't it be more proper to depend on agda/agda-stdlib#v1.7.3 and just add the changes in the IOHK fork as .../Ext.agda files, namely:
- Unique seq equality = bag equality as file
Data/List/Relation/Unary/Unique/Propositional/Properties/WithK.agda - Non-normalising monoid solver as file
Tactic.MonoidSolver.Extwhich also re-exports the standardTactic.MonoidSolverassolve-normalisedandsolve-normalised-macro.
There was a problem hiding this comment.
I think it depends on the viewpoint. I'd like to get these in the actual stdlib at some point and in that case it's easier to do it like this.
| rev = "f434542c4baf667805161eeb35e5ec772233e180"; | ||
| sha256 = "e+gb3z+cTFW4QS0c/SQqnNVBxf9hGHKOZa/vSMkHDvw="; |
There was a problem hiding this comment.
I am hoping to release a 2.6.4-compatible stdlib-meta soon (also requested for another in-house product that uses stdlib-meta), but let's not block this now; I will simplify when the time comes.
* Make everything compile with Agda 2.6.4 * Update stdlib and stdlib-meta dependencies * Update nix to Agda 2.6.4 * Add IOG cache --------- Co-authored-by: whatisRT <[email protected]> add safe to options pragma
These are the minimal changes required to build with Agda 2.6.4.
I am clueless when it comes to nix, so I need some help:
default.nixbut it didn't complain about the sha256 hash being the same as before.