Add dev packages for Coq Platform packages which don't have one as yet

extra-dev/packages/coq-coqprime-generator/coq-coqprime-generator.dev/opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://github.com/thery/coqprime"
+bug-reports: "https://github.com/thery/coqprime/issues"
+dev-repo: "git+https://github.com/thery/coqprime.git"
+license: "LGPL-2.1-only"
+authors: ["Laurent Théry"]
+build: [
+  # cd to a subfolder in opam is tricky, so just move gencertif to the root folder
+  [ "find" "gencertif" "-type" "f" "-exec" "mv" "{}" "." ";" ]
+  [ "autoreconf" "-i" "-s" ]
+  [ "./configure" "--prefix" prefix
+    # Optiosn for finding opam local gmp-ecm
+    "CPPFLAGS=-I%{prefix}%/include"
+    "LDFLAGS=-L%{lib}%"
+    # Options for homebrew on Intel silicon (overwriting the above)
+    "CPPFLAGS=-I%{prefix}%/include -I/opt/local/include" { os-distribution = "macports" & os = "macos" }
+    "LDFLAGS=-L%{lib}% -L/opt/local/lib" { os-distribution = "macports" & os = "macos" }
+    # Options for homebrew on Apple silicon (overwriting the above)
+    "CPPFLAGS=-I%{prefix}%/include -I/opt/homebrew/include" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
+    "LDFLAGS=-L%{lib}% -L/opt/homebrew/lib" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
+    # Options for Windows cygwin
+    "--build=%{arch}%-pc-cygwin" { os = "win32" & os-distribution = "cygwinports" }
+    "--host=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
+    "--target=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
+  ]
+  [ make "-j" "%{jobs}%" ]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "ocaml"
+  "num"
+  "conf-gmp"
+  "gmp-ecm"
+]
+synopsis: "Certificate generator for prime numbers in Coq"
+url {
+  src: "git+https://github.com/thery/coqprime#master"
+}

extra-dev/packages/coq-dpdgraph/coq-dpdgraph.dev/opam

@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+
+homepage: "https://github.com/coq-community/coq-dpdgraph"
+dev-repo: "git+https://github.com/coq-community/coq-dpdgraph.git"
+bug-reports: "https://github.com/coq-community/coq-dpdgraph/issues"
+license: "LGPL-2.1-only"
+
+synopsis: "Compute dependencies between Coq objects (definitions, theorems) and produce graphs"
+description: """
+Coq plugin that extracts the dependencies between Coq objects,
+and produces files with dependency information. Includes tools
+to visualize dependency graphs and find unused definitions."""
+
+build: [
+  ["autoconf"] {dev}
+  ["./configure"]
+  [make "-j%{jobs}%" "WARN_ERR="]
+]
+run-test: [make "test-suite"]
+install: [make "install" "BINDIR=%{bin}%"]
+depends: [
+  "ocaml" {>= "4.05.0"}
+  "coq" {= "dev"}
+  "conf-autoconf" {build & dev}
+  "ocamlgraph" 
+]
+
+tags: [
+  "category:Miscellaneous/Coq Extensions"
+  "keyword:dependency graph"
+  "keyword:dependency analysis"
+  "logpath:dpdgraph"
+]
+authors: [
+  "Anne Pacalet"
+  "Yves Bertot"
+  "Olivier Pons"
+]
+
+url {
+  src: "git+https://github.com/coq-community/coq-dpdgraph#coq-master"
+}

extra-dev/packages/coq-gappa/coq-gappa.dev/opam

@@ -0,0 +1,32 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://gappa.gitlabpages.inria.fr/"
+dev-repo: "git+https://gitlab.inria.fr/gappa/coq.git"
+bug-reports: "https://gitlab.inria.fr/gappa/coq/issues"
+license: "LGPL-3.0-or-later"
+build: [
+  ["autoconf"] {dev}
+  ["./configure"]
+  ["./remake" "-j%{jobs}%"]
+]
+install: ["./remake" "install"]
+depends: [
+  "ocaml"
+  "ocamlfind" {build}
+  "coq" {>= "8.8.1"}
+  "coq-flocq" {>= "3.0"}
+  "conf-autoconf" {build & dev}
+  ("conf-g++" {build} | "conf-clang" {build})
+]
+tags: [
+  "keyword:floating-point arithmetic"
+  "keyword:interval arithmetic"
+  "keyword:decision procedure"
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "logpath:Gappa"
+]
+authors: [ "Guillaume Melquiond <[email protected]>" ]
+synopsis: "A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover"
+url {
+  src: "git+https://gitlab.inria.fr/gappa/coq.git/#master"
+}

