From 94f7e06670bbf277328393f5b8e3d9c87746cd1d Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Fri, 20 Oct 2023 08:31:53 +0200 Subject: [PATCH 1/4] Make everything compile with Agda 2.6.4 --- src/Ledger/Epoch.agda | 4 ++-- src/Ledger/Gov.lagda | 6 +++--- src/Ledger/PPUp/Properties.agda | 8 ++++---- src/Ledger/Utxo.lagda | 6 +++--- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Ledger/Epoch.agda b/src/Ledger/Epoch.agda index 4e8e72d4a..b7a878e6b 100644 --- a/src/Ledger/Epoch.agda +++ b/src/Ledger/Epoch.agda @@ -29,8 +29,8 @@ record EpochStructure : Set₁ where preoEpoch = hasPreorderFromStrictPartialOrder {_<_ = _<_ on firstSlot} record { isEquivalence = isEquivalence - ; irrefl = λ where refl → <-irrefl refl - ; trans = <-trans + ; irrefl = λ where refl → <-irrefl {A = Slot} refl + ; trans = <-trans {A = Slot} ; <-resp-≈ = (λ where refl → id) , (λ where refl → id) } diff --git a/src/Ledger/Gov.lagda b/src/Ledger/Gov.lagda index 29464382f..6a58f7304 100644 --- a/src/Ledger/Gov.lagda +++ b/src/Ledger/Gov.lagda @@ -154,9 +154,9 @@ instance (yesᵈ (wf , dep) , noᵈ notNewComm) → just (_ , GOV-Propose wf dep λ isNewComm → ⊥-elim (notNewComm (_ , _ , _ , isNewComm))) _ → nothing Computational-GOV' .completeness (⟦ _ , _ , pparams ⟧ᵗ , k) s (inj₁ record { gid = aid ; role = role }) s' (GOV-Vote mem cV) - with lookupActionId pparams role aid s | "agda#6868" - ... | noᵈ ¬p | _ = ⊥-elim (¬p (⤖⇒ (fromRelated Any↔) .to (_ , ∈-fromList .from mem , refl , cV))) - ... | yesᵈ p | _ with ⤖⇒ (fromRelated Any↔) .from p + with lookupActionId pparams role aid s + ... | noᵈ ¬p = ⊥-elim (¬p (⤖⇒ (fromRelated Any↔) .to (_ , ∈-fromList .from mem , refl , cV))) + ... | yesᵈ p with ⤖⇒ (fromRelated Any↔) .from p ... | (_ , mem , refl , cV) = refl Computational-GOV' .completeness (⟦ _ , epoch , pparams ⟧ᵗ , k) s (inj₂ record { action = a ; deposit = d }) s' (GOV-Propose wf dep newOk) with ¿ actionWellFormed a ≡ true × d ≡ pparams .PParams.govActionDeposit ¿ | isNewCommittee a diff --git a/src/Ledger/PPUp/Properties.agda b/src/Ledger/PPUp/Properties.agda index 3750ca578..0a3d89559 100644 --- a/src/Ledger/PPUp/Properties.agda +++ b/src/Ledger/PPUp/Properties.agda @@ -44,7 +44,7 @@ instance Computational-PPUP .completeness Γ _ (just up) _ _ | PPUpdateCurrent p₁ p₂ p₃ p₄ rewrite dec-yes ¿ Current-Property Γ up ¿ (p₁ , p₂ , p₃ , p₄) .proj₂ = refl Computational-PPUP .completeness Γ _ (just up) _ _ | PPUpdateFuture p₁ p₂ p₃ p₄ - with ¿ Current-Property Γ up ¿ | ¿ Future-Property Γ up ¿ | "agda#6868" - ... | yes (_ , _ , ¬p₃ , _) | _ | _ = ⊥-elim $ <⇒¬>⊎≈ ¬p₃ (≤⇔<∨≈ .Equivalence.to p₃) - ... | no _ | yes p | _ = refl - ... | no _ | no ¬p | _ = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄)) + with ¿ Current-Property Γ up ¿ | ¿ Future-Property Γ up ¿ + ... | yes (_ , _ , ¬p₃ , _) | _ = ⊥-elim $ <⇒¬>⊎≈ {A = Slot} ¬p₃ (≤⇔<∨≈ .Equivalence.to p₃) + ... | no _ | yes p = refl + ... | no _ | no ¬p = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄)) diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index 8427fa5bb..57d855152 100644 --- a/src/Ledger/Utxo.lagda +++ b/src/Ledger/Utxo.lagda @@ -30,7 +30,7 @@ instance _ = ExUnit-CommutativeMonoid HasCoin-Map : ∀ {A} → ⦃ DecEq A ⦄ → HasCoin (A ⇀ Coin) - HasCoin-Map .getCoin s = Σᵐᵛ[ x ← s ᶠᵐ ] x + HasCoin-Map .getCoin s = indexedSumᵐᵛ ⦃ +-0-commutativeMonoid ⦄ id (s ᶠᵐ) isPhaseTwoScriptAddress : Tx → Addr → Bool isPhaseTwoScriptAddress tx a @@ -42,7 +42,7 @@ isPhaseTwoScriptAddress tx a ... | just s = isP2Script s totExUnits : Tx → ExUnits -totExUnits tx = Σᵐ[ x ← tx .wits .txrdmrs ᶠᵐ ] (x .proj₂ .proj₂) +totExUnits tx = indexedSumᵐ ⦃ ExUnit-CommutativeMonoid ⦄ (λ x → x .proj₂ .proj₂) (tx .wits .txrdmrs ᶠᵐ) where open Tx; open TxWitnesses -- utxoEntrySizeWithoutVal = 27 words (8 bytes) @@ -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) From 7976fbc5dcf8d203e0657875e8933619205dec24 Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Fri, 20 Oct 2023 08:47:26 +0200 Subject: [PATCH 2/4] Update stdlib and stdlib-meta dependencies --- default.nix | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/default.nix b/default.nix index cb355722f..474f01759 100644 --- a/default.nix +++ b/default.nix @@ -16,7 +16,7 @@ let src = fetchFromGitHub { repo = "agda-stdlib"; owner = "input-output-hk"; - rev = "bdfab77b179c937856c49d72321ca26e2a27d568"; + rev = "cb72ba52dfbd4f83d1034e352eb88550a3e1f681"; sha256 = "+PMZjmMK5xz+3Va7RN1ErtQghzpUlzsc9JBUoL+iasc="; }; }); @@ -27,7 +27,7 @@ let src = fetchFromGitHub { repo = "stdlib-meta"; owner = "input-output-hk"; - rev = "897555aefd77c83e88492255641da3bcc4879461"; + rev = "f434542c4baf667805161eeb35e5ec772233e180"; sha256 = "EIKcLjGdnI/6nSCI18v7kPxoojAWsz8O5d9wwol2M0w="; }; meta = { }; From edce8959650b753730ec036b2d09667c118a98ff Mon Sep 17 00:00:00 2001 From: whatisRT Date: Mon, 23 Oct 2023 15:00:03 +0200 Subject: [PATCH 3/4] Update nix to Agda 2.6.4 --- default.nix | 4 +- nix/sources.json | 6 +-- nix/sources.nix | 114 ++++++++++++++++++++++++----------------------- 3 files changed, 64 insertions(+), 60 deletions(-) diff --git a/default.nix b/default.nix index 474f01759..78d81d640 100644 --- a/default.nix +++ b/default.nix @@ -17,7 +17,7 @@ let repo = "agda-stdlib"; owner = "input-output-hk"; rev = "cb72ba52dfbd4f83d1034e352eb88550a3e1f681"; - sha256 = "+PMZjmMK5xz+3Va7RN1ErtQghzpUlzsc9JBUoL+iasc="; + sha256 = "+OByLIWv+pdHvWt41hniE4oeo2DJZewRyYYmNXvCix0="; }; }); @@ -28,7 +28,7 @@ let repo = "stdlib-meta"; owner = "input-output-hk"; rev = "f434542c4baf667805161eeb35e5ec772233e180"; - sha256 = "EIKcLjGdnI/6nSCI18v7kPxoojAWsz8O5d9wwol2M0w="; + sha256 = "e+gb3z+cTFW4QS0c/SQqnNVBxf9hGHKOZa/vSMkHDvw="; }; meta = { }; libraryFile = "stdlib-meta.agda-lib"; diff --git a/nix/sources.json b/nix/sources.json index f02526e16..15400a143 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -5,10 +5,10 @@ "homepage": "", "owner": "NixOS", "repo": "nixpkgs", - "rev": "8276a165b9fa3db1a7a4f29ee29b680e0799b9dc", - "sha256": "1157f8p4lvywglcb8spwk2qwcnzs6000cqyx5s9bnkj6zmwjpqwx", + "rev": "caf1c4efda9aac9b6b8437d4c8c89c927dcaebee", + "sha256": "1v5cgnbxickfsck8jiwbmhkjbkw0iy09lam0g04jwg2yw0llqxj2", "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/8276a165b9fa3db1a7a4f29ee29b680e0799b9dc.tar.gz", + "url": "https://github.com/NixOS/nixpkgs/archive/caf1c4efda9aac9b6b8437d4c8c89c927dcaebee.tar.gz", "url_template": "https://github.com///archive/.tar.gz" }, "nixpkgs": { diff --git a/nix/sources.nix b/nix/sources.nix index 9a01c8acf..fe3dadf7e 100644 --- a/nix/sources.nix +++ b/nix/sources.nix @@ -10,33 +10,34 @@ let let name' = sanitizeName name + "-src"; in - if spec.builtin or true then - builtins_fetchurl { inherit (spec) url sha256; name = name'; } - else - pkgs.fetchurl { inherit (spec) url sha256; name = name'; }; + if spec.builtin or true then + builtins_fetchurl { inherit (spec) url sha256; name = name'; } + else + pkgs.fetchurl { inherit (spec) url sha256; name = name'; }; fetch_tarball = pkgs: name: spec: let name' = sanitizeName name + "-src"; in - if spec.builtin or true then - builtins_fetchTarball { name = name'; inherit (spec) url sha256; } - else - pkgs.fetchzip { name = name'; inherit (spec) url sha256; }; + if spec.builtin or true then + builtins_fetchTarball { name = name'; inherit (spec) url sha256; } + else + pkgs.fetchzip { name = name'; inherit (spec) url sha256; }; fetch_git = name: spec: let ref = - if spec ? ref then spec.ref else + spec.ref or ( if spec ? branch then "refs/heads/${spec.branch}" else - if spec ? tag then "refs/tags/${spec.tag}" else - abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!"; - submodules = if spec ? submodules then spec.submodules else false; + if spec ? tag then "refs/tags/${spec.tag}" else + abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!" + ); + submodules = spec.submodules or false; submoduleArg = let nixSupportsSubmodules = builtins.compareVersions builtins.nixVersion "2.4" >= 0; emptyArgWithWarning = - if submodules == true + if submodules then builtins.trace ( @@ -44,15 +45,15 @@ let + "but your nix's (${builtins.nixVersion}) builtins.fetchGit " + "does not support them" ) - {} - else {}; + { } + else { }; in - if nixSupportsSubmodules - then { inherit submodules; } - else emptyArgWithWarning; + if nixSupportsSubmodules + then { inherit submodules; } + else emptyArgWithWarning; in - builtins.fetchGit - ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg); + builtins.fetchGit + ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg); fetch_local = spec: spec.path; @@ -86,16 +87,16 @@ let hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath; hasThisAsNixpkgsPath = == ./.; in - if builtins.hasAttr "nixpkgs" sources - then sourcesNixpkgs - else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then - import {} - else - abort - '' - Please specify either (through -I or NIX_PATH=nixpkgs=...) or - add a package called "nixpkgs" to your sources.json. - ''; + if builtins.hasAttr "nixpkgs" sources + then sourcesNixpkgs + else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then + import { } + else + abort + '' + Please specify either (through -I or NIX_PATH=nixpkgs=...) or + add a package called "nixpkgs" to your sources.json. + ''; # The actual fetching function. fetch = pkgs: name: spec: @@ -115,13 +116,13 @@ let # the path directly as opposed to the fetched source. replace = name: drv: let - saneName = stringAsChars (c: if isNull (builtins.match "[a-zA-Z0-9]" c) then "_" else c) name; + saneName = stringAsChars (c: if (builtins.match "[a-zA-Z0-9]" c) == null then "_" else c) name; ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}"; in - if ersatz == "" then drv else - # this turns the string into an actual Nix path (for both absolute and - # relative paths) - if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}"; + if ersatz == "" then drv else + # this turns the string into an actual Nix path (for both absolute and + # relative paths) + if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}"; # Ports of functions for older nix versions @@ -132,7 +133,7 @@ let ); # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295 - range = first: last: if first > last then [] else builtins.genList (n: first + n) (last - first + 1); + range = first: last: if first > last then [ ] else builtins.genList (n: first + n) (last - first + 1); # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257 stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1)); @@ -143,43 +144,46 @@ let concatStrings = builtins.concatStringsSep ""; # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331 - optionalAttrs = cond: as: if cond then as else {}; + optionalAttrs = cond: as: if cond then as else { }; # fetchTarball version that is compatible between all the versions of Nix builtins_fetchTarball = { url, name ? null, sha256 }@attrs: let inherit (builtins) lessThan nixVersion fetchTarball; in - if lessThan nixVersion "1.12" then - fetchTarball ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; })) - else - fetchTarball attrs; + if lessThan nixVersion "1.12" then + fetchTarball ({ inherit url; } // (optionalAttrs (name != null) { inherit name; })) + else + fetchTarball attrs; # fetchurl version that is compatible between all the versions of Nix builtins_fetchurl = { url, name ? null, sha256 }@attrs: let inherit (builtins) lessThan nixVersion fetchurl; in - if lessThan nixVersion "1.12" then - fetchurl ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; })) - else - fetchurl attrs; + if lessThan nixVersion "1.12" then + fetchurl ({ inherit url; } // (optionalAttrs (name != null) { inherit name; })) + else + fetchurl attrs; # Create the final "sources" from the config mkSources = config: - mapAttrs ( - name: spec: - if builtins.hasAttr "outPath" spec - then abort - "The values in sources.json should not have an 'outPath' attribute" - else - spec // { outPath = replace name (fetch config.pkgs name spec); } - ) config.sources; + mapAttrs + ( + name: spec: + if builtins.hasAttr "outPath" spec + then + abort + "The values in sources.json should not have an 'outPath' attribute" + else + spec // { outPath = replace name (fetch config.pkgs name spec); } + ) + config.sources; # The "config" used by the fetchers mkConfig = { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null - , sources ? if isNull sourcesFile then {} else builtins.fromJSON (builtins.readFile sourcesFile) + , sources ? if sourcesFile == null then { } else builtins.fromJSON (builtins.readFile sourcesFile) , system ? builtins.currentSystem , pkgs ? mkPkgs sources system }: rec { @@ -191,4 +195,4 @@ let }; in -mkSources (mkConfig {}) // { __functor = _: settings: mkSources (mkConfig settings); } +mkSources (mkConfig { }) // { __functor = _: settings: mkSources (mkConfig settings); } From 39f7636f20cc6847faeeb330f3e5eb9a420a0193 Mon Sep 17 00:00:00 2001 From: whatisRT Date: Tue, 31 Oct 2023 18:26:24 +0100 Subject: [PATCH 4/4] Add IOG cache --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 9ce1fdda1..7bff907b1 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -34,7 +34,7 @@ jobs: nix_path: nixpkgs=channel:nixos-unstable extra_nix_config: | trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= - substituters = https://cache.nixos.org/ + substituters = https://cache.iog.io https://cache.nixos.org/ - name: Restore store id: cache-store-restore