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
IntersectMBO · Mar 6, 2025 · b1672f1 · b1672f1
1 parent 25723a5
commit b1672f1
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 30 deletions.
diff --git 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
@@ -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 <GIT_SHA> | 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
diff --git 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