diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 1aa7f0b..baf2fa3 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -25,11 +25,17 @@ jobs: - 'mathcomp/mathcomp:1.13.0-coq-8.12' - 'mathcomp/mathcomp:1.13.0-coq-8.13' - 'mathcomp/mathcomp:1.13.0-coq-8.14' - - 'mathcomp/mathcomp:1.13.0-coq-dev' + - 'mathcomp/mathcomp:1.13.0-coq-8.15' + - 'mathcomp/mathcomp:1.14.0-coq-8.11' + - 'mathcomp/mathcomp:1.14.0-coq-8.12' + - 'mathcomp/mathcomp:1.14.0-coq-8.13' + - 'mathcomp/mathcomp:1.14.0-coq-8.14' + - 'mathcomp/mathcomp:1.14.0-coq-8.15' - 'mathcomp/mathcomp-dev:coq-8.11' - 'mathcomp/mathcomp-dev:coq-8.12' - 'mathcomp/mathcomp-dev:coq-8.13' - 'mathcomp/mathcomp-dev:coq-8.14' + - 'mathcomp/mathcomp-dev:coq-8.15' - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: diff --git a/Licence_CeCILL-C_V1-en.txt b/LICENSE similarity index 100% rename from Licence_CeCILL-C_V1-en.txt rename to LICENSE diff --git a/README.md b/README.md index 7654f10..ef767bc 100644 --- a/README.md +++ b/README.md @@ -5,10 +5,21 @@ Follow the instructions on https://github.com/coq-community/templates to regener # Apery [![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/apery/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/math-comp/apery/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/coq-community/apery/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-link]: https://github.com/coq-community/apery/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 @@ -26,7 +37,9 @@ remains the sole trusted code base. - Frédéric Chyzak (initial) - Assia Mahboubi (initial) - Thomas Sibut-Pinote (initial) -- License: [CeCILL-C](Licence_CeCILL-C_V1-en.txt) +- Coq-community maintainer(s): + - Assia Mahboubi ([**@amahboubi**](https://github.com/amahboubi)) +- License: [CeCILL-C](LICENSE) - Compatible Coq versions: 8.11 or later - Additional dependencies: - [MathComp ssreflect 1.12 or later](https://math-comp.github.io) @@ -53,7 +66,7 @@ opam install coq-mathcomp-apery To instead build and install manually, do: ``` shell -git clone https://github.com/math-comp/apery.git +git clone https://github.com/coq-community/apery.git cd apery make # or make -j make install diff --git a/coq-mathcomp-apery.opam b/coq-mathcomp-apery.opam index 0835b56..24850e5 100644 --- a/coq-mathcomp-apery.opam +++ b/coq-mathcomp-apery.opam @@ -5,9 +5,9 @@ opam-version: "2.0" maintainer: "assia.mahboubi@inria.fr" version: "dev" -homepage: "https://github.com/math-comp/apery" -dev-repo: "git+https://github.com/math-comp/apery.git" -bug-reports: "https://github.com/math-comp/apery/issues" +homepage: "https://github.com/coq-community/apery" +dev-repo: "git+https://github.com/coq-community/apery.git" +bug-reports: "https://github.com/coq-community/apery/issues" license: "CECILL-C" synopsis: "A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational" @@ -23,8 +23,8 @@ remains the sole trusted code base.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.11" & < "8.15~") | (= "dev")} - "coq-mathcomp-ssreflect" {(>= "1.12" & < "1.14~") | (= "dev")} + "coq" {(>= "8.11" & < "8.16~") | (= "dev")} + "coq-mathcomp-ssreflect" {(>= "1.12" & < "1.15~") | (= "dev")} "coq-mathcomp-algebra" "coq-mathcomp-field" "coq-coqeal" {>= "1.0.5"} diff --git a/meta.yml b/meta.yml index 33181a4..5ffbef1 100644 --- a/meta.yml +++ b/meta.yml @@ -1,8 +1,8 @@ fullname: Apery shortname: apery -organization: math-comp +organization: coq-community opam_name: coq-mathcomp-apery -community: false +community: true action: true coqdoc: false @@ -33,6 +33,10 @@ authors: - name: Thomas Sibut-Pinote initial: true +maintainers: +- name: Assia Mahboubi + nickname: amahboubi + opam-file-maintainer: assia.mahboubi@inria.fr opam-file-version: dev @@ -40,11 +44,10 @@ opam-file-version: dev license: fullname: CeCILL-C identifier: CECILL-C - file: Licence_CeCILL-C_V1-en.txt supported_coq_versions: text: 8.11 or later - opam: '{(>= "8.11" & < "8.15~") | (= "dev")}' + opam: '{(>= "8.11" & < "8.16~") | (= "dev")}' tested_coq_opam_versions: - version: '1.12.0-coq-8.11' @@ -63,7 +66,17 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.14' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-dev' +- version: '1.13.0-coq-8.15' + repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.11' + repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.12' + repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.13' + repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.14' + repo: 'mathcomp/mathcomp' +- version: '1.14.0-coq-8.15' repo: 'mathcomp/mathcomp' - version: 'coq-8.11' repo: 'mathcomp/mathcomp-dev' @@ -73,13 +86,15 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp-dev' - version: 'coq-8.14' repo: 'mathcomp/mathcomp-dev' +- version: 'coq-8.15' + repo: 'mathcomp/mathcomp-dev' - version: 'coq-dev' repo: 'mathcomp/mathcomp-dev' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{(>= "1.12" & < "1.14~") | (= "dev")}' + version: '{(>= "1.12" & < "1.15~") | (= "dev")}' description: |- [MathComp ssreflect 1.12 or later](https://math-comp.github.io) - opam: