From 2d237b29d532c33bedc1c3d5db70e92b0e76aac0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 12 Dec 2024 13:38:20 +0100
Subject: [PATCH] switch ci to docker

---
 .github/workflows/main.yml   | 39 +++++++++++++++---------------------
 builtin-doc/coq-builtin.elpi |  7 +++++++
 dune-project                 |  2 +-
 etc/setup-project.sh         |  5 ++++-
 theories/elpi.v.in           |  2 +-
 5 files changed, 29 insertions(+), 26 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index f8147c217..af0a3d29b 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -26,32 +26,25 @@ env:
 
 jobs:
 
-  build:
-    runs-on: ubuntu-latest
+  docker:
+    runs-on: ubuntu-latest  # container actions require GNU/Linux
     strategy:
-      fail-fast: false
       matrix:
-        coq_version: [ '8.20+rc1' , 'dev' ]
-        ocaml_version:
-          - '4.14.x'
-          - '5.2.x'
+        image:
+          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.20.0'
+      fail-fast: false  # don't stop jobs if one fails
     steps:
-    - uses: actions/checkout@v2
-    - uses: avsm/setup-ocaml@v3
-      with:
-        ocaml-compiler: ${{ matrix.ocaml_version }}
-        opam-pin: false
-        opam-local-packages:
-    - run: opam repo add coq-dev https://coq.inria.fr/opam/core-dev
-    - run: opam install coq-core.${{ matrix.coq_version }}
-    - run: opam install coq-stdlib.${{ matrix.coq_version }}
-    - run: |
-        opam pin add coq-core ${{ matrix.coq_version }}
-        opam pin add coq-stdlib ${{ matrix.coq_version }}
-      if: ${{ matrix.coq_version != 'dev' }}
-    - run: opam install ./coq-elpi.opam --deps-only --with-test -y --ignore-constraints-on coq 
-    - run: opam exec make build
-    - run: opam exec make test
+      - uses: actions/checkout@v3
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-elpi.opam'
+          custom_image: ${{ matrix.image }}
+          export: 'OPAMWITHTEST OPAMIGNORECONSTRAINTS OPAMVERBOSE'  # space-separated list of variables
+        env:
+          OPAMWITHTEST: 'true'
+          OPAMIGNORECONSTRAINTS: 'coq'
+          OPAMVERBOSE: '3'
 
   release:
     runs-on: ubuntu-latest
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
index 2efa967d5..eb19b8cab 100644
--- a/builtin-doc/coq-builtin.elpi
+++ b/builtin-doc/coq-builtin.elpi
@@ -1360,6 +1360,13 @@ external pred coq.arguments.simplification i:gref,
 external pred coq.arguments.set-simplification i:gref, 
                                                i:simplification_strategy.
 
+% [coq.arguments.reset-simplification GR] resets the behavior of the
+% simplification tactics.
+% Also resets the ! and / modifiers for the Arguments command.
+% Supported attributes:
+% - @global! (default: false)
+external pred coq.arguments.reset-simplification i:gref.
+
 % [coq.locate-abbreviation Name Abbreviation] locates an abbreviation.  It's
 % a fatal error if Name cannot be located.
 external pred coq.locate-abbreviation i:id, o:abbreviation.
diff --git a/dune-project b/dune-project
index a27cbc7b9..1967ac1ea 100644
--- a/dune-project
+++ b/dune-project
@@ -1,7 +1,7 @@
 (lang dune 3.13)
 (using coq 0.8)
 (name coq-elpi)
-(generate_opam_files)
+;(generate_opam_files)
 
 (source (github LPCIC/coq-elpi))
 (license LGPL-2.1-or-later)
diff --git a/etc/setup-project.sh b/etc/setup-project.sh
index e74d67c49..d05e25aa8 100755
--- a/etc/setup-project.sh
+++ b/etc/setup-project.sh
@@ -1,4 +1,7 @@
-if [ -z "$DEPS" ]; then DEPS="elpi_elpi elpi"; else DEPS="elpi_elpi elpi $DEPS"; fi
+
+if coqc --print-version | cut -d ' ' -f 1 | grep -q "^9" ; then STDLIB="Stdlib"; else STDLIB=""; fi
+
+if [ -z "$DEPS" ]; then DEPS="elpi_elpi elpi $STDLIB"; else DEPS="elpi_elpi elpi $STDLIB $DEPS"; fi
 
 cat > dune <<EOF
 (env
diff --git a/theories/elpi.v.in b/theories/elpi.v.in
index 17a6e4f99..89b0555cb 100644
--- a/theories/elpi.v.in
+++ b/theories/elpi.v.in
@@ -1,4 +1,4 @@
-From Coq Require Ltac.
+(*From Coq Require Ltac.*)
 From elpi_elpi Require Import dummy.
 Declare ML Module "coq-elpi.elpi".