forked from coq/opam
-
Notifications
You must be signed in to change notification settings - Fork 0
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
Showing
7 changed files
with
270 additions
and
0 deletions.
There are no files selected for viewing
40 changes: 40 additions & 0 deletions
40
released/packages/coq-geocoq-algebraic/coq-geocoq-algebraic.2.5.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,40 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "Pierre Boutry <[email protected]>" | ||
|
|
||
| homepage: "http://geocoq.github.io/GeoCoq/" | ||
| dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" | ||
| bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" | ||
| license: "LGPL-3.0-only" | ||
|
|
||
| synopsis: "A formalization of foundations of geometry in Coq" | ||
| description: "This subpackage contains a model of Tarski's axioms and some counter-models." | ||
|
|
||
| build: [["./configure-algebraic.sh"] | ||
| [make "-j%{jobs}%"]] | ||
| depends: [ | ||
| "coq-geocoq-main" { = version } | ||
| "coq-mathcomp-field" { >= "1.11.0" & < "2.0~" } | ||
| ] | ||
| conflicts: ["coq-geocoq-pof" { != version } ] | ||
|
|
||
| tags: [ | ||
| "category:Mathematics/Geometry/General" | ||
| "keyword:geometry" | ||
| "keyword:Euclidean geometry" | ||
| "keyword:hyperbolic geometry" | ||
| "keyword:foundations" | ||
| "keyword:Tarski" | ||
| "keyword:parallel postulates" | ||
| "keyword:model" | ||
| "keyword:counter-model" | ||
| "keyword:Cartesian space" | ||
| ] | ||
| authors: [ | ||
| "Pierre Boutry <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Stéphane Kastenbaum <[email protected]>" | ||
| ] | ||
|
|
||
| url { | ||
| src: "git+https://github.com/GeoCoq/GeoCoq.git#6a4984c058d409d1163c7c2e9227bd5fc570ed49" | ||
| } |
39 changes: 39 additions & 0 deletions
39
released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.5.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,39 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "Pierre Boutry <[email protected]>" | ||
|
|
||
| homepage: "http://geocoq.github.io/GeoCoq/" | ||
| dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" | ||
| bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" | ||
| license: "LGPL-3.0-only" | ||
|
|
||
| synopsis: "A formalization of foundations of geometry in Coq" | ||
| description: "This subpackage contains the axioms." | ||
|
|
||
| build: [["./configure-axioms.sh"] | ||
| [make "-j%{jobs}%"]] | ||
| depends: ["coq-geocoq-coinc" { = version }] | ||
|
|
||
| tags: [ | ||
| "category:Mathematics/Geometry/General" | ||
| "keyword:geometry" | ||
| "keyword:neutral geometry" | ||
| "keyword:Euclidean geometry" | ||
| "keyword:foundations" | ||
| "keyword:Tarski" | ||
| "keyword:Hilbert" | ||
| "keyword:Euclid" | ||
| "keyword:Elements" | ||
| "keyword:parallel postulates" | ||
| ] | ||
| authors: [ | ||
| "Michael Beeson <[email protected]>" | ||
| "Gabriel Braun <[email protected]>" | ||
| "Pierre Boutry <[email protected]>" | ||
| "Charly Gries <[email protected]>" | ||
| "Julien Narboux <[email protected]>" | ||
| "Pascal Schreck <[email protected]>" | ||
| ] | ||
|
|
||
| url { | ||
| src: "git+https://github.com/GeoCoq/GeoCoq.git#6a4984c058d409d1163c7c2e9227bd5fc570ed49" | ||
| } |
29 changes: 29 additions & 0 deletions
29
released/packages/coq-geocoq-coinc/coq-geocoq-coinc.2.5.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,29 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "Pierre Boutry <[email protected]>" | ||
|
|
||
| homepage: "http://geocoq.github.io/GeoCoq/" | ||
| dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" | ||
| bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" | ||
| license: "LGPL-3.0-only" | ||
|
|
||
| synopsis: "A formalization of foundations of geometry in Coq" | ||
| description: "This subpackage contains some tactics to deal with incidence properties." | ||
|
|
||
| build: [["./configure-coinc.sh"] | ||
| [make "-j%{jobs}%"]] | ||
| depends: ["coq" { >= "8.10" } ] | ||
|
|
||
| tags: [ | ||
| "category:Mathematics/Geometry/General" | ||
| "keyword:geometry" | ||
| "keyword:automation" | ||
| ] | ||
| authors: [ | ||
| "Pierre Boutry <[email protected]>" | ||
| "Julien Narboux <[email protected]>" | ||
| "Pascal Schreck <[email protected]>" | ||
| ] | ||
|
|
||
| url { | ||
| src: "git+https://github.com/GeoCoq/GeoCoq.git#6a4984c058d409d1163c7c2e9227bd5fc570ed49" | ||
| } |
33 changes: 33 additions & 0 deletions
33
released/packages/coq-geocoq-elements/coq-geocoq-elements.2.5.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,33 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "Pierre Boutry <[email protected]>" | ||
|
|
||
| homepage: "http://geocoq.github.io/GeoCoq/" | ||
| dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" | ||
| bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" | ||
| license: "LGPL-3.0-only" | ||
|
|
||
| synopsis: "A formalization of foundations of geometry in Coq" | ||
| description: "This subpackage contains a formalization of Euclid's proofs from Book I of the Elements." | ||
|
|
||
| build: [["./configure-elements.sh"] | ||
| [make "-j%{jobs}%"]] | ||
| depends: ["coq-geocoq-axioms" { = version }] | ||
|
|
||
| tags: [ | ||
| "category:Mathematics/Geometry/General" | ||
| "keyword:geometry" | ||
| "keyword:neutral geometry" | ||
| "keyword:Euclidean geometry" | ||
| "keyword:foundations" | ||
| "keyword:Euclid" | ||
| "keyword:Elements" | ||
| ] | ||
| authors: [ | ||
| "Michael Beeson <[email protected]>" | ||
| "Julien Narboux <[email protected]>" | ||
| "Freek Wiedijk <[email protected]>" | ||
| ] | ||
|
|
||
| url { | ||
| src: "git+https://github.com/GeoCoq/GeoCoq.git#6a4984c058d409d1163c7c2e9227bd5fc570ed49" | ||
| } |
44 changes: 44 additions & 0 deletions
44
released/packages/coq-geocoq-main/coq-geocoq-main.2.5.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: "Pierre Boutry <[email protected]>" | ||
|
|
||
| homepage: "http://geocoq.github.io/GeoCoq/" | ||
| dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" | ||
| bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" | ||
| license: "LGPL-3.0-only" | ||
|
|
||
| synopsis: "A formalization of foundations of geometry in Coq" | ||
| description: "This subpackage contains the main developments from Hilbert's and Tarski's axiom systems." | ||
|
|
||
| build: [["./configure-main.sh"] | ||
| [make "-j%{jobs}%"]] | ||
| depends: ["coq-geocoq-axioms" { = version }] | ||
|
|
||
| tags: [ | ||
| "category:Mathematics/Geometry/General" | ||
| "keyword:geometry" | ||
| "keyword:neutral geometry" | ||
| "keyword:Euclidean geometry" | ||
| "keyword:foundations" | ||
| "keyword:Tarski" | ||
| "keyword:Hilbert" | ||
| "keyword:Euclid" | ||
| "keyword:Pappus" | ||
| "keyword:Desargues" | ||
| "keyword:arithmetization" | ||
| "keyword:Pythagoras" | ||
| "keyword:Thales' intercept theorem" | ||
| "keyword:continuity" | ||
| "keyword:ruler and compass" | ||
| "keyword:parallel postulates" | ||
| ] | ||
| authors: [ | ||
| "Gabriel Braun <[email protected]>" | ||
| "Pierre Boutry <[email protected]>" | ||
| "Charly Gries <[email protected]>" | ||
| "Julien Narboux <[email protected]>" | ||
| "Pascal Schreck <[email protected]>" | ||
| ] | ||
|
|
||
| url { | ||
| src: "git+https://github.com/GeoCoq/GeoCoq.git#6a4984c058d409d1163c7c2e9227bd5fc570ed49" | ||
| } |
30 changes: 30 additions & 0 deletions
30
released/packages/coq-geocoq-pof/coq-geocoq-pof.2.5.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,30 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "Pierre Boutry <[email protected]>" | ||
|
|
||
| homepage: "http://geocoq.github.io/GeoCoq/" | ||
| dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" | ||
| bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" | ||
| license: "LGPL-3.0-only" | ||
|
|
||
| synopsis: "A formalization of foundations of geometry in Coq" | ||
| description: "This is a virtual package that can be safely removed." | ||
|
|
||
| depends: ["coq-geocoq-algebraic" { = version }] | ||
|
|
||
| tags: [ | ||
| "category:Mathematics/Geometry/General" | ||
| "keyword:geometry" | ||
| "keyword:Euclidean geometry" | ||
| "keyword:hyperbolic geometry" | ||
| "keyword:foundations" | ||
| "keyword:Tarski" | ||
| "keyword:parallel postulates" | ||
| "keyword:model" | ||
| "keyword:counter-model" | ||
| "keyword:Cartesian space" | ||
| ] | ||
| authors: [ | ||
| "Pierre Boutry <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Stéphane Kastenbaum <[email protected]>" | ||
| ] |
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,55 @@ | ||
| opam-version: "2.0" | ||
| maintainer: "Pierre Boutry <[email protected]>" | ||
|
|
||
| homepage: "http://geocoq.github.io/GeoCoq/" | ||
| dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" | ||
| bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" | ||
| license: "LGPL-3.0-only" | ||
|
|
||
| synopsis: "A formalization of foundations of geometry in Coq" | ||
| description: "This package depends on all subpackages." | ||
|
|
||
| depends: [ | ||
| "coq-geocoq-algebraic" { = version } | ||
| "coq-geocoq-elements" { = version } | ||
| ] | ||
|
|
||
| tags: [ | ||
| "category:Mathematics/Geometry/General" | ||
| "keyword:geometry" | ||
| "keyword:neutral geometry" | ||
| "keyword:Euclidean geometry" | ||
| "keyword:hyperbolic geometry" | ||
| "keyword:foundations" | ||
| "keyword:Tarski" | ||
| "keyword:Hilbert" | ||
| "keyword:Euclid" | ||
| "keyword:Elements" | ||
| "keyword:Pappus" | ||
| "keyword:Desargues" | ||
| "keyword:arithmetization" | ||
| "keyword:Pythagoras" | ||
| "keyword:Thales' intercept theorem" | ||
| "keyword:continuity" | ||
| "keyword:ruler and compass" | ||
| "keyword:parallel postulates" | ||
| "keyword:model" | ||
| "keyword:counter-model" | ||
| "keyword:Cartesian space" | ||
| "keyword:automation" | ||
| ] | ||
| authors: [ | ||
| "Michael Beeson <[email protected]>" | ||
| "Gabriel Braun <[email protected]>" | ||
| "Pierre Boutry <[email protected]>" | ||
| "Cyril Cohen <[email protected]>" | ||
| "Charly Gries <[email protected]>" | ||
| "Stéphane Kastenbaum <[email protected]>" | ||
| "Julien Narboux <[email protected]>" | ||
| "Pascal Schreck <[email protected]>" | ||
| "Freek Wiedijk <[email protected]>" | ||
| ] | ||
|
|
||
| url { | ||
| src: "git+https://github.com/GeoCoq/GeoCoq.git#6a4984c058d409d1163c7c2e9227bd5fc570ed49" | ||
| } |