From a726e95025b42df936ee1e0ebf7094c26fd573a1 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Mon, 19 Jun 2023 14:46:15 +0200 Subject: [PATCH] meta update for coq-community, test up to MathComp 1.17 and Coq 8.17 --- .github/workflows/docker-action.yml | 16 +++++++-------- README.md | 18 +++++++++++++++-- coq-mathcomp-tarjan.opam | 4 ++-- meta.yml | 30 +++++++++++++---------------- 4 files changed, 38 insertions(+), 30 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 3c9e4b6..96abd23 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/README.md b/README.md index a9fd36e..da20078 100644 --- a/README.md +++ b/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): diff --git a/coq-mathcomp-tarjan.opam b/coq-mathcomp-tarjan.opam index 3665f29..0596472 100644 --- a/coq-mathcomp-tarjan.opam +++ b/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" ] diff --git a/meta.yml b/meta.yml index 1b2dfbb..f0fad99 100644 --- a/meta.yml +++ b/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 @@ -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