GeoCoq.2.4.1

GeoCoq · Mar 3, 2024 · ba255af · ba255af
1 parent 73cae2b
commit ba255af
Show file tree

Hide file tree

Showing 6 changed files with 210 additions and 0 deletions.
diff --git a/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.1/opam b/released/packages/coq-geocoq-axioms/coq-geocoq-axioms.2.4.1/opam
@@ -0,0 +1,35 @@
+opam-version: "2.0"
+synopsis: "A formalization of foundations of geometry in Coq"
+description: "This subpackage contains the axioms."
+maintainer: "Pierre Boutry <[email protected]>"
+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]>"]
+license: "LGPL 3"
+homepage: "http://geocoq.github.io/GeoCoq/"
+bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
+dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git"
+depends: [ "coq-geocoq-coinc" { = "2.4.1" } ]
+build: [
+  ["./configure-axioms.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [[make "install"]]
+tags: [ "keyword:geometry"
+        "keyword:neutral geometry"
+        "keyword:euclidean geometry"
+        "keyword:foundations"
+        "keyword:Tarski"
+        "keyword:Hilbert"
+        "keyword:Euclid"
+        "keyword:Elements"
+        "keyword:parallel postulates"
+        "category:Mathematics/Geometry/General"
+        "date:2024-03-03" ]
+url {
+  src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz"
+  checksum: "md5=14212f17e868a53ec0b6b84feda5c44d"
+}
diff --git a/released/packages/coq-geocoq-coinc/coq-geocoq-coinc.2.4.1/opam b/released/packages/coq-geocoq-coinc/coq-geocoq-coinc.2.4.1/opam
@@ -0,0 +1,26 @@
+opam-version: "2.0"
+synopsis: "A formalization of foundations of geometry in Coq"
+description: "This subpackage contains some tactics to deal with incidence properties."
+maintainer: "Pierre Boutry <[email protected]>"
+authors: ["Pierre Boutry <[email protected]>"
+          "Julien Narboux <[email protected]>"
+          "Pascal Schreck <[email protected]>"]
+license: "LGPL 3"
+homepage: "http://geocoq.github.io/GeoCoq/"
+bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
+dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git"
+depends: [ "coq" { (>= "8.7" & < "8.12~") } ]
+build: [
+  ["./configure-coinc.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [[make "install"]]
+tags: [ "keyword:geometry"
+        "keyword:automation"
+        "category:Mathematics/Geometry/General"
+        "date:2024-03-03" ]
+url {
+  src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz"
+  checksum: "md5=14212f17e868a53ec0b6b84feda5c44d"
+
+}
diff --git a/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.1/opam b/released/packages/coq-geocoq-elements/coq-geocoq-elements.2.4.1/opam
@@ -0,0 +1,29 @@
+opam-version: "2.0"
+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."
+maintainer: "Julien Narboux <[email protected]>"
+authors: ["Michael Beeson <[email protected]>"
+          "Julien Narboux <[email protected]>"
+          "Freek Wiedijk <[email protected]>"]
+license: "LGPL 3"
+homepage: "http://geocoq.github.io/GeoCoq/"
+bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
+dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git"
+depends: [ "coq-geocoq-axioms" { = "2.4.1" } ]
+build: [
+  ["./configure-elements.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [[make "install"]]
+tags: [ "keyword:geometry"
+        "keyword:neutral geometry"
+        "keyword:euclidean geometry"
+        "keyword:foundations"
+        "keyword:Euclid"
+        "keyword:Elements"
+        "category:Mathematics/Geometry/General"
+        "date:2024-03-03" ]
+url {
+  src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz"
+  checksum: "md5=14212f17e868a53ec0b6b84feda5c44d"
+}
diff --git a/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.1/opam b/released/packages/coq-geocoq-main/coq-geocoq-main.2.4.1/opam
@@ -0,0 +1,42 @@
+opam-version: "2.0"
+synopsis: "A formalization of foundations of geometry in Coq"
+description: "This subpackage contains the main developments from Hilbert's and Tarski's axiom systems."
+maintainer: "Pierre Boutry <[email protected]>"
+authors: ["Gabriel Braun <[email protected]>"
+          "Pierre Boutry <[email protected]>"
+          "Charly Gries <[email protected]>"
+          "Julien Narboux <[email protected]>"
+          "Pascal Schreck <[email protected]>"]
+license: "LGPL 3"
+homepage: "http://geocoq.github.io/GeoCoq/"
+bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
+dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git"
+depends: [ "coq-geocoq-axioms" { = "2.4.1" } ]
+build: [
+  ["mkdir" "main/"]
+  ["mv" "main.v" "main/"]
+  ["./configure-main.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [[make "install"]]
+tags: [ "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"
+        "category:Mathematics/Geometry/General"
+        "date:2024-03-03" ]
+url {
+  src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz"
+  checksum: "md5=14212f17e868a53ec0b6b84feda5c44d"
+}
diff --git a/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.1/opam b/released/packages/coq-geocoq-pof/coq-geocoq-pof.2.4.1/opam
@@ -0,0 +1,33 @@
+opam-version: "2.0"
+synopsis: "A formalization of foundations of geometry in Coq"
+description: "This subpackage contains a model of Tarski's axioms."
+maintainer: "Pierre Boutry <[email protected]>"
+authors: ["Pierre Boutry <[email protected]>"
+          "Cyril Cohen <[email protected]>"]
+license: "LGPL 3"
+homepage: "http://geocoq.github.io/GeoCoq/"
+bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
+dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git"
+depends: [
+  "coq-geocoq-main" { = "2.4.1" }
+  "coq-mathcomp-field" { >= "1.6.4" & < "1.11.0" }
+]
+build: [
+  ["mkdir" "-p" "Meta_theory2/Models"]
+  ["mv" "Meta_theory/Models/POF_to_Tarski.v" "Meta_theory2/Models"]
+  ["./configure-pof.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [[make "install"]]
+tags: [ "keyword:geometry"
+        "keyword:euclidean geometry"
+        "keyword:foundations"
+        "keyword:Tarski"
+        "keyword:model"
+        "keyword:Cartesian space"
+        "category:Mathematics/Geometry/General"
+        "date:2024-03-03" ]
+url {
+  src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz"
+  checksum: "md5=14212f17e868a53ec0b6b84feda5c44d"
+}
diff --git a/released/packages/coq-geocoq/coq-geocoq.2.4.1/opam b/released/packages/coq-geocoq/coq-geocoq.2.4.1/opam
@@ -0,0 +1,45 @@
+opam-version: "2.0"
+synopsis: "A formalization of foundations of geometry in Coq"
+description: "This package depends on all subpackages."
+maintainer: "Pierre Boutry <[email protected]>"
+authors: ["Michael Beeson <[email protected]>"
+          "Gabriel Braun <[email protected]>"
+          "Pierre Boutry <[email protected]>"
+          "Cyril Cohen <[email protected]>"
+          "Charly Gries <[email protected]>"
+          "Julien Narboux <[email protected]>"
+          "Pascal Schreck <[email protected]>"
+          "Freek Wiedijk <[email protected]>"]
+license: "LGPL 3"
+homepage: "http://geocoq.github.io/GeoCoq/"
+bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
+dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git"
+depends: [
+  "coq-geocoq-elements" { = "2.4.1" }
+  "coq-geocoq-pof" { = "2.4.1" }
+]
+tags: [ "keyword:geometry"
+        "keyword:neutral geometry"
+        "keyword:euclidean 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:Cartesian space"
+        "keyword:automation"
+        "category:Mathematics/Geometry/General"
+        "date:2024-03-03" ]
+url {
+  src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.1.tar.gz"
+  checksum: "md5=14212f17e868a53ec0b6b84feda5c44d"
+}