Skip to content

Commit b171ce8

Browse files
affeldt-aistaffeldt-aist
committed
release MathComp-Analysis 1.13.0
1 parent 57e927c commit b171ce8

File tree

6 files changed

+303
-0
lines changed
  • released/packages
    • coq-mathcomp-analysis-stdlib/coq-mathcomp-analysis-stdlib.1.13.0
    • coq-mathcomp-analysis/coq-mathcomp-analysis.1.13.0
    • coq-mathcomp-classical/coq-mathcomp-classical.1.13.0
    • coq-mathcomp-experimental-reals/coq-mathcomp-experimental-reals.1.13.0
    • coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.13.0
    • coq-mathcomp-reals/coq-mathcomp-reals.1.13.0

6 files changed

+303
-0
lines changed

‎released/packages/coq-mathcomp-analysis-stdlib/coq-mathcomp-analysis-stdlib.1.13.0/opam

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
opam-version: "2.0"
2+
maintainer: "Reynald Affeldt <[email protected]>"
3+
4+
homepage: "https://github.com/math-comp/analysis"
5+
dev-repo: "git+https://github.com/math-comp/analysis.git"
6+
bug-reports: "https://github.com/math-comp/analysis/issues"
7+
license: "CECILL-C"
8+
9+
synopsis: "A library to link real numbers from mathematical components and Stdlib"
10+
description: """
11+
This package contains a library to link real numbers for
12+
the Coq proof-assistant using the Mathematical Components library and Stdlib."""
13+
14+
build: [make "-C" "analysis_stdlib" "-j%{jobs}%"]
15+
install: [make "-C" "analysis_stdlib" "install"]
16+
depends: [
17+
"coq-mathcomp-analysis" { = version}
18+
"coq-mathcomp-reals-stdlib"
19+
]
20+
21+
tags: [
22+
"category:Mathematics/Real Numbers"
23+
"keyword:real numbers"
24+
"keyword:reals"
25+
"logpath:mathcomp.reals_stdlib"
26+
]
27+
authors: [
28+
"Reynald Affeldt"
29+
"Alessandro Bruni"
30+
"Yves Bertot"
31+
"Cyril Cohen"
32+
"Marie Kerjean"
33+
"Assia Mahboubi"
34+
"Damien Rouhling"
35+
"Pierre Roux"
36+
"Kazuhiko Sakaguchi"
37+
"Zachary Stone"
38+
"Pierre-Yves Strub"
39+
"Laurent Théry"
40+
]
41+
42+
url {
43+
src: "https://github.com/math-comp/analysis/archive/1.13.0.tar.gz"
44+
checksum: "sha256=f976bf84d1c34ca5307d989eaf1a1471f74d39144c8a00d61bbf3aadd453b709"
45+
}

‎released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.1.13.0/opam

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
opam-version: "2.0"
2+
maintainer: "Reynald Affeldt <[email protected]>"
3+
4+
homepage: "https://github.com/math-comp/analysis"
5+
dev-repo: "git+https://github.com/math-comp/analysis.git"
6+
bug-reports: "https://github.com/math-comp/analysis/issues"
7+
license: "CECILL-C"
8+
9+
synopsis: "An analysis library for mathematical components"
10+
description: """
11+
This package contains a library for real analysis for
12+
the Coq proof-assistant and using the Mathematical Components library."""
13+
14+
build: [make "-C" "theories" "-j%{jobs}%"]
15+
install: [make "-C" "theories" "install"]
16+
depends: [
17+
"coq-mathcomp-reals" { = version}
18+
"coq-mathcomp-solvable"
19+
"coq-mathcomp-field"
20+
"coq-mathcomp-bigenough" { (>= "1.0.0") }
21+
]
22+
23+
tags: [
24+
"category:Mathematics/Real Calculus and Topology"
25+
"keyword:analysis"
26+
"keyword:Cantor"
27+
"keyword:topology"
28+
"keyword:real numbers"
29+
"keyword:sequence"
30+
"keyword:convexity"
31+
"keyword:Landau notation"
32+
"keyword:logarithm"
33+
"keyword:sin"
34+
"keyword:cos"
35+
"keyword:tangent"
36+
"keyword:trigonometric function"
37+
"keyword:exponential"
38+
"keyword:differentiation"
39+
"keyword:derivative"
40+
"keyword:measure theory"
41+
"keyword:integration"
42+
"keyword:Lebesgue"
43+
"keyword:probability"
44+
"logpath:mathcomp.analysis"
45+
]
46+
authors: [
47+
"Reynald Affeldt"
48+
"Alessandro Bruni"
49+
"Yves Bertot"
50+
"Cyril Cohen"
51+
"Marie Kerjean"
52+
"Assia Mahboubi"
53+
"Damien Rouhling"
54+
"Pierre Roux"
55+
"Kazuhiko Sakaguchi"
56+
"Zachary Stone"
57+
"Pierre-Yves Strub"
58+
"Laurent Théry"
59+
]
60+
61+
url {
62+
src: "https://github.com/math-comp/analysis/archive/1.13.0.tar.gz"
63+
checksum: "sha256=c5fb34eafa49c3d5a465db541fc478c83bd866f8fe11024cb1304c1d476801d5"
64+
}

