From 874079e76834469e7383cc79d595526cef0abaa3 Mon Sep 17 00:00:00 2001
From: Calvin Beck <hobbes@ualberta.ca>
Date: Tue, 18 Nov 2025 19:46:53 -0500
Subject: [PATCH] Update Docker CI build for Rocq 9.0.

- 9.1 doesn't work yet because of rocq-relation-algebra.
---
 .github/workflows/coq.yml | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
index 2cd7ea3..7873085 100644
--- a/.github/workflows/coq.yml
+++ b/.github/workflows/coq.yml
@@ -1,12 +1,8 @@
 name: Docker CI
 
 on:
-  push:
-    branches:
-      - master
   pull_request:
-    branches:
-      - '**'
+  push:
 
 jobs:
   build:
@@ -14,20 +10,33 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.15.2'
+          - "9.0"
         ocaml_version:
-          - '4.14.0-flambda'
+          - "4.14-flambda"
       max-parallel: 4
       fail-fast: false
 
     steps:
-      - uses: actions/checkout@v2
-      - uses: coq-community/docker-coq-action@v1
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Compile under docker
+        uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-ctree.opam'
+          opam_file: 'rocq-ctree.opam'
           coq_version: ${{ matrix.coq_version }}
           ocaml_version: ${{ matrix.ocaml_version }}
           export: 'OPAMWITHTEST'
+          before_install: |
+            startGroup "Workaround permission issue"
+              sudo chown -R 1000:1000 .
+            endGroup
+            startGroup "Generate Opam File"
+              dune build rocq-ctree.opam
+            endGroup
+            startGroup "Print opam config"
+              opam config list; opam repo list; opam list
+            endGroup
         env:
           OPAMWITHTEST: 'true'