From b1672f15ec02b60388b31ab3e72c954d5fd80478 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 6 Mar 2025 13:48:58 +0100 Subject: [PATCH] Use the nix flake to provide formal-ledger-specifications SRP (#4912) * Use flake to provide SRP * Replace instructions in `cabal.project` by pointer to CONTRIBUTING.md --- CONTRIBUTING.md | 11 ++++++----- cabal.project | 28 +++------------------------- flake.lock | 17 +++++++++++++++++ flake.nix | 6 ++++++ 4 files changed, 32 insertions(+), 30 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 510e256dcd0..1a8703c02f2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -295,11 +295,12 @@ To update the version of the Agda spec that the conformance tests are using: 1. Locate the `MAlonzo-code` branch in the [formal-ledger-specifications repo](https://github.com/IntersectMBO/formal-ledger-specifications) 2. Identify the SHA of the commit that you need, belonging to that branch -3. In the `cardano-ledger` repository, update the `cabal.project` file by replacing the `tag` and `sha256` fields in the `source-repository-package` stanza with the appropriate values. - -You can determine the correct `sha256` like this: - * update the `tag` with the SHA of the chosen commit and run `cabal`. The resulting error message will include the expected `sha256` value. - * alternatively, use a tool like `nix-prefetch-git` to fetch and compute the `sha256` +3. In the `cardano-ledger` repository: + - Update the `cabal.project` file by replacing the `tag` field in the `source-repository-package` stanza with SHA. + - Update the `flake.lock`: + ```shell + nix flake update formal-ledger-specifications --override-input formal-ledger-specifications github:IntersectMBO/formal-ledger-specifications/SHA + ``` If the commit you need in `formal-ledger-specifications` is not on master, open a PR for your branch in the `formal-ledger-specifications` repository. This will create a branch with the updated generated code, which you can then use as described above. You will not be able to merge in `cardano-leder` master a reference to a commit not yet merged in `formal-ledger-specifications`. diff --git a/cabal.project b/cabal.project index e647e8e8227..ecb80b8f444 100644 --- a/cabal.project +++ b/cabal.project @@ -10,38 +10,16 @@ repository cardano-haskell-packages c00aae8461a256275598500ea0e187588c35a5d5d7454fb57eac18d9edb86a56 d4a35cd3121aa00d18544bb0ac01c3e1691d618f462c46129271bccf39f7e8ee --- While using SRPs one can obtain the `--sha256` value for a package --- by first setting it to some random value and letting the tooling --- tell you what it should be, for example, using `nix develop` will --- throw an error with the correct value to use or even better you --- can use `nix-prefetch-git`: --- --- $ nix-shell -p nix-prefetch-git --- $ nix-prefetch-git https://github.com/intersectmbo/formal-ledger-specifications --rev | jq .hash source-repository-package type: git location: https://github.com/IntersectMBO/formal-ledger-specifications.git + subdir: generated -- !WARNING!: -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE! - subdir: generated - --sha256: sha256-vrxKI3I1kwt+XiHk+UAWm49veRPTWkVPOvwNzVxuFs8= tag: 9b706ae8c332d5ad10def54aa51d4a66836df363 --- NOTE: If you would like to update the above, look for the `MAlonzo-code` --- branch in the `formal-ledger-specifications` repo and copy the SHA of --- the commit you need. The `MAlonzo-code` branch functions like an alternative --- `master / main` branch for the generated code, see the details here: --- https://github.com/IntersectMBO/formal-ledger-specifications/pull/530 --- If you are working on something in `formal-ledger-specifications` --- and would like to see how they reflect here, just open a PR / draft PR --- in `formal-ledger-specifications` for your branch and that will --- automatically create a branch for the generated code that you can try here --- by editing the above SRP. --- Once your changes are merged in `formal-ledger-specifications`, the branch --- for the generated code will be merged into `MAlonzo-code` automatically. --- Before merging a PR in `cardano-ledger`, make sure that the above SRP --- points to a commit in `MAlonzo-code` if you were fiddling with the SRP --- as part of your PR. +-- NOTE: If you would like to update the above, +-- see CONTRIBUTING.md#to-update-the-referenced-agda-ledger-spec index-state: , hackage.haskell.org 2025-01-14T00:25:08Z , cardano-haskell-packages 2025-01-08T16:35:32Z diff --git a/flake.lock b/flake.lock index 7cbfdd6d141..86d2567b0d3 100644 --- a/flake.lock +++ b/flake.lock @@ -201,6 +201,22 @@ "type": "github" } }, + "formal-ledger-specifications": { + "flake": false, + "locked": { + "lastModified": 1739273763, + "narHash": "sha256-vrxKI3I1kwt+XiHk+UAWm49veRPTWkVPOvwNzVxuFs8=", + "owner": "IntersectMBO", + "repo": "formal-ledger-specifications", + "rev": "9b706ae8c332d5ad10def54aa51d4a66836df363", + "type": "github" + }, + "original": { + "owner": "IntersectMBO", + "repo": "formal-ledger-specifications", + "type": "github" + } + }, "ghc-8.6.5-iohk": { "flake": false, "locked": { @@ -843,6 +859,7 @@ "cardano-mainnet-mirror": "cardano-mainnet-mirror", "flake-compat": "flake-compat", "flake-utils": "flake-utils", + "formal-ledger-specifications": "formal-ledger-specifications", "haskellNix": "haskellNix", "iohkNix": "iohkNix", "nixpkgs": [ diff --git a/flake.nix b/flake.nix index f384001bc3f..6338cd67af8 100644 --- a/flake.nix +++ b/flake.nix @@ -24,6 +24,11 @@ }; pre-commit-hooks.url = "github:cachix/pre-commit-hooks.nix"; + + formal-ledger-specifications = { + url = "github:IntersectMBO/formal-ledger-specifications"; + flake = false; + }; }; outputs = inputs: let @@ -71,6 +76,7 @@ # inputMap = { "https://chap.intersectmbo.org/" = inputs.CHaP; + "https://github.com/IntersectMBO/formal-ledger-specifications.git" = inputs.formal-ledger-specifications; }; cabalProjectLocal = '' repository cardano-haskell-packages-local