Skip to content

Commit

Permalink
[extra-dev] Add coq-mathcomp-reals, coq-mathcomp-altreals, coq-mathco…
Browse files Browse the repository at this point in the history
…mp-reals-stdlib and coq-mathcomp-analysis-stdlib
  • Loading branch information
proux01 committed Oct 29, 2024
1 parent 2560a7d commit 6389306
Show file tree
Hide file tree
Showing 6 changed files with 202 additions and 6 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"

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 repository contains a library for alternative real numbers for
the Coq proof-assistant and using the Mathematical Components library."""

build: [make "-C" "altreals" "-j%{jobs}%"]
install: [make "-C" "altreals" "install"]
depends: [
"coq-mathcomp-reals" { = version}
]

tags: [
"category:Mathematics/Real Numbers"
"keyword:real numbers"
"keyword:reals"
"logpath:mathcomp.altreals"
]
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: "git+https://github.com/math-comp/analysis.git#master"
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"

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 repository 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: "git+https://github.com/math-comp/analysis.git#master"
}
Original file line number Diff line number Diff line change
Expand Up @@ -14,21 +14,40 @@ the Coq proof-assistant and using the Mathematical Components library."""
build: [make "-C" "theories" "-j%{jobs}%"]
install: [make "-C" "theories" "install"]
depends: [
"coq-mathcomp-classical" { = version}
"coq-mathcomp-solvable" { (>= "1.13.0") }
"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:extended real numbers"
"keyword:filter"
"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"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,22 @@ the Coq proof-assistant and using the Mathematical Components library."""
build: [make "-C" "classical" "-j%{jobs}%"]
install: [make "-C" "classical" "install"]
depends: [
"coq" { (>= "8.14") }
"coq-mathcomp-ssreflect" { (>= "1.13.0") }
"coq" { (>= "8.19") }
"coq-mathcomp-ssreflect" { (>= "2.1.0") | (= "dev") }
"coq-mathcomp-fingroup"
"coq-mathcomp-algebra"
"coq-mathcomp-finmap" { (>= "1.5.1") }
"coq-hierarchy-builder" { (>= "1.2.0") }
"coq-mathcomp-finmap" { (>= "2.0.0") | (= "dev") }
"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"
"logpath:mathcomp.classical"
]
authors: [
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"

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 repository 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: "git+https://github.com/math-comp/analysis.git#master"
}
43 changes: 43 additions & 0 deletions extra-dev/packages/coq-mathcomp-reals/coq-mathcomp-reals.dev/opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"

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 repository 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"
"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: "git+https://github.com/math-comp/analysis.git#master"
}

0 comments on commit 6389306

Please sign in to comment.