extra-dev/packages/coq-interval/coq-interval.dev/opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+homepage: "https://coqinterval.gitlabpages.inria.fr/"
+dev-repo: "git+https://gitlab.inria.fr/coqinterval/interval.git"
+bug-reports: "https://gitlab.inria.fr/coqinterval/interval/issues"
+license: "CeCILL-C"
+build: [
+  ["autoconf"] {dev}
+  ["./configure"]
+  ["./remake" "-j%{jobs}%"]
+]
+install: ["./remake" "install"]
+depends: [
+  "coq" {>= "8.8"}
+  "coq-bignums"
+  "coq-flocq" {>= "3.1"}
+  "coq-mathcomp-ssreflect" {>= "1.6"}
+  "coq-coquelicot" {>= "3.0"}
+  "conf-autoconf" {build & dev}
+  ("conf-g++" {build} | "conf-clang" {build})
+]
+tags: [
+  "keyword:interval arithmetic"
+  "keyword:decision procedure"
+  "keyword:floating-point arithmetic"
+  "keyword:reflexive tactic"
+  "keyword:Taylor models"
+  "category:Mathematics/Real Calculus and Topology"
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "logpath:Interval"
+]
+authors: [
+  "Guillaume Melquiond <[email protected]>"
+  "Érik Martin-Dorel <[email protected]>"
+  "Pierre Roux <[email protected]>"
+  "Thomas Sibut-Pinote <[email protected]>"
+]
+synopsis: "A Coq tactic for proving bounds on real-valued expressions automatically"
+url {
+  src: "git+https://gitlab.inria.fr//coqinterval/interval.git/#master"
+}

extra-dev/packages/coq-iris-heap-lang/coq-iris-heap-lang.dev/opam

@@ -0,0 +1,27 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <[email protected]>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+
+synopsis: "The canonical example language for Iris"
+description: """
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
+"""
+tags: [
+  "logpath:iris.heap_lang"
+]
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_heap_lang" "-j%{jobs}%"]
+install: ["./make-package" "iris_heap_lang" "install"]
+
+url {
+  src: "git+https://gitlab.mpi-sws.org/iris/iris#master"
+}

extra-dev/packages/coq-iris/coq-iris.dev/opam

@@ -0,0 +1,38 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <[email protected]>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+
+synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+description: """
+Iris is a framework for reasoning about the safety of concurrent programs using
+concurrent separation logic. It can be used to develop a program logic, for
+defining logical relations, and for reasoning about type systems, among other
+applications. This package includes the base logic, Iris Proof Mode (IPM) /
+MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
+for an instantiation of the program logic to a particular programming language.
+"""
+tags: [
+  "logpath:iris.prelude"
+  "logpath:iris.algebra"
+  "logpath:iris.si_logic"
+  "logpath:iris.bi"
+  "logpath:iris.proofmode"
+  "logpath:iris.base_logic"
+  "logpath:iris.program_logic"
+]
+
+depends: [
+  "coq" {>= "8.13"}
+  "coq-stdpp" {>= "1.7.0"}
+]
+
+build: ["./make-package" "iris" "-j%{jobs}%"]
+install: ["./make-package" "iris" "install"]
+
+url {
+  src: "git+https://gitlab.mpi-sws.org/iris/iris#master"
+}

extra-dev/packages/coq-libhyps/coq-libhyps.dev/opam

@@ -0,0 +1,47 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+synopsis: "Hypotheses manipulation library"
+
+homepage: "https://github.com/Matafou/LibHyps"
+dev-repo: "git+https://github.com/Matafou/LibHyps.git"
+bug-reports: "https://github.com/Matafou/LibHyps/issues"
+doc: "https://github.com/Matafou/LibHyps/blob/master/Demo/demo.v"
+license: "MIT"
+
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+
+install: [make "install"]
+
+depends: [
+  "coq" {>= "8.11"}
+]
+
+tags: [
+  "keyword:proof environment manipulation"
+  "keyword:forward reasoning"
+  "keyword:hypothesis naming"
+  "category:Miscellaneous/Coq Tactics Library"
+  "logpath:LibHyps"
+]
+
+authors: [
+ "Pierre Courtieu"
+]
+
+description: "
+This library defines a set of tactics to manipulate hypothesis
+individually or by group. In particular it allows applying a tactic on
+each hypothesis of a goal, or only on *new* hypothesis after some
+tactic. Examples of manipulations: automatic renaming, subst, revert,
+or any tactic expecting a hypothesis name as argument.
+
+It also provides the especialize tactic to ease forward reasoning by
+instantianting one, several or all premisses of a hypothesis.
+"
+
+url {
+    src: "git+https://github.com/Matafou/LibHyps#master"
+}

extra-dev/packages/coq-stdpp/coq-stdpp.dev/opam

@@ -0,0 +1,43 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <[email protected]>"
+authors: "The std++ team"
+license: "BSD-3-Clause"
+homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
+bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
+
+synopsis: "An extended \"Standard Library\" for Coq"
+description: """
+The key features of this library are as follows:
+
+- It provides a great number of definitions and lemmas for common data
+  structures such as lists, finite maps, finite sets, and finite multisets.
+- It uses type classes for common notations (like `∅`, `∪`, and Haskell-style
+  monad notations) so that these can be overloaded for different data structures.
+- It uses type classes to keep track of common properties of types, like it
+  having decidable equality or being countable or finite.
+- Most data structures are represented in canonical ways so that Leibniz
+  equality can be used as much as possible (for example, for maps we have
+  `m1 = m2` iff `∀ i, m1 !! i = m2 !! i`). On top of that, the library provides
+  setoid instances for most types and operations.
+- It provides various tactics for common tasks, like an ssreflect inspired
+  `done` tactic for finishing trivial goals, a simple breadth-first solver
+  `naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
+  for proving compatibility of functions with respect to relations, and a solver
+  `set_solver` for goals involving set operations.
+- It is entirely dependency- and axiom-free.
+"""
+tags: [
+  "logpath:stdpp"
+]
+
+depends: [
+  "coq" {>= "8.11"}
+]
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+
+url {
+  src: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
+}