Skip to content

Commit 5b40420

Browse files
pi8027pi8027
authored
Bump MathComp version to >= 1.12.0 (#3)
* Bump MathComp version to 1.12.0 * Cleanup
1 parent c484e1f commit 5b40420

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

49 files changed

+1508
-2432
lines changed

‎.github/workflows/coq-ci.yml

-29
This file was deleted.

‎.github/workflows/docker-action.yml

+44
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
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:1.12.0-coq-8.11'
21+
- 'mathcomp/mathcomp:1.12.0-coq-8.12'
22+
- 'mathcomp/mathcomp:1.12.0-coq-8.13'
23+
- 'mathcomp/mathcomp:1.12.0-coq-8.14'
24+
- 'mathcomp/mathcomp:1.13.0-coq-8.11'
25+
- 'mathcomp/mathcomp:1.13.0-coq-8.12'
26+
- 'mathcomp/mathcomp:1.13.0-coq-8.13'
27+
- 'mathcomp/mathcomp:1.13.0-coq-8.14'
28+
- 'mathcomp/mathcomp:1.13.0-coq-dev'
29+
- 'mathcomp/mathcomp-dev:coq-8.11'
30+
- 'mathcomp/mathcomp-dev:coq-8.12'
31+
- 'mathcomp/mathcomp-dev:coq-8.13'
32+
- 'mathcomp/mathcomp-dev:coq-8.14'
33+
- 'mathcomp/mathcomp-dev:coq-dev'
34+
fail-fast: false
35+
steps:
36+
- uses: actions/checkout@v2
37+
- uses: coq-community/docker-coq-action@v1
38+
with:
39+
opam_file: 'coq-mathcomp-apery.opam'
40+
custom_image: ${{ matrix.image }}
41+
42+
# See also:
43+
# https://github.com/coq-community/docker-coq-action#readme
44+
# https://github.com/erikmd/docker-coq-github-action-demo

‎README.md

+11-7
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
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+
--->
15
# Apery
26

3-
[![CI][action-shield]][action-link]
7+
[![Docker CI][docker-action-shield]][docker-action-link]
48

5-
[action-shield]: https://github.com/math-comp/apery/workflows/CI/badge.svg?branch=master
6-
[action-link]: https://github.com/math-comp/apery/actions?query=workflow%3ACI
9+
[docker-action-shield]: https://github.com/math-comp/apery/workflows/Docker%20CI/badge.svg?branch=master
10+
[docker-action-link]: https://github.com/math-comp/apery/actions?query=workflow:"Docker%20CI"
711

812

913

@@ -23,13 +27,13 @@ remains the sole trusted code base.
2327
- Assia Mahboubi (initial)
2428
- Thomas Sibut-Pinote (initial)
2529
- License: [CeCILL-C](Licence_CeCILL-C_V1-en.txt)
26-
- Compatible Coq versions: 8.11
30+
- Compatible Coq versions: 8.11 or later
2731
- Additional dependencies:
28-
- [MathComp ssreflect 1.10](https://math-comp.github.io)
32+
- [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
2933
- [MathComp algebra](https://math-comp.github.io)
3034
- [MathComp field](https://math-comp.github.io)
31-
- [CoqEAL 1.0.3 or later](https://github.com/CoqEAL/CoqEAL)
32-
- [MathComp real closed fields 1.0.4 or later](https://github.com/math-comp/real-closed)
35+
- [CoqEAL 1.0.5 or later](https://github.com/CoqEAL/CoqEAL)
36+
- [MathComp real closed fields 1.1.2 or later](https://github.com/math-comp/real-closed)
3337
- [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
3438
- Coq namespace: `mathcomp.apery`
3539
- Related publication(s):

‎coq-mathcomp-apery.opam

+8-5
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
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: "[email protected]"
36
version: "dev"
@@ -17,15 +20,15 @@ computer algebra program (in this case in Maple/Algolib). These
1720
relations are formally checked a posteriori, so that Coq's kernel
1821
remains the sole trusted code base."""
1922

20-
build: [make "-j%{jobs}%" ]
23+
build: [make "-j%{jobs}%"]
2124
install: [make "install"]
2225
depends: [
23-
"coq" {>= "8.11" & < "8.12~"}
24-
"coq-mathcomp-ssreflect" {>= "1.10" & < "1.11~"}
26+
"coq" {(>= "8.11" & < "8.15~") | (= "dev")}
27+
"coq-mathcomp-ssreflect" {(>= "1.12" & < "1.14~") | (= "dev")}
2528
"coq-mathcomp-algebra"
2629
"coq-mathcomp-field"
27-
"coq-coqeal" {>= "1.0.3"}
28-
"coq-mathcomp-real-closed" {>= "1.0.4"}
30+
"coq-coqeal" {>= "1.0.5"}
31+
"coq-mathcomp-real-closed" {>= "1.1.2"}
2932
"coq-mathcomp-bigenough" {>= "1.0.0"}
3033
]
3134

‎include/ops_header.v

+2-5
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
Require Import Psatz.
2-
Require Import Field.
31
Require Import ZArith.
42

53
From mathcomp Require Import all_ssreflect all_algebra.
@@ -15,7 +13,6 @@ Set Implicit Arguments.
1513
Unset Strict Implicit.
1614
Unset Printing Implicit Defensive.
1715

18-
Import GRing.Theory.
19-
Import Num.Theory.
16+
Import Order.TTheory GRing.Theory Num.Theory.
2017

21-
Open Scope ring_scope.
18+
Local Open Scope ring_scope.

‎meta.yml

+35-9
Original file line numberDiff line numberDiff line change
@@ -43,19 +43,45 @@ license:
4343
file: Licence_CeCILL-C_V1-en.txt
4444

4545
supported_coq_versions:
46-
text: 8.11
47-
opam: '{>= "8.11" & < "8.12~"}'
46+
text: 8.11 or later
47+
opam: '{(>= "8.11" & < "8.15~") | (= "dev")}'
4848

4949
tested_coq_opam_versions:
50-
- version: '1.10.0-coq-8.11'
50+
- version: '1.12.0-coq-8.11'
5151
repo: 'mathcomp/mathcomp'
52+
- version: '1.12.0-coq-8.12'
53+
repo: 'mathcomp/mathcomp'
54+
- version: '1.12.0-coq-8.13'
55+
repo: 'mathcomp/mathcomp'
56+
- version: '1.12.0-coq-8.14'
57+
repo: 'mathcomp/mathcomp'
58+
- version: '1.13.0-coq-8.11'
59+
repo: 'mathcomp/mathcomp'
60+
- version: '1.13.0-coq-8.12'
61+
repo: 'mathcomp/mathcomp'
62+
- version: '1.13.0-coq-8.13'
63+
repo: 'mathcomp/mathcomp'
64+
- version: '1.13.0-coq-8.14'
65+
repo: 'mathcomp/mathcomp'
66+
- version: '1.13.0-coq-dev'
67+
repo: 'mathcomp/mathcomp'
68+
- version: 'coq-8.11'
69+
repo: 'mathcomp/mathcomp-dev'
70+
- version: 'coq-8.12'
71+
repo: 'mathcomp/mathcomp-dev'
72+
- version: 'coq-8.13'
73+
repo: 'mathcomp/mathcomp-dev'
74+
- version: 'coq-8.14'
75+
repo: 'mathcomp/mathcomp-dev'
76+
- version: 'coq-dev'
77+
repo: 'mathcomp/mathcomp-dev'
5278

5379
dependencies:
5480
- opam:
5581
name: coq-mathcomp-ssreflect
56-
version: '{>= "1.10" & < "1.11~"}'
82+
version: '{(>= "1.12" & < "1.14~") | (= "dev")}'
5783
description: |-
58-
[MathComp ssreflect 1.10](https://math-comp.github.io)
84+
[MathComp ssreflect 1.12 or later](https://math-comp.github.io)
5985
- opam:
6086
name: coq-mathcomp-algebra
6187
description: |-
@@ -66,14 +92,14 @@ dependencies:
6692
[MathComp field](https://math-comp.github.io)
6793
- opam:
6894
name: coq-coqeal
69-
version: '{>= "1.0.3"}'
95+
version: '{>= "1.0.5"}'
7096
description: |-
71-
[CoqEAL 1.0.3 or later](https://github.com/CoqEAL/CoqEAL)
97+
[CoqEAL 1.0.5 or later](https://github.com/CoqEAL/CoqEAL)
7298
- opam:
7399
name: coq-mathcomp-real-closed
74-
version: '{>= "1.0.4"}'
100+
version: '{>= "1.1.2"}'
75101
description: |-
76-
[MathComp real closed fields 1.0.4 or later](https://github.com/math-comp/real-closed)
102+
[MathComp real closed fields 1.1.2 or later](https://github.com/math-comp/real-closed)
77103
- opam:
78104
name: coq-mathcomp-bigenough
79105
version: '{>= "1.0.0"}'

0 commit comments

Comments
 (0)