switch opam ci to docker

.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

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.

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)

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

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".