CI: GitHub Actions

.github/workflows/docker-action.yml

@@ -0,0 +1,72 @@
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        coq:
+          - '8.9'
+          - '8.11'
+          - '8.12'
+          - '8.13'
+          - '8.14'
+          - '8.15'
+          - '8.16'
+          - '8.17'
+          - 'dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-ext-lib.opam'
+          coq_version: ${{ matrix.coq }}
+          before_script: |
+            startGroup "Workaround permission issue"
+              sudo chown -R coq:coq .
+            endGroup
+          after_script: |
+            set -o pipefail  # recommended if the script uses pipes
+
+            startGroup "Generate Coqdoc"
+              make -j`nproc` html
+            endGroup
+
+            startGroup "Test dependants"
+              opam install conf-clang
+              PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
+              PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
+              for PACKAGE in $PACKAGES
+              do DEPS_FAILED=false
+                 opam install --deps-only $PACKAGE || DEPS_FAILED=true
+                 [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
+              done
+            endGroup
+          export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
+        env:
+          OPAMWITHTEST: true
+          OPAMCONFIRMLEVEL: unsafe-yes
+      - name: Revert permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+      - uses: actions/upload-artifact@v3
+        with:
+          name: coqdoc
+          path: html
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

Makefile

@@ -1,5 +1,6 @@
 all: theories examples
 
+COQDOCJS_LN?=true
 -include coqdocjs/Makefile.doc
 COQMAKEFILE?=Makefile.coq
 

README.md

@@ -4,13 +4,13 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 --->
 # coq-ext-lib
 
-[![CircleCI][circleci-shield]][circleci-link]
+[![Docker CI][docker-action-shield]][docker-action-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[circleci-shield]: https://circleci.com/gh/coq-community/coq-ext-lib.svg?style=svg
-[circleci-link]:   https://circleci.com/gh/coq-community/coq-ext-lib
+[docker-action-shield]: https://github.com/coq-community/coq-ext-lib/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/coq-ext-lib/actions?query=workflow:"Docker%20CI"
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md

meta.yml

@@ -4,7 +4,7 @@ shortname: coq-ext-lib
 opam_name: coq-ext-lib
 organization: coq-community
 community: true
-circleci: false
+action: false
 ci_test_dependants: true
 submodule: true
 
@@ -38,6 +38,8 @@ tested_coq_opam_versions:
   - version: '8.13'
   - version: '8.14'
   - version: '8.15'
+  - version: '8.16'
+  - version: '8.17'
   - version: 'dev'
 
 make_target: theories
@@ -53,6 +55,11 @@ circleci_after_script: |2-
       - store_artifacts:
           path: coqdoc.tgz
 
+action_appendix: |2-
+            export: 'OPAMWITHTEST'
+          env:
+            OPAMWITHTEST: true
+
 documentation: |
   Ideas
   -----

theories/Data/Char.v

@@ -6,7 +6,7 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Definition ascii_dec (l r : Ascii.ascii) : bool :=
+Definition deprecated_ascii_dec (l r : Ascii.ascii) : bool :=
   match l , r with
     | Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
       Ascii.Ascii r1 r2 r3 r4 r5 r6 r7 r8 =>
@@ -28,7 +28,10 @@ Definition ascii_dec (l r : Ascii.ascii) : bool :=
         else false
   end.
 
-Theorem ascii_dec_sound : forall l r,
+#[deprecated(since="8.9",note="Use Ascii.eqb instead.")]
+Notation ascii_dec := deprecated_ascii_dec.
+
+Theorem deprecated_ascii_dec_sound : forall l r,
   ascii_dec l r = true <-> l = r.
 Proof.
   unfold ascii_dec. intros.
@@ -39,17 +42,20 @@ Proof.
          end; split; congruence.
 Qed.
 
+#[deprecated(since="8.9",note="Use Ascii.eqb_eq instead.")]
+Notation ascii_dec_sound := deprecated_ascii_dec_sound.
+
 Global Instance RelDec_ascii : RelDec (@eq Ascii.ascii) :=
-{ rel_dec := ascii_dec }.
+{ rel_dec := Ascii.eqb }.
 
 Global Instance RelDec_Correct_ascii : RelDec_Correct RelDec_ascii.
 Proof.
-  constructor; auto using ascii_dec_sound.
+  constructor; auto using Ascii.eqb_eq.
 Qed.
 
-Global Instance Reflect_ascii_dec a b : Reflect (ascii_dec a b) (a = b) (a <> b).
+Global Instance Reflect_ascii_dec a b : Reflect (Ascii.eqb a b) (a = b) (a <> b).
 Proof.
-  apply iff_to_reflect; auto using ascii_dec_sound.
+  apply iff_to_reflect; auto using Ascii.eqb_eq.
 Qed.
 
 Definition digit2ascii (n:nat) : Ascii.ascii :=

theories/Data/String.v

@@ -18,72 +18,77 @@ Local Notation "x >> y" := (match x with
                               | z => z
                             end) (only parsing, at level 30).
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.12",note="Use Bool.compare instead.")] *)
-Definition bool_cmp (l r : bool) : comparison :=
+Definition deprecated_bool_cmp (l r : bool) : comparison :=
   match l , r with
     | true , false => Gt
     | false , true => Lt
     | true , true
     | false , false => Eq
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.15",note="Use Ascii.compare instead.")] *)
-Definition ascii_cmp (l r : Ascii.ascii) : comparison :=
+#[deprecated(since="8.12",note="Use Bool.compare instead.")]
+Notation bool_cmp := deprecated_bool_cmp.
+
+Definition deprecated_ascii_cmp (l r : Ascii.ascii) : comparison :=
   match l , r with
     | Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
       Ascii.Ascii r1 r2 r3 r4 r5 r6 r7 r8 =>
       bool_cmp l8 r8 >> bool_cmp l7 r7 >> bool_cmp l6 r6 >> bool_cmp l5 r5 >>
       bool_cmp l4 r4 >> bool_cmp l3 r3 >> bool_cmp l2 r2 >> bool_cmp l1 r1
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.9",note="Use String.eqb instead.")] *)
-Fixpoint string_dec (l r : string) : bool :=
+#[deprecated(since="8.15",note="Use Ascii.compare instead.")]
+Notation ascii_cmp := deprecated_ascii_cmp.
+
+Fixpoint deprecated_string_dec (l r : string) : bool :=
   match l , r with
     | EmptyString , EmptyString => true
     | String l ls , String r rs =>
-      if ascii_dec l r then string_dec ls rs
+      if Ascii.eqb l r then deprecated_string_dec ls rs
       else false
     | _ , _ => false
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.9",note="Use String.eqb_spec instead.")] *)
-Theorem string_dec_sound : forall l r,
+#[deprecated(since="8.9",note="Use String.eqb instead.")]
+Notation string_dec := deprecated_string_dec.
+
+Theorem deprecated_string_dec_sound : forall l r,
   string_dec l r = true <-> l = r.
 Proof.
-  induction l; destruct r; simpl; split; try solve [ intuition ; congruence ];
-  consider (ascii_dec a a0); intros; subst. f_equal. eapply IHl; auto.
-  apply IHl. congruence.
-  inversion H. congruence.
+  induction l; destruct r; try (constructor; easy); simpl.
+  case (Ascii.eqb_spec a a0); simpl; [intros -> | constructor; now intros [= ]].
+  case (IHl r); intros; constructor; intros; f_equal; auto.
+  inversion H1; subst; auto.
 Qed.
 
+#[deprecated(since="8.9",note="Use String.eqb_eq instead.")]
+Notation string_dec_sound := deprecated_string_dec_sound.
+
 Global Instance RelDec_string : RelDec (@eq string) :=
-{| rel_dec := string_dec |}.
+{| rel_dec := String.eqb |}.
 
 Global Instance RelDec_Correct_string : RelDec_Correct RelDec_string.
 Proof.
-  constructor; auto using string_dec_sound.
+  constructor; auto using String.eqb_eq.
 Qed.
 
-Global Instance Reflect_string_dec a b : Reflect (string_dec a b) (a = b) (a <> b).
+Global Instance Reflect_string_dec a b : Reflect (String.eqb a b) (a = b) (a <> b).
 Proof.
-  apply iff_to_reflect; auto using string_dec_sound.
+  apply iff_to_reflect; auto using String.eqb_eq.
 Qed.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.15",note="Use String.compare instead.")] *)
-Fixpoint string_cmp (l r : string) : comparison :=
+Fixpoint deprecated_string_cmp (l r : string) : comparison :=
   match l , r with
     | EmptyString , EmptyString => Eq
     | EmptyString , _ => Lt
     | _ , EmptyString => Gt
     | String l ls , String r rs =>
-      ascii_cmp l r >> string_cmp ls rs
+      ascii_cmp l r >> deprecated_string_cmp ls rs
   end.
 
+#[deprecated(since="8.15",note="Use String.compare instead.")]
+Notation string_cmp := deprecated_string_cmp.
+
 Section Program_Scope.
   Variable modulus : nat.
   Hypothesis one_lt_mod : 1 < modulus.