Merge pull request #25 from coq-community/mc-1-community-update

meta update for coq-community, test up to MathComp 1.17 and Coq 8.17

Author: palmskog

.github/workflows/docker-action.yml

@@ -17,27 +17,25 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.17'
-          - 'mathcomp/mathcomp-dev:coq-8.13'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.12'
           - 'mathcomp/mathcomp:1.12.0-coq-8.14'
           - 'mathcomp/mathcomp:1.12.0-coq-8.12'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-mathcomp-tarjan.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -5,10 +5,21 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 # Tarjan and Kosaraju
 
 [![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]
 
 [docker-action-shield]: https://github.com/math-comp/tarjan/workflows/Docker%20CI/badge.svg?branch=master
 [docker-action-link]: https://github.com/math-comp/tarjan/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
+
+[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg
+[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md
+
+[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg
+[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users
 
 
 
@@ -24,10 +35,13 @@ sorting with extended guarantees for acyclic graphs.
   - Jean-Jacques Lévy (initial)
   - Karl Palmskog
   - Laurent Théry (initial)
+- Coq-community maintainer(s):
+  - Cyril Cohen ([**@CohenCyril**](https://github.com/CohenCyril))
+  - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [CeCILL-B](CeCILL-B)
-- Compatible Coq versions: 8.10 or later
+- Compatible Coq versions: 8.12 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 1.12 to 1.17](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
 - Coq namespace: `mathcomp.tarjan`
 - Related publication(s):

coq-mathcomp-tarjan.opam

@@ -20,8 +20,8 @@ sorting with extended guarantees for acyclic graphs."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.12" & < "8.18~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.17~") | (= "dev")}
+  "coq" {>= "8.12"}
+  "coq-mathcomp-ssreflect" {>= "1.12.0" & < "1.18~"}
   "coq-mathcomp-fingroup" 
 ]
 

meta.yml

@@ -3,7 +3,7 @@ fullname: Tarjan and Kosaraju
 shortname: tarjan
 organization: math-comp
 opam_name: coq-mathcomp-tarjan
-community: false
+community: true
 action: true
 coqdoc: false
 
@@ -34,8 +34,8 @@ authors:
 maintainers:
 - name: Cyril Cohen
   nickname: CohenCyril
-- name: Laurent Théry
-  nickname: thery
+- name: Karl Palmskog
+  nickname: palmskog
 
 opam-file-maintainer: Cyril Cohen <[email protected]>
 
@@ -47,33 +47,31 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: '8.10 or later'
-  opam: '{(>= "8.10" & < "8.16~") | (= "dev")}'
+  text: '8.12 or later'
+  opam: '{>= "8.12"}'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.12.0" & < "1.15~") | (= "dev")}'
+    version: '{>= "1.12.0" & < "1.18~"}'
   description: |-
-    [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
+    [MathComp ssreflect 1.12 to 1.17](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.15'
-  repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.14'
-  repo: 'mathcomp/mathcomp-dev'
+- version: '1.17.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.11'
-  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.13'
@@ -84,8 +82,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.10'
-  repo: 'mathcomp/mathcomp'
 
 namespace: mathcomp.tarjan