-
Notifications
You must be signed in to change notification settings - Fork 166
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
d04aed1
commit 71206c3
Showing
6 changed files
with
300 additions
and
0 deletions.
There are no files selected for viewing
45 changes: 45 additions & 0 deletions
45
released/packages/coq-mathcomp-analysis-stdlib/coq-mathcomp-analysis-stdlib.1.7.0/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
opam-version: "2.0" | ||
maintainer: "Reynald Affeldt <[email protected]>" | ||
|
||
homepage: "https://github.com/math-comp/analysis" | ||
dev-repo: "git+https://github.com/math-comp/analysis.git" | ||
bug-reports: "https://github.com/math-comp/analysis/issues" | ||
license: "CECILL-C" | ||
|
||
synopsis: "A library to link real numbers from mathematical components and Stdlib" | ||
description: """ | ||
This package contains a library to link real numbers for | ||
the Coq proof-assistant using the Mathematical Components library and Stdlib.""" | ||
|
||
build: [make "-C" "analysis_stdlib" "-j%{jobs}%"] | ||
install: [make "-C" "analysis_stdlib" "install"] | ||
depends: [ | ||
"coq-mathcomp-analysis" { = version} | ||
"coq-mathcomp-reals-stdlib" | ||
] | ||
|
||
tags: [ | ||
"category:Mathematics/Real Numbers" | ||
"keyword:real numbers" | ||
"keyword:reals" | ||
"logpath:mathcomp.reals_stdlib" | ||
] | ||
authors: [ | ||
"Reynald Affeldt" | ||
"Alessandro Bruni" | ||
"Yves Bertot" | ||
"Cyril Cohen" | ||
"Marie Kerjean" | ||
"Assia Mahboubi" | ||
"Damien Rouhling" | ||
"Pierre Roux" | ||
"Kazuhiko Sakaguchi" | ||
"Zachary Stone" | ||
"Pierre-Yves Strub" | ||
"Laurent Théry" | ||
] | ||
|
||
url { | ||
src: "https://github.com/math-comp/analysis/archive/1.7.0.tar.gz" | ||
checksum: "sha256=54c6db0f72a8302000bd28c3ec9b26c63f3c620282e3bd714c9c84bd8bafa861" | ||
} |
64 changes: 64 additions & 0 deletions
64
released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.1.7.0/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
opam-version: "2.0" | ||
maintainer: "Reynald Affeldt <[email protected]>" | ||
|
||
homepage: "https://github.com/math-comp/analysis" | ||
dev-repo: "git+https://github.com/math-comp/analysis.git" | ||
bug-reports: "https://github.com/math-comp/analysis/issues" | ||
license: "CECILL-C" | ||
|
||
synopsis: "An analysis library for mathematical components" | ||
description: """ | ||
This package contains a library for real analysis for | ||
the Coq proof-assistant and using the Mathematical Components library.""" | ||
|
||
build: [make "-C" "theories" "-j%{jobs}%"] | ||
install: [make "-C" "theories" "install"] | ||
depends: [ | ||
"coq-mathcomp-reals" { = version} | ||
"coq-mathcomp-solvable" | ||
"coq-mathcomp-field" | ||
"coq-mathcomp-bigenough" { (>= "1.0.0") } | ||
] | ||
|
||
tags: [ | ||
"category:Mathematics/Real Calculus and Topology" | ||
"keyword:analysis" | ||
"keyword:Cantor" | ||
"keyword:topology" | ||
"keyword:real numbers" | ||
"keyword:sequence" | ||
"keyword:convexity" | ||
"keyword:Landau notation" | ||
"keyword:logarithm" | ||
"keyword:sin" | ||
"keyword:cos" | ||
"keyword:tangent" | ||
"keyword:trigonometric function" | ||
"keyword:exponential" | ||
"keyword:differentiation" | ||
"keyword:derivative" | ||
"keyword:measure theory" | ||
"keyword:integration" | ||
"keyword:Lebesgue" | ||
"keyword:probability" | ||
"logpath:mathcomp.analysis" | ||
] | ||
authors: [ | ||
"Reynald Affeldt" | ||
"Alessandro Bruni" | ||
"Yves Bertot" | ||
"Cyril Cohen" | ||
"Marie Kerjean" | ||
"Assia Mahboubi" | ||
"Damien Rouhling" | ||
"Pierre Roux" | ||
"Kazuhiko Sakaguchi" | ||
"Zachary Stone" | ||
"Pierre-Yves Strub" | ||
"Laurent Théry" | ||
] | ||
|
||
url { | ||
src: "https://github.com/math-comp/analysis/archive/1.7.0.tar.gz" | ||
checksum: "sha256=54c6db0f72a8302000bd28c3ec9b26c63f3c620282e3bd714c9c84bd8bafa861" | ||
} |
54 changes: 54 additions & 0 deletions
54
released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.7.0/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,54 @@ | ||
opam-version: "2.0" | ||
maintainer: "Reynald Affeldt <[email protected]>" | ||
|
||
homepage: "https://github.com/math-comp/analysis" | ||
dev-repo: "git+https://github.com/math-comp/analysis.git" | ||
bug-reports: "https://github.com/math-comp/analysis/issues" | ||
license: "CECILL-C" | ||
|
||
synopsis: "A library for classical logic for mathematical components" | ||
description: """ | ||
This repository contains a library for classical logic for | ||
the Coq proof-assistant and using the Mathematical Components library.""" | ||
|
||
build: [make "-C" "classical" "-j%{jobs}%"] | ||
install: [make "-C" "classical" "install"] | ||
depends: [ | ||
"coq" { (>= "8.19" & < "8.21~") | (= "dev") } | ||
"coq-mathcomp-ssreflect" { (>= "2.1.0") } | ||
"coq-mathcomp-fingroup" | ||
"coq-mathcomp-algebra" | ||
"coq-mathcomp-finmap" { (>= "2.0.0") } | ||
"coq-hierarchy-builder" { (>= "1.4.0") } | ||
] | ||
|
||
tags: [ | ||
"category:Mathematics/Logic/Classical logic" | ||
"keyword:classical logic" | ||
"keyword:logic" | ||
"keyword:sets" | ||
"keyword:set theory" | ||
"keyword:function" | ||
"keyword:cardinal" | ||
"keyword:filter" | ||
"logpath:mathcomp.classical" | ||
] | ||
authors: [ | ||
"Reynald Affeldt" | ||
"Alessandro Bruni" | ||
"Yves Bertot" | ||
"Cyril Cohen" | ||
"Marie Kerjean" | ||
"Assia Mahboubi" | ||
"Damien Rouhling" | ||
"Pierre Roux" | ||
"Kazuhiko Sakaguchi" | ||
"Zachary Stone" | ||
"Pierre-Yves Strub" | ||
"Laurent Théry" | ||
] | ||
|
||
url { | ||
src: "https://github.com/math-comp/analysis/archive/1.7.0.tar.gz" | ||
checksum: "sha256=54c6db0f72a8302000bd28c3ec9b26c63f3c620282e3bd714c9c84bd8bafa861" | ||
} |
48 changes: 48 additions & 0 deletions
48
released/packages/coq-mathcomp-experimental-reals/coq-mathcomp-experimental-reals.1.7.0/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,48 @@ | ||
opam-version: "2.0" | ||
maintainer: "Reynald Affeldt <[email protected]>" | ||
|
||
homepage: "https://github.com/math-comp/analysis" | ||
dev-repo: "git+https://github.com/math-comp/analysis.git" | ||
bug-reports: "https://github.com/math-comp/analysis/issues" | ||
license: "CECILL-C" | ||
|
||
synopsis: "A library for alternative real numbers for mathematical components" | ||
description: """ | ||
This package contains an experiment along real numbers | ||
made at the beginning of the MathComp-Analysis library | ||
(which now offers the coq-mathcomp-reals package). | ||
|
||
Beware that this still contains a few Admitted.""" | ||
|
||
build: [make "-C" "experimental_reals" "-j%{jobs}%"] | ||
install: [make "-C" "experimental_reals" "install"] | ||
depends: [ | ||
"coq-mathcomp-reals" { = version} | ||
"coq-mathcomp-bigenough" { (>= "1.0.0") } | ||
] | ||
|
||
tags: [ | ||
"category:Mathematics/Real Numbers" | ||
"keyword:real numbers" | ||
"keyword:reals" | ||
"logpath:mathcomp.experimental_reals" | ||
] | ||
authors: [ | ||
"Reynald Affeldt" | ||
"Alessandro Bruni" | ||
"Yves Bertot" | ||
"Cyril Cohen" | ||
"Marie Kerjean" | ||
"Assia Mahboubi" | ||
"Damien Rouhling" | ||
"Pierre Roux" | ||
"Kazuhiko Sakaguchi" | ||
"Zachary Stone" | ||
"Pierre-Yves Strub" | ||
"Laurent Théry" | ||
] | ||
|
||
url { | ||
src: "https://github.com/math-comp/analysis/archive/1.7.0.tar.gz" | ||
checksum: "sha256=54c6db0f72a8302000bd28c3ec9b26c63f3c620282e3bd714c9c84bd8bafa861" | ||
} |
44 changes: 44 additions & 0 deletions
44
released/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.1.7.0/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
opam-version: "2.0" | ||
maintainer: "Reynald Affeldt <[email protected]>" | ||
|
||
homepage: "https://github.com/math-comp/analysis" | ||
dev-repo: "git+https://github.com/math-comp/analysis.git" | ||
bug-reports: "https://github.com/math-comp/analysis/issues" | ||
license: "CECILL-C" | ||
|
||
synopsis: "A library to link real numbers from mathematical components and Stdlib" | ||
description: """ | ||
This package contains a library to link real numbers for | ||
the Coq proof-assistant using the Mathematical Components library and Stdlib.""" | ||
|
||
build: [make "-C" "reals_stdlib" "-j%{jobs}%"] | ||
install: [make "-C" "reals_stdlib" "install"] | ||
depends: [ | ||
"coq-mathcomp-reals" { = version} | ||
] | ||
|
||
tags: [ | ||
"category:Mathematics/Real Numbers" | ||
"keyword:real numbers" | ||
"keyword:reals" | ||
"logpath:mathcomp.reals_stdlib" | ||
] | ||
authors: [ | ||
"Reynald Affeldt" | ||
"Alessandro Bruni" | ||
"Yves Bertot" | ||
"Cyril Cohen" | ||
"Marie Kerjean" | ||
"Assia Mahboubi" | ||
"Damien Rouhling" | ||
"Pierre Roux" | ||
"Kazuhiko Sakaguchi" | ||
"Zachary Stone" | ||
"Pierre-Yves Strub" | ||
"Laurent Théry" | ||
] | ||
|
||
url { | ||
src: "https://github.com/math-comp/analysis/archive/1.7.0.tar.gz" | ||
checksum: "sha256=54c6db0f72a8302000bd28c3ec9b26c63f3c620282e3bd714c9c84bd8bafa861" | ||
} |
45 changes: 45 additions & 0 deletions
45
released/packages/coq-mathcomp-reals/coq-mathcomp-reals.1.7.0/opam
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
opam-version: "2.0" | ||
maintainer: "Reynald Affeldt <[email protected]>" | ||
|
||
homepage: "https://github.com/math-comp/analysis" | ||
dev-repo: "git+https://github.com/math-comp/analysis.git" | ||
bug-reports: "https://github.com/math-comp/analysis/issues" | ||
license: "CECILL-C" | ||
|
||
synopsis: "A library for real numbers for mathematical components" | ||
description: """ | ||
This package contains a library for real numbers for | ||
the Coq proof-assistant and using the Mathematical Components library.""" | ||
|
||
build: [make "-C" "reals" "-j%{jobs}%"] | ||
install: [make "-C" "reals" "install"] | ||
depends: [ | ||
"coq-mathcomp-classical" { = version} | ||
] | ||
|
||
tags: [ | ||
"category:Mathematics/Real Numbers" | ||
"keyword:real numbers" | ||
"keyword:reals" | ||
"keyword:extended real numbers" | ||
"logpath:mathcomp.reals" | ||
] | ||
authors: [ | ||
"Reynald Affeldt" | ||
"Alessandro Bruni" | ||
"Yves Bertot" | ||
"Cyril Cohen" | ||
"Marie Kerjean" | ||
"Assia Mahboubi" | ||
"Damien Rouhling" | ||
"Pierre Roux" | ||
"Kazuhiko Sakaguchi" | ||
"Zachary Stone" | ||
"Pierre-Yves Strub" | ||
"Laurent Théry" | ||
] | ||
|
||
url { | ||
src: "https://github.com/math-comp/analysis/archive/1.7.0.tar.gz" | ||
checksum: "sha256=54c6db0f72a8302000bd28c3ec9b26c63f3c620282e3bd714c9c84bd8bafa861" | ||
} |