diff --git a/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.13.1/opam b/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.13.1/opam deleted file mode 100644 index eff8b8781e..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.13.1/opam +++ /dev/null @@ -1,55 +0,0 @@ -opam-version: "2.0" -name: "coq-compcert" -synopsis: "The CompCert C compiler (64 bit)" -maintainer: "Michael Soegtrop" -authors: "Xavier Leroy " -license: "INRIA Non-Commercial License Agreement" -tags: [ - "category:Computer Science/Semantics and Compilation/Compilation" - "category:Computer Science/Semantics and Compilation/Semantics" - "keyword:C" - "keyword:compiler" - "logpath:compcert" - "date:2022-11-25" -] -homepage: "http://compcert.inria.fr/" -bug-reports: "https://github.com/AbsInt/CompCert/issues" -depends: [ - "coq" {>= "8.12.0" & < "8.19~"} - "menhir" {>= "20190626" & != "dev"} - "ocaml" {>= "4.05.0" & < "5~"} - "coq-flocq" {>= "4.1.0" & < "5~"} - "coq-menhirlib" {>= "20190626"} -] -build: [ - [ - "./configure" - "amd64-linux" {os = "linux" & arch = "x86_64"} - "amd64-macosx" {os = "macos" & arch = "x86_64"} - "arm64-linux" {os = "linux" & (arch = "arm64" | arch = "aarch64")} - "arm64-macosx" {os = "macos" & (arch = "arm64" | arch = "aarch64")} - "amd64-cygwin" {os = "cygwin"} - "amd64-cygwin" {os = "win32" & os-distribution = "cygwinports"} - "-toolprefix" - {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} - "x86_64-pc-cygwin-" - {os = "win32" & os-distribution = "cygwinports" & arch = "i686"} - "-prefix" - "%{prefix}%" - "-install-coqdev" - "-clightgen" - "-use-external-Flocq" - "-use-external-MenhirLib" - "-coqdevdir" - "%{lib}%/coq/user-contrib/compcert" - "-ignore-coq-version" - ] - [make "-j%{jobs}%" {ocaml:version >= "4.06"}] -] -install: [make "install"] -dev-repo: "git+https://github.com/AbsInt/CompCert.git" -url { - src: "https://github.com/AbsInt/CompCert/archive/v3.13.1.tar.gz" - checksum: - "sha512=828a2f700e32400fc9d3ad2265b67194c48b10fef7f4b6bc1ed5a35d556088cc7defb697faf38c8b871b5b55e58e05f563e827255d2fc9bb964ac5f2cc1024d0" -} diff --git a/opam/opam-coq-archive/released/packages/coq-corn/coq-corn.8.18.0/opam b/opam/opam-coq-archive/released/packages/coq-corn/coq-corn.8.18.0/opam deleted file mode 100644 index 539d053285..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-corn/coq-corn.8.18.0/opam +++ /dev/null @@ -1,98 +0,0 @@ -opam-version: "2.0" -maintainer: "b.a.w.spitters@gmail.com" -version: "dev" - -homepage: "https://github.com/coq-community/corn" -dev-repo: "git+https://github.com/coq-community/corn.git" -bug-reports: "https://github.com/coq-community/corn/issues" -license: "GPL-2.0" - -synopsis: "The Coq Constructive Repository at Nijmegen." -description: """ -CoRN includes the following parts: - -- Algebraic Hierarchy - - An axiomatic formalization of the most common algebraic - structures, including setoids, monoids, groups, rings, - fields, ordered fields, rings of polynomials, real and - complex numbers - -- Model of the Real Numbers - - Construction of a concrete real number structure - satisfying the previously defined axioms - -- Fundamental Theorem of Algebra - - A proof that every non-constant polynomial on the complex - plane has at least one root - -- Real Calculus - - A collection of elementary results on real analysis, - including continuity, differentiability, integration, - Taylor's theorem and the Fundamental Theorem of Calculus - -- Exact Real Computation - - Fast verified computation inside Coq. This includes: real numbers, functions, - integrals, graphs of functions, differential equations. -""" - -build: [ - ["./configure.sh"] - [make "-j%{jobs}%"] -] -install: [make "install"] -depends: [ - "coq" {(>= "8.14" & < "8.19~") | (= "dev")} - "coq-math-classes" {(>= "8.8.1") | (= "dev")} - "coq-bignums" -] - -tags: [ - "category:Mathematics/Algebra" - "category:Mathematics/Real Calculus and Topology" - "category:Mathematics/Exact Real computation" - "keyword:constructive mathematics" - "keyword:algebra" - "keyword:real calculus" - "keyword:real numbers" - "keyword:Fundamental Theorem of Algebra" - "logpath:CoRN" - "date:2023-10-16" -] -authors: [ - "Evgeny Makarov" - "Robbert Krebbers" - "Eelis van der Weegen" - "Bas Spitters" - "Jelle Herold" - "Russell O'Connor" - "Cezary Kaliszyk" - "Dan Synek" - "Luís Cruz-Filipe" - "Milad Niqui" - "Iris Loeb" - "Herman Geuvers" - "Randy Pollack" - "Freek Wiedijk" - "Jan Zwanenburg" - "Dimitri Hendriks" - "Henk Barendregt" - "Mariusz Giero" - "Rik van Ginneken" - "Dimitri Hendriks" - "Sébastien Hinderer" - "Bart Kirkels" - "Pierre Letouzey" - "Lionel Mamane" - "Nickolay Shmyrev" - "Vincent Semeria" -] - -url { - src: "https://github.com/coq-community/corn/archive/8.18.0.tar.gz" - checksum: "sha512=cd61c8314fcbec3b38429e94c77ff76caccfb38cbfbc95faf9bbe127f86756299d9744a288a36c4cf9c02e0a8701e57491eab0eab44747458bcbc021e8f3b408" -} \ No newline at end of file diff --git a/opam/opam-coq-archive/released/packages/coq-math-classes/coq-math-classes.8.18.0/opam b/opam/opam-coq-archive/released/packages/coq-math-classes/coq-math-classes.8.18.0/opam deleted file mode 100644 index 8b24ff2f0f..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-math-classes/coq-math-classes.8.18.0/opam +++ /dev/null @@ -1,49 +0,0 @@ -opam-version: "2.0" -maintainer: "b.a.w.spitters@gmail.com" - -homepage: "https://github.com/coq-community/math-classes" -dev-repo: "git+https://github.com/coq-community/math-classes.git" -bug-reports: "https://github.com/coq-community/math-classes/issues" -license: "MIT" - -synopsis: "A library of abstract interfaces for mathematical structures in Coq" -description: """ -Math classes is a library of abstract interfaces for mathematical -structures, such as: - -* Algebraic hierarchy (groups, rings, fields, …) -* Relations, orders, … -* Categories, functors, universal algebra, … -* Numbers: N, Z, Q, … -* Operations, (shift, power, abs, …) - -It is heavily based on Coq’s new type classes in order to provide: -structure inference, multiple inheritance/sharing, convenient -algebraic manipulation (e.g. rewriting) and idiomatic use of -notations. -""" - -build: [ - [ "./configure.sh" ] - [ make "-j%{jobs}%" ] -] -install: [make "install"] -depends: [ - "coq" {>= "8.11" & < "8.19~"} - "coq-bignums" -] - -tags: [ - "logpath:MathClasses" - "date:2023-03-04" -] -authors: [ - "Eelis van der Weegen" - "Bas Spitters" - "Robbert Krebbers" -] - -url { - src: "https://github.com/coq-community/math-classes/archive/refs/tags/8.18.0.tar.gz" - checksum: "sha512=ee593e4f851e25b0396176b3ecf62c1c504cde06eedbefd8eef7e932cc21967ddf2b38a9a20087b4074203dc66312316c0b0748ae6605f6734c312a010297621" -} diff --git a/opam/opam-coq-archive/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam b/opam/opam-coq-archive/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam deleted file mode 100644 index 6d881c038b..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-mtac2/coq-mtac2.1.4+8.18/opam +++ /dev/null @@ -1,25 +0,0 @@ -opam-version: "1.2" -maintainer: "beta.ziliani@gmail.com" -homepage: "https://github.com/Mtac2/Mtac2" -dev-repo: "https://github.com/Mtac2/Mtac2.git" -bug-reports: "https://github.com/Mtac2/Mtac2/issues" -authors: ["Beta Ziliani " "Jan-Oliver Kaiser " "Yann Régis-Gianas "] -license: "MIT" -build: [ - ["./configure.sh"] - [make "-j%{jobs}%"] -] -install: [ - [make "install"] -] -remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Mtac2"] -depends: [ - "coq" {>= "8.18"} - "coq-unicoq" -] -url { - src: "https://github.com/Mtac2/Mtac2/archive/refs/tags/v1.4-coq8.18.tar.gz" - checksum: [ - "sha512=50a12d086da0416774b4464a234df7ce86c191c45345b2951b6c6ecdbe7675e215e2507b8af45daafd3ea09c35862ad8c1adee61ae34995148c73eb85749d68a" - ] -} \ No newline at end of file diff --git a/opam/opam-coq-archive/released/packages/coq-unicoq/coq-unicoq.1.6+8.18/opam b/opam/opam-coq-archive/released/packages/coq-unicoq/coq-unicoq.1.6+8.18/opam deleted file mode 100644 index 9cd2333337..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-unicoq/coq-unicoq.1.6+8.18/opam +++ /dev/null @@ -1,27 +0,0 @@ -opam-version: "2.0" -maintainer: "matthieu.sozeau@inria.fr" -authors: [ "Matthieu Sozeau " "Beta Ziliani " ] -dev-repo: "git+https://github.com/unicoq/unicoq.git" -homepage: "https://github.com/unicoq/unicoq" -bug-reports: "https://github.com/unicoq/unicoq/issues" -license: "MIT" -build: [ - ["coq_makefile" "-f" "_CoqProject" "-o" "Makefile"] - [make "-j%{jobs}%"] -] -install: [ - [make "install"] -] -depends: [ - "ocaml" - "coq" {>= "8.17" & < "8.19~"} -] -synopsis: "An enhanced unification algorithm for Coq" -tags: [ - "logpath:Unicoq" - "date:2023-03-28" -] -url { - src: "https://github.com/unicoq/unicoq/archive/v1.6-8.18.tar.gz" - checksum: "sha512=29b5a7f54b50d0c6de5b08ce865ce65e10d648fbab910728f970e8b88e24319dfd541c51de080b5f416f0220c1d27729787b1960cbfb7b17b48a906f52d709f8" -} diff --git a/opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20231010/opam b/opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20231010/opam deleted file mode 100644 index e921019019..0000000000 --- a/opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20231010/opam +++ /dev/null @@ -1,18 +0,0 @@ -opam-version: "2.0" -maintainer: "The UniMath Development Team" -homepage: "https://github.com/UniMath/UniMath" -dev-repo: "git+https://github.com/UniMath/UniMath.git" -bug-reports: "https://github.com/UniMath/UniMath/issues" -license: "Similar to MIT license" -authors: ["The UniMath Development Team"] -build: [make "BUILD_COQ=no" "-j%{jobs}%"] -install: [make "BUILD_COQ=no" "install"] -depends: [ - "ocaml" - "coq" {>= "8.16.1"} -] -synopsis: "Library of Univalent Mathematics" -url { - src: "https://github.com/UniMath/UniMath/archive/refs/tags/v20231010.tar.gz" - checksum: "sha512=27729e1e6cba0df2e07d4789fd2cefcdba71e2374afb16bdaabee4132d1ab8721096602aa83e2aa599b994e1a744b969f0d5134677fbaecb3241c916d32353ac" -}