Skip to content

Commit 017a857

Browse files
pi8027pi8027
committed
Switch to Rocq-community templates
1 parent 468a7cc commit 017a857

File tree

5 files changed

+195
-106
lines changed

5 files changed

+195
-106
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 0 additions & 75 deletions
This file was deleted.

‎.github/workflows/docker-action.yml‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# This file was generated from `meta.yml`, please do not edit manually.
2+
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
3+
name: Docker CI
4+
5+
on:
6+
push:
7+
branches:
8+
- master
9+
pull_request:
10+
branches:
11+
- '**'
12+
13+
jobs:
14+
build:
15+
# the OS must be GNU/Linux to be able to use the docker-coq-action
16+
runs-on: ubuntu-latest
17+
strategy:
18+
matrix:
19+
image:
20+
- 'mathcomp/mathcomp:2.4.0-coq-8.20'
21+
- 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
22+
- 'mathcomp/mathcomp:2.4.0-rocq-prover-dev'
23+
- 'mathcomp/mathcomp-dev:coq-8.20'
24+
- 'mathcomp/mathcomp-dev:rocq-prover-9.0'
25+
- 'mathcomp/mathcomp-dev:rocq-prover-dev'
26+
fail-fast: false
27+
steps:
28+
- uses: actions/checkout@v4
29+
- uses: coq-community/docker-coq-action@v1
30+
with:
31+
opam_file: 'coq-mathcomp-multinomials.opam'
32+
custom_image: ${{ matrix.image }}
33+
34+
35+
# See also:
36+
# https://github.com/coq-community/docker-coq-action#readme
37+
# https://github.com/erikmd/docker-coq-github-action-demo

‎README.md‎

Lines changed: 42 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,43 +1,65 @@
1-
A Multivariate polynomial Library for the Mathematical Components Library
2-
========================================================================
1+
<!---
2+
This file was generated from `meta.yml`, please do not edit manually.
3+
Follow the instructions on https://github.com/coq-community/templates to regenerate.
4+
--->
5+
# A Multivariate polynomial Library for the Mathematical Components Library
36

4-
This library provides a library for monomial algebra,for multivariate
5-
polynomials over ring structures and an extended theory for
6-
polynomials whose coefficients range over commutative rings and
7-
integral domains.
7+
[![Docker CI][docker-action-shield]][docker-action-link]
88

9-
Building and installation instructions
10-
------------------------------------------------------------------------
9+
[docker-action-shield]: https://github.com/math-comp/multinomials/actions/workflows/docker-action.yml/badge.svg?branch=master
10+
[docker-action-link]: https://github.com/math-comp/multinomials/actions/workflows/docker-action.yml
1111

