Skip to content

Commit

Permalink
Merge pull request #8 from coq-community/community-boilerplate
Browse files Browse the repository at this point in the history
adapt boilerplate after move to coq-community
  • Loading branch information
palmskog authored Feb 3, 2022
2 parents 776e0ef + 1f60982 commit 7df8fb4
Show file tree
Hide file tree
Showing 5 changed files with 50 additions and 16 deletions.
8 changes: 7 additions & 1 deletion .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
File renamed without changes.
21 changes: 17 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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



Expand All @@ -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)
Expand All @@ -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 <number-of-cores-on-your-machine>
make install
Expand Down
10 changes: 5 additions & 5 deletions coq-mathcomp-apery.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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"}
Expand Down
27 changes: 21 additions & 6 deletions meta.yml
Original file line number Diff line number Diff line change
@@ -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

Expand Down Expand Up @@ -33,18 +33,21 @@ authors:
- name: Thomas Sibut-Pinote
initial: true

maintainers:
- name: Assia Mahboubi
nickname: amahboubi

opam-file-maintainer: assia.mahboubi@inria.fr

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'
Expand All @@ -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'
Expand All @@ -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:
Expand Down

0 comments on commit 7df8fb4

Please sign in to comment.