You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Add instruction for conformance testing against local build (#4910)
* Add instructions for conformance testing against local build with examples
* Add instructions to build the Haskell code from formal ledger
---------
Co-authored-by: teodanciu <teodora.danciu@tweag.io>
Copy file name to clipboardExpand all lines: CONTRIBUTING.md
+41Lines changed: 41 additions & 0 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -289,6 +289,12 @@ from [the Shelley ledger spec](./eras/shelley/formal-spec)).
289
289
4. Add a link to the package near the bottom of [flake.nix](./flake.nix),
290
290
following the existing examples.
291
291
292
+
### To build the Haskell code from the Agda ledger spec
293
+
294
+
See [Build the spec using nix-build](https://github.com/IntersectMBO/formal-ledger-specifications/tree/master?tab=readme-ov-file#build-the-spec-using-nix-build)
295
+
and [Contributing](https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/CONTRIBUTING.md)
296
+
in the [formal-ledger-specifications repo](https://github.com/IntersectMBO/formal-ledger-specifications).
297
+
292
298
### To update the referenced Agda ledger spec
293
299
294
300
To update the version of the Agda spec that the conformance tests are using:
@@ -304,6 +310,41 @@ To update the version of the Agda spec that the conformance tests are using:
304
310
305
311
If the commit you need in`formal-ledger-specifications` is not on master, open a PR foryour branchin 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`.
306
312
313
+
### To run conformance testing against a local build of the Agda ledger spec
314
+
315
+
1. Enter the `nix develop` shell
316
+
2. Comment out the `source-repository-package` section in`cabal.project`
317
+
3. Add the path to the local build directory (containing the `cardano-ledger-executable-spec.cabal` file, see below forexamples) to `packages`in`cabal.project`
318
+
4. Execute the tests, e.g., running `cabal test cardano-ledger-conformance`
319
+
320
+
To change the local build directory, redo step 3 _without leaving_ the `nix develop` shell.
321
+
322
+
#### Examples
323
+
324
+
- As an absolute path:
325
+
326
+
Compiling the `formal-ledger-specifications` to Haskell via:
327
+
```shell
328
+
nix-build -A ledger.hsSrc
329
+
```
330
+
returns a path to the nix store, e.g., `/nix/store/9pv3x44dfnwrz0jjrh9mlxa9y143i987-hs-src-0.1`, that can be used as:
in the packages section of the `cabal.project` file.
335
+
336
+
- As a relative path:
337
+
338
+
Cloning the [formal-ledger-specifications repo](https://github.com/IntersectMBO/formal-ledger-specifications) on a `MAlonzo` branch as a sibling folder, e.g., `spec`, of `cardano-leder`:
0 commit comments