extra-dev: dev recipes for 13 packages whose release cap is stale

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

@@ -0,0 +1,42 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "anton.a.trunov@gmail.com"
+
+homepage: "https://github.com/coq-community/bits"
+dev-repo: "git+https://github.com/coq-community/bits.git"
+bug-reports: "https://github.com/coq-community/bits/issues"
+license: "Apache-2.0"
+
+synopsis: "Coq bit vector library"
+description: """
+A formalization of bitset operations in Coq with a corresponding
+axiomatization and extraction to OCaml native integers."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "ocamlbuild" 
+  "coq-mathcomp-algebra" {= "dev"}
+  "coq-mathcomp-algebra-tactics"
+]
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "keyword:bit arithmetic"
+  "keyword:bitset"
+  "keyword:bit vector"
+  "keyword:extraction"
+  "logpath:Bits"
+]
+authors: [
+  "Andrew Kennedy <akenn@microsoft.com>"
+  "Arthur Blot <arthur.blot@ens-lyon.fr>"
+  "Pierre-Évariste Dagand <pierre-evariste.dagand@lip6.fr>"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/bits.git#master"
+}

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

@@ -0,0 +1,33 @@
+opam-version: "2.0"
+maintainer: "johnw@newartisans.com"
+
+homepage: "https://github.com/jwiegley/coq-cds4ltl"
+dev-repo: "git+https://github.com/jwiegley/coq-cds4ltl.git"
+bug-reports: "https://github.com/jwiegley/coq-cds4ltl/issues"
+license: "BSD-3-Clause"
+
+synopsis: "A Calculational Deductive System for Linear Temporal Logic"
+description: """
+An axiomatic and denotational formalization of the theorems described by the
+paper: A Calculational Deductive System for Linear Temporal Logic (CDS4LTL).
+"""
+
+build: [make "-j%{jobs}%" ]
+install: [make "install"]
+depends: [
+  "rocq-core" {= "dev"}
+  "rocq-stdlib" {= "dev"}
+]
+
+tags: [
+  "keyword: temporal logic"
+  "category: Mathematics/Logic/Modal logic"
+  "logpath: CDS4LTL"
+]
+authors: [
+  "John Wiegley"
+]
+
+url {
+  src: "git+https://github.com/jwiegley/coq-cds4ltl.git#master"
+}

extra-dev/packages/coq-comp-dec-modal/coq-comp-dec-modal.dev/opam

@@ -0,0 +1,55 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "christian.doczkal@inria.fr"
+
+homepage: "https://github.com/coq-community/comp-dec-modal"
+dev-repo: "git+https://github.com/coq-community/comp-dec-modal.git"
+bug-reports: "https://github.com/coq-community/comp-dec-modal/issues"
+doc: "https://coq-community.github.io/comp-dec-modal/"
+license: "CECILL-B"
+
+synopsis: "Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse"
+description: """
+This project presents machine-checked constructive proofs of
+soundness, completeness, decidability, and the small-model property
+for the logics K, K*, CTL, and PDL (with and without converse).
+
+For all considered logics, we prove soundness and completeness of
+their respective Hilbert-style axiomatization. For K, K*, and CTL,
+we also prove soundness and completeness for Gentzen systems (i.e.,
+sequent calculi).
+
+For each logic, the central construction is a pruning-based
+algorithm computing for a given formula either a satisfying model of
+bounded size or a proof of its negation. The completeness and
+decidability results then follow with soundness from the existence
+of said algorithm.
+  """
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-hierarchy-builder" {>= "1.6.0"}
+]
+
+tags: [
+  "category:Mathematics/Logic/Modal logic"
+  "keyword:modal logic"
+  "keyword:completeness"
+  "keyword:decidability"
+  "keyword:Hilbert system"
+  "keyword:computation tree logic"
+  "keyword:propositional dynamic logic"
+  "logpath:CompDecModal"
+]
+authors: [
+  "Christian Doczkal"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/comp-dec-modal.git#master"
+}

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

@@ -0,0 +1,41 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/coq-community/coqtail-math"
+dev-repo: "git+https://github.com/coq-community/coqtail-math.git"
+bug-reports: "https://github.com/coq-community/coqtail-math/issues"
+license: "LGPL-3.0-only"
+
+synopsis: "Library of mathematical theorems and tools proved inside the Coq"
+description: """
+Coqtail is a library of mathematical theorems and tools proved inside
+the Coq proof assistant. Results range mostly from arithmetic to real
+and complex analysis."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+]
+
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword:real analysis"
+  "keyword:complex analysis"
+  "logpath:Coqtail"
+]
+authors: [
+  "Guillaume Allais"
+  "Sylvain Dailler"
+  "Hugo Férée"
+  "Jean-Marie Madiot"
+  "Pierre-Marie Pédrot"
+  "Amaury Pouly"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/coqtail-math.git#master"
+}

extra-dev/packages/coq-exact-real-arithmetic/coq-exact-real-arithmetic.dev/opam

@@ -0,0 +1,30 @@
+opam-version: "2.0"
+maintainer: "Hugo.Herbelin@inria.fr"
+homepage: "https://github.com/rocq-community/exact-real-arithmetic"
+license: "LGPL 2.1"
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "ocaml"
+  "coq" {= "dev"}
+]
+tags: [
+  "keyword: correctness"
+  "keyword: real numbers"
+  "keyword: arithmetic"
+  "category: Mathematics/Real Numbers"
+]
+authors: [
+  "Jérôme Creci"
+]
+bug-reports: "https://github.com/rocq-community/exact-real-arithmetic/issues"
+dev-repo: "git+https://github.com/rocq-community/exact-real-arithmetic.git"
+synopsis: "Exact Real Arithmetic"
+description: """
+This contribution contains a proof of correctness
+of some exact real arithmetic algorithms from the PhD thesis of
+Valérie Ménissier-Morain"""
+
+url {
+  src: "git+https://github.com/rocq-community/exact-real-arithmetic.git#master"
+}

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

