From a208b51208d7a3b66b848a887ca5b8c66177917e Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Thu, 26 Feb 2026 11:27:17 +0000
Subject: [PATCH] CI: try out OPAM caching

---
 .github/workflows/ci.yml | 15 +++++++++++++++
 Makefile                 |  6 +++++-
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 8ede6ed..839d0a9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -81,6 +81,15 @@ jobs:
         ref: 6e3971e07897f17e06cd21c4e20558ea4161861a
         path: peregrine-tool
 
+    - name: Restore OPAM cache
+      id: opam-cache
+      uses: actions/cache@v5
+      with:
+        path: "~/.opam"
+        key: opam-${{matrix.ocaml}}-${{hashFiles('peregrine-tool/.github/rocq-peregrine.opam.locked')}}
+        restore-keys: |
+          opam-${{matrix.ocaml}}-
+
     - name: Set up OCaml
       uses: ocaml/setup-ocaml@v3
       with:
@@ -105,3 +114,9 @@ jobs:
         github_token: ${{ secrets.GITHUB_TOKEN }}
         publish_dir: test/html
 
+    - name: OPAM cache clean-up
+      run: |
+        opam remove rocq-peregrine
+        opam pin remove rocq-peregrine
+        eval $(opam env)
+        opam clean -a -c -s --logs
diff --git a/Makefile b/Makefile
index 820eaec..822164c 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY: default build install html clean
+.PHONY: default build install coq html clean
 
 default: build
 
@@ -13,6 +13,10 @@ test: test/Tests.agda
 test/Tests.agda: test/Main.hs test/agda2lambox-tests.agda-lib test/untyped/*.agda test/typed/*.agda test/agda2rust/*.agda
 	cabal test
 
+coq:
+	coq_makefile -f _CoqProject -o CoqMakefile
+	make -f CoqMakefile
+
 html: test
 	make -C test html