‎released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.13.0/opam

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
opam-version: "2.0"
2+
maintainer: "Reynald Affeldt <[email protected]>"
3+
4+
homepage: "https://github.com/math-comp/analysis"
5+
dev-repo: "git+https://github.com/math-comp/analysis.git"
6+
bug-reports: "https://github.com/math-comp/analysis/issues"
7+
license: "CECILL-C"
8+
9+
synopsis: "A library for classical logic for mathematical components"
10+
description: """
11+
This repository contains a library for classical logic for
12+
the Coq proof-assistant and using the Mathematical Components library."""
13+
14+
build: [make "-C" "classical" "-j%{jobs}%"]
15+
install: [make "-C" "classical" "install"]
16+
depends: [
17+
("coq" {>= "8.20" & < "8.21~"}
18+
| "coq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
19+
"coq-mathcomp-ssreflect" { (>= "2.3.0" & < "2.5~") | (= "dev") }
20+
"coq-mathcomp-fingroup"
21+
"coq-mathcomp-algebra"
22+
"coq-mathcomp-finmap" { (>= "2.1.0") }
23+
"coq-hierarchy-builder" { (>= "1.8.0") }
24+
]
25+
26+
tags: [
27+
"category:Mathematics/Logic/Classical logic"
28+
"keyword:classical logic"
29+
"keyword:logic"
30+
"keyword:sets"
31+
"keyword:set theory"
32+
"keyword:function"
33+
"keyword:cardinal"
34+
"keyword:filter"
35+
"logpath:mathcomp.classical"
36+
]
37+
authors: [
38+
"Reynald Affeldt"
39+
"Alessandro Bruni"
40+
"Yves Bertot"
41+
"Cyril Cohen"
42+
"Marie Kerjean"
43+
"Assia Mahboubi"
44+
"Damien Rouhling"
45+
"Pierre Roux"
46+
"Kazuhiko Sakaguchi"
47+
"Zachary Stone"
48+
"Pierre-Yves Strub"
49+
"Laurent Théry"
50+
]
51+
52+
url {
53+
src: "https://github.com/math-comp/analysis/archive/1.13.0.tar.gz"
54+
checksum: "sha256=f976bf84d1c34ca5307d989eaf1a1471f74d39144c8a00d61bbf3aadd453b709"
55+
}

‎released/packages/coq-mathcomp-experimental-reals/coq-mathcomp-experimental-reals.1.13.0/opam

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
opam-version: "2.0"
2+
maintainer: "Reynald Affeldt <[email protected]>"
3+
4+
homepage: "https://github.com/math-comp/analysis"
5+
dev-repo: "git+https://github.com/math-comp/analysis.git"
6+
bug-reports: "https://github.com/math-comp/analysis/issues"
7+
license: "CECILL-C"
8+
9+
synopsis: "A library for alternative real numbers for mathematical components"
10+
description: """
11+
This package contains an experiment along real numbers
12+
made at the beginning of the MathComp-Analysis library
13+
(which now offers the coq-mathcomp-reals package).
14+
15+
Beware that this still contains a few Admitted."""
16+
17+
build: [make "-C" "experimental_reals" "-j%{jobs}%"]
18+
install: [make "-C" "experimental_reals" "install"]
19+
depends: [
20+
"coq-mathcomp-reals" { = version}
21+
"coq-mathcomp-bigenough" { (>= "1.0.0") }
22+
]
23+
24+
tags: [
25+
"category:Mathematics/Real Numbers"
26+
"keyword:real numbers"
27+
"keyword:reals"
28+
"logpath:mathcomp.experimental_reals"
29+
]
30+
authors: [
31+
"Reynald Affeldt"
32+
"Alessandro Bruni"
33+
"Yves Bertot"
34+
"Cyril Cohen"
35+
"Marie Kerjean"
36+
"Assia Mahboubi"
37+
"Damien Rouhling"
38+
"Pierre Roux"
39+
"Kazuhiko Sakaguchi"
40+
"Zachary Stone"
41+
"Pierre-Yves Strub"
42+
"Laurent Théry"
43+
]
44+
45+
url {
46+
src: "https://github.com/math-comp/analysis/archive/1.13.0.tar.gz"
47+
checksum: "sha256=f976bf84d1c34ca5307d989eaf1a1471f74d39144c8a00d61bbf3aadd453b709"
48+
}

‎released/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.13.0/opam

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
opam-version: "2.0"
2+
maintainer: "Reynald Affeldt <[email protected]>"
3+
4+
homepage: "https://github.com/math-comp/analysis"
5+
dev-repo: "git+https://github.com/math-comp/analysis.git"
6+
bug-reports: "https://github.com/math-comp/analysis/issues"
7+
license: "CECILL-C"
8+
9+
synopsis: "A library to link real numbers from mathematical components and Stdlib"
10+
description: """
11+
This package contains a library to link real numbers for
12+
the Coq proof-assistant using the Mathematical Components library and Stdlib."""
13+
14+
build: [make "-C" "reals_stdlib" "-j%{jobs}%"]
15+
install: [make "-C" "reals_stdlib" "install"]
16+
depends: [
17+
("coq" {< "8.21~"}
18+
| "rocq-stdlib" { (>= "9.0" & < "9.1~") | (= "dev") })
19+
"coq-mathcomp-reals" { = version}
20+
]
21+
22+
tags: [
23+
"category:Mathematics/Real Numbers"
24+
"keyword:real numbers"
25+
"keyword:reals"
26+
"logpath:mathcomp.reals_stdlib"
27+
]
28+
authors: [
29+
"Reynald Affeldt"
30+
"Alessandro Bruni"
31+
"Yves Bertot"
32+
"Cyril Cohen"
33+
"Marie Kerjean"
34+
"Assia Mahboubi"
35+
"Damien Rouhling"
36+
"Pierre Roux"
37+
"Kazuhiko Sakaguchi"
38+
"Zachary Stone"
39+
"Pierre-Yves Strub"
40+
"Laurent Théry"
41+
]
42+
43+
url {
44+
src: "https://github.com/math-comp/analysis/releases/download/1.13.0/analysis-1.13.0.tar.gz"
45+
checksum: "sha256=c5fb34eafa49c3d5a465db541fc478c83bd866f8fe11024cb1304c1d476801d5"
46+
}

‎released/packages/coq-mathcomp-reals/coq-mathcomp-reals.1.13.0/opam

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
opam-version: "2.0"
2+
maintainer: "Reynald Affeldt <[email protected]>"
3+
4+
homepage: "https://github.com/math-comp/analysis"
5+
dev-repo: "git+https://github.com/math-comp/analysis.git"
6+
bug-reports: "https://github.com/math-comp/analysis/issues"
7+
license: "CECILL-C"
8+
9+
synopsis: "A library for real numbers for mathematical components"
10+
description: """
11+
This package contains a library for real numbers for
12+
the Coq proof-assistant and using the Mathematical Components library."""
13+
14+
build: [make "-C" "reals" "-j%{jobs}%"]
15+
install: [make "-C" "reals" "install"]
16+
depends: [
17+
"coq-mathcomp-classical" { = version}
18+
]
19+
20+
tags: [
21+
"category:Mathematics/Real Numbers"
22+
"keyword:real numbers"
23+
"keyword:reals"
24+
"keyword:extended real numbers"
25+
"logpath:mathcomp.reals"
26+
]
27+
authors: [
28+
"Reynald Affeldt"
29+
"Alessandro Bruni"
30+
"Yves Bertot"
31+
"Cyril Cohen"
32+
"Marie Kerjean"
33+
"Assia Mahboubi"
34+
"Damien Rouhling"
35+
"Pierre Roux"
36+
"Kazuhiko Sakaguchi"
37+
"Zachary Stone"
38+
"Pierre-Yves Strub"
39+
"Laurent Théry"
40+
]
41+
42+
url {
43+
src: "https://github.com/math-comp/analysis/archive/1.13.0.tar.gz"
44+
checksum: "sha256=f976bf84d1c34ca5307d989eaf1a1471f74d39144c8a00d61bbf3aadd453b709"
45+
}

0 commit comments

Comments
 (0)