From c6ae777ea613bb572ec339aac1b122c51c05f8b8 Mon Sep 17 00:00:00 2001
From: Dimitrios Economou <dimitrios.j.economou@gmail.com>
Date: Tue, 29 Jul 2025 15:02:24 +0100
Subject: [PATCH] Add instructions for local Rocq testing

---
 README.md | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/README.md b/README.md
index a7993c642..687cbd90f 100644
--- a/README.md
+++ b/README.md
@@ -98,6 +98,25 @@ and its dependencies.
    `cerberus-lib` to stay in sync, by re-running the `opam install`
    step above.)
 
+   If you want to run the Rocq test script locally:
+   ```
+   # Setup opam
+   opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
+   opam pin --yes -n coq-struct-tact https://github.com/uwplse/StructTact.git
+   opam install --deps-only --yes ./cn.opam
+
+   # Install CN with Coq
+   opam pin --yes --no-action add cn .
+   opam pin --yes --no-action add cn-coq .
+   opam install --yes cn cn-coq
+
+   # Run test script
+   ./tests/run-cn-coq.sh
+
+   # Run on a file
+   ./tests/run-cn-coq.sh -f file-path
+   ```
+
 ## Contributing
 
 Please see our [contributing