@@ -0,0 +1,59 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "thery@sophia.inria.fr"
+
+homepage: "https://github.com/thery/hanoi"
+dev-repo: "git+https://github.com/thery/hanoi.git"
+bug-reports: "https://github.com/thery/hanoi/issues"
+license: "MIT"
+
+synopsis: "Hanoi tower in Rocq"
+description: """
+Hanoi tower in Rocq
+
+
+| File                              |  Content                                 | 
+| --------------------------------- | -----------------------------------------| 
+| [extra](./extra.v)                | Extra theorems from the standard library |
+| [gdist](./gdist.v)                | Distance in a graph                      |
+| [ghanoi](./ghanoi.v)              | General Hanoi framework                  |
+| [ghanoi3](./ghanoi3.v)            | General Hanoi framework with 3 pegs      |
+| [lhanoi3](./lhanoi3.v)            | Linear Hanoi tower with 3 pegs           |
+| [rhanoi3](./rhanoi3.v)            | Regular Hanoi tower with 3 pegs          |
+| [triangular](./triangular.v)      | Theorems about triangular numbers        |
+| [phi](./phi.v)                    | Theorems about the Φ function            |
+| [psi](./psi.v)                    | Theorems about the Ψ function            |
+| [ghanoi4](./ghanoi4.v)            | General Hanoi framework with 4 pegs      |
+| [rhanoi4](./rhanoi4.v)            | Regular Hanoi tower with 4 pegs          |
+| [star](./star.v)                  | Some maths for the shanoi                |
+| [shanoi](./shanoi.v)              | Hanoi tower in star                      |
+| [shanoi4](./shanoi4.v)            | Hanoi tower with 4 pegs in star          |
+
+A note about this development is available 
+[here](https://hal.inria.fr/hal-02903548).
+
+An interactive version of the library is available 
+[here](https://thery.github.io/hanoi/index.html)."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "rocq-mathcomp-ssreflect" {(>= "2.5.0")}
+  "rocq-mathcomp-algebra" {(>= "2.5.0")}
+  "coq-mathcomp-finmap" {(>= "2.2.2")}
+]
+
+tags: [
+  "keyword:hanoi tower"
+  "logpath:hanoi"
+]
+authors: [
+  "Laurent Théry"
+]
+
+url {
+  src: "git+https://github.com/thery/hanoi.git#master"
+}

extra-dev/packages/coq-mathcomp-abel/coq-mathcomp-abel.dev/opam

@@ -0,0 +1,48 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
+
+homepage: "https://github.com/math-comp/abel"
+dev-repo: "git+https://github.com/math-comp/abel.git"
+bug-reports: "https://github.com/math-comp/abel/issues"
+license: "CECILL-B"
+
+synopsis: "Abel - Ruffini's theorem"
+description: """
+This repository contains a proof of Abel - Galois Theorem
+(equivalence between being solvable by radicals and having a
+solvable Galois group) and Abel - Ruffini Theorem (unsolvability of
+quintic equations) in the Coq proof-assistant and using the
+Mathematical Components library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "rocq-core" {= "dev"}
+  "coq-mathcomp-ssreflect" {= "dev"}
+  "coq-mathcomp-fingroup" 
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-solvable" 
+  "coq-mathcomp-field" 
+  "coq-mathcomp-real-closed" {= "dev"}
+]
+
+tags: [
+  "keyword:algebra"
+  "keyword:Galois"
+  "keyword:Abel Ruffini"
+  "keyword:unsolvability of quintincs"
+  "logpath:Abel"
+]
+authors: [
+  "Sophie Bernard"
+  "Cyril Cohen"
+  "Assia Mahboubi"
+  "Pierre-Yves Strub"
+]
+
+url {
+  src: "git+https://github.com/math-comp/abel.git#master"
+}

extra-dev/packages/coq-mathcomp-apery/coq-mathcomp-apery.dev/opam

@@ -0,0 +1,51 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "assia.mahboubi@inria.fr"
+
+homepage: "https://github.com/coq-community/apery"
+dev-repo: "git+https://github.com/coq-community/apery.git"
+bug-reports: "https://github.com/coq-community/apery/issues"
+license: "CECILL-C"
+
+synopsis: "A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational"
+description: """
+This project contains a formal proof that the real number ζ(3),
+also known as Apéry's constant, is irrational. It follows roughly
+Apéry's original sketch of a proof. However, the recurrence
+relations constituting the crux of the proof have been guessed by a
+computer algebra program (in this case in Maple/Algolib). These
+relations are formally checked a posteriori, so that Coq's kernel
+remains the sole trusted code base."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {= "dev"}
+  "coq-mathcomp-ssreflect" {= "dev"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-field" 
+  "coq-coqeal" {>= "2.1.0"}
+  "coq-mathcomp-real-closed" {= "dev"}
+  "coq-mathcomp-bigenough" {= "dev"}
+  "coq-mathcomp-zify" 
+  "coq-mathcomp-algebra-tactics" 
+]
+
+tags: [
+  "category:Mathematics/Arithmetic and Number Theory/Number theory"
+  "keyword:apery recurrence"
+  "keyword:irrationality"
+  "keyword:creative telescoping"
+  "logpath:mathcomp.apery"
+]
+authors: [
+  "Frédéric Chyzak"
+  "Assia Mahboubi"
+  "Thomas Sibut-Pinote"
+]
+
+url {
+  src: "git+https://github.com/rocq-community/apery.git#master"
+}