12-
The easiest way to install the latest released version this library is
13-
via [OPAM](https://opam.ocaml.org/doc/Install.html):
12+
13+
14+
15+
This library provides a library for monomial algebra, for multivariate
16+
polynomials over ring structures and an extended theory for polynomials whose
17+
coefficients range over commutative rings and integral domains.
18+
19+
## Meta
20+
21+
- Author(s):
22+
- Pierre-Yves Strub (initial)
23+
- License: [CeCILL-B Free Software License Agreement](CeCILL-B)
24+
- Compatible Rocq/Coq versions: 8.20 or later
25+
- Additional dependencies:
26+
- [MathComp](https://math-comp.github.io) ssreflect 2.4 or later
27+
- [MathComp](https://math-comp.github.io) algebra
28+
- [MathComp finmap](https://github.com/math-comp/finmap)
29+
- [MathComp bigenough](https://github.com/math-comp/bigenough)
30+
- Rocq/Coq namespace: `mathcomp.multinomials`
31+
- Related publication(s): none
32+
33+
## Building and installation instructions
34+
35+
The easiest way to install the latest released version of A Multivariate polynomial Library for the Mathematical Components Library
36+
is via [OPAM](https://opam.ocaml.org/doc/Install.html):
1437

1538
```shell
1639
opam repo add coq-released https://coq.inria.fr/opam/released
1740
opam install coq-mathcomp-multinomials
1841
```
1942

20-
If you want to install it manually, do:
43+
To instead build and install manually, do:
2144

2245
``` shell
2346
git clone https://github.com/math-comp/multinomials.git
2447
cd multinomials
25-
make # or make -j <number-of-cores-on-your-machine>
48+
make build # or make -j <number-of-cores-on-your-machine> build
2649
make install
2750
```
2851

29-
Authors
30-
========================================================================
3152

32-
"Pierre-Yves Strub" \<pierre-yves@strub.nu\>
53+
54+
## Credits
3355

3456
Contributors:
3557

36-
- [Florent Hivert](https://www.lri.fr/~hivert/)
37-
- [Laurent Thery](https://www-sop.inria.fr/marelle/personnel/Laurent.Thery/moi.html)
58+
- [Florent Hivert](https://www.lri.fr/~hivert/)
59+
- [Laurent Thery](https://www-sop.inria.fr/marelle/personnel/Laurent.Thery/moi.html)
3860

3961
This library is also the result of discussions with:
4062

41-
- Sophie Bernard
42-
- [Cyril Cohen](http://www.cyrilcohen.fr/)
43-
- [Laurence Rideau](http://www-sop.inria.fr/members/Laurence.Rideau/)
63+
- Sophie Bernard
64+
- [Cyril Cohen](http://www.cyrilcohen.fr/)
65+
- [Laurence Rideau](http://www-sop.inria.fr/members/Laurence.Rideau/)

‎coq-mathcomp-multinomials.opam‎

Lines changed: 24 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,38 @@
1+
# This file was generated from `meta.yml`, please do not edit manually.
2+
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
3+
14
opam-version: "2.0"
25
maintainer: "pierre-yves@strub.nu"
6+
version: "dev"
7+
38
homepage: "https://github.com/math-comp/multinomials"
4-
bug-reports: "https://github.com/math-comp/multinomials/issues"
59
dev-repo: "git+https://github.com/math-comp/multinomials.git"
10+
bug-reports: "https://github.com/math-comp/multinomials/issues"
611
license: "CECILL-B"
7-
authors: ["Pierre-Yves Strub"]
8-
build: [make "-j%{jobs}%"]
12+
13+
synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
14+
description: """
15+
This library provides a library for monomial algebra, for multivariate
16+
polynomials over ring structures and an extended theory for polynomials whose
17+
coefficients range over commutative rings and integral domains."""
18+
19+
build: [make "-j%{jobs}%" "build"]
920
install: [make "install"]
1021
depends: [
11-
("coq" {>= "8.20" & < "8.21~"}
12-
| "rocq-core" {>= "9.0"})
22+
"coq" {>= "8.20"}
1323
"coq-mathcomp-ssreflect" {>= "2.4"}
14-
"coq-mathcomp-algebra"
15-
"coq-mathcomp-bigenough"
16-
"coq-mathcomp-finmap"
24+
"coq-mathcomp-algebra"
25+
"coq-mathcomp-finmap"
26+
"coq-mathcomp-bigenough"
1727
]
28+
1829
tags: [
19-
"keyword:multinomials"
20-
"keyword:monoid algebra"
2130
"category:Mathematics/Algebra/Multinomials"
2231
"category:Mathematics/Algebra/Monoid algebra"
32+
"keyword:multinomials"
33+
"keyword:monoid algebra"
2334
"logpath:mathcomp.multinomials"
2435
]
25-
synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
36+
authors: [
37+
"Pierre-Yves Strub"
38+
]

‎meta.yml‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
---
2+
fullname: A Multivariate polynomial Library for the Mathematical Components Library
3+
shortname: multinomials
4+
opam_name: coq-mathcomp-multinomials
5+
organization: math-comp
6+
action: true
7+
8+
synopsis: >-
9+
A Multivariate polynomial Library for the Mathematical Components Library
10+
11+
description: |-
12+
This library provides a library for monomial algebra,for multivariate
13+
polynomials over ring structures and an extended theory for polynomials whose
14+
coefficients range over commutative rings and integral domains.
15+
16+
authors:
17+
- name: Pierre-Yves Strub
18+
initial: true
19+
20+
opam-file-maintainer: pierre-yves@strub.nu
21+
22+
license:
23+
fullname: CeCILL-B Free Software License Agreement
24+
identifier: CECILL-B
25+
file: CeCILL-B
26+
27+
supported_coq_versions:
28+
text: 8.20 or later
29+
opam: '{>= "8.20"}'
30+
31+
tested_coq_nix_versions:
32+
33+
tested_coq_opam_versions:
34+
- version: '2.4.0-coq-8.20'
35+
repo: 'mathcomp/mathcomp'
36+
- version: '2.4.0-rocq-prover-9.0'
37+
repo: 'mathcomp/mathcomp'
38+
- version: '2.4.0-rocq-prover-dev'
39+
repo: 'mathcomp/mathcomp'
40+
- version: 'coq-8.20'
41+
repo: 'mathcomp/mathcomp-dev'
42+
- version: 'rocq-prover-9.0'
43+
repo: 'mathcomp/mathcomp-dev'
44+
- version: 'rocq-prover-dev'
45+
repo: 'mathcomp/mathcomp-dev'
46+
47+
dependencies:
48+
- opam:
49+
name: coq-mathcomp-ssreflect
50+
version: '{>= "2.4"}'
51+
description: |-
52+
[MathComp](https://math-comp.github.io) ssreflect 2.4 or later
53+
- opam:
54+
name: coq-mathcomp-algebra
55+
description: |-
56+
[MathComp](https://math-comp.github.io) algebra
57+
- opam:
58+
name: coq-mathcomp-finmap
59+
description: |-
60+
[MathComp finmap](https://github.com/math-comp/finmap)
61+
- opam:
62+
name: coq-mathcomp-bigenough
63+
description: |-
64+
[MathComp bigenough](https://github.com/math-comp/bigenough)
65+
66+
make_target: build
67+
namespace: mathcomp.multinomials
68+
69+
keywords:
70+
- name: multinomials
71+
- name: monoid algebra
72+
73+
categories:
74+
- name: Mathematics/Algebra/Multinomials
75+
- name: Mathematics/Algebra/Monoid algebra
76+
77+
documentation: |-
78+
79+
## Credits
80+
81+
Contributors:
82+
83+
- [Florent Hivert](https://www.lri.fr/~hivert/)
84+
- [Laurent Thery](https://www-sop.inria.fr/marelle/personnel/Laurent.Thery/moi.html)
85+
86+
This library is also the result of discussions with:
87+
88+
- Sophie Bernard
89+
- [Cyril Cohen](http://www.cyrilcohen.fr/)
90+
- [Laurence Rideau](http://www-sop.inria.fr/members/Laurence.Rideau/)
91+
92+
---

0 commit comments

Comments
 (0)