extra-dev: add 32 dev recipes and update 11 more, for packages that install successfully

extra-dev/packages/coq-aac-tactics/coq-aac-tactics.dev/opam

@@ -1,43 +1,16 @@
 opam-version: "2.0"
 maintainer: "palmskog@gmail.com"
 
-homepage: "https://github.com/coq-community/aac-tactics"
-dev-repo: "git+https://github.com/coq-community/aac-tactics.git"
-bug-reports: "https://github.com/coq-community/aac-tactics/issues"
+homepage: "https://github.com/rocq-community/aac-tactics"
+dev-repo: "git+https://github.com/rocq-community/aac-tactics.git"
+bug-reports: "https://github.com/rocq-community/aac-tactics/issues"
 license: "LGPL-3.0-or-later"
 
-synopsis: "Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators"
-description: """
-This Coq plugin provides tactics for rewriting and proving universally
-quantified equations modulo associativity and commutativity of some operator,
-with idempotent commutative operators enabling additional simplifications.
-The tactics can be applied for custom operators by registering the operators and
-their properties as type class instances. Instances for many commonly used operators,
-such as for binary integer arithmetic and booleans, are provided with the plugin."""
-
-build: [make "-j%{jobs}%"]
-install: [make "install"]
-depends: [
-  "ocaml" {>= "4.09.0"}
-  "coq" {= "dev"}
-]
-
-tags: [
-  "category:Miscellaneous/Coq Extensions"
-  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
-  "keyword:reflexive tactic"
-  "keyword:rewriting"
-  "keyword:rewriting modulo associativity and commutativity"
-  "keyword:rewriting modulo ac"
-  "keyword:decision procedure"
-  "logpath:AAC_tactics"
-]
+depends: [ "rocq-aac-tactics" { = version } ]
 authors: [
   "Thomas Braibant"
   "Damien Pous"
   "Fabian Kunze"
 ]
 
-url {
-  src: "git+https://github.com/coq-community/aac-tactics.git#master"
-}
+synopsis: "Compatibility package for rocq-aac-tactics"

extra-dev/packages/coq-bedrock2-compiler/coq-bedrock2-compiler.dev/opam

@@ -0,0 +1,38 @@
+opam-version: "2.0"
+authors: [
+  "Massachusetts Institute of Technology"
+  "Kevix"
+  "SiFive"
+]
+maintainer: "Jason Gross <jgross@mit.edu>"
+homepage: "https://github.com/mit-plv/bedrock2"
+bug-reports: "https://github.com/mit-plv/bedrock2/issues"
+license: "MIT"
+build: [
+  # No reason to build compiler_ex since there's no install_compiler_ex target; the install_compiler target installs only compiler_noex
+  [make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "compiler_noex"]
+]
+install: [make "EXTERNAL_DEPENDENCIES=1" "install_compiler"]
+depends: [
+  "conf-findutils" {build}
+  "coq" {= "dev"}
+  "coq-bedrock2" {= version}
+  "coq-riscv" {= "0.0.6"}
+  "zarith" {>= "1.11"}
+]
+dev-repo: "git+https://github.com/mit-plv/bedrock2.git"
+synopsis: "A work-in-progress language and compiler for verified low-level programming (compiler part)"
+description: """
+bedrock2 is a low-level systems programming language. This language is
+equipped with a simple program logic for proving correctness of the
+programs.  This package includes a verified compiler targeting RISC-V
+from this language.
+
+The project has similar goals as bedrock, but uses a different design.
+No code is shared between bedrock and bedrock2.
+"""
+tags: ["logpath:bedrock2"]
+
+url {
+  src: "git+https://github.com/mit-plv/bedrock2.git#master"
+}

extra-dev/packages/coq-graph-theory-planar/coq-graph-theory-planar.dev/opam

@@ -0,0 +1,38 @@
+opam-version: "2.0"
+maintainer: "christian.doczkal@mpi-sp.org"
+
+homepage: "https://github.com/coq-community/graph-theory"
+dev-repo: "git+https://github.com/coq-community/graph-theory.git"
+bug-reports: "https://github.com/coq-community/graph-theory/issues"
+license: "CECILL-B"
+
+synopsis: "Graph theory results on planarity in Coq and MathComp"
+description: """
+Formal definitions and results on graph planarity in Coq using the Mathematical Components
+library, including Wagner's Theorem. Relies on hypermaps and other notions developed
+as part of the Coq proof of the Four-Color Theorem."""
+
+build: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+  "dune" {>= "3.5"}
+  "coq" {= "dev"}
+  "coq-mathcomp-ssreflect" {>= "2.5.0"}
+  ("coq-mathcomp-algebra" {>= "2.6.0"} | "coq-mathcomp-algebra-tactics")
+  "coq-graph-theory" {= version}
+  "coq-fourcolor"
+]
+
+tags: [
+  "category:Computer Science/Graph Theory"
+  "keyword:graph theory"
+  "keyword:planarity"
+  "logpath:GraphTheory.planar"
+]
+authors: [
+  "Christian Doczkal"
+  "Damien Pous"
+]
+
+url {
+  src: "git+https://github.com/coq-community/graph-theory.git#master"
+}

extra-dev/packages/coq-graph-theory/coq-graph-theory.dev/opam

@@ -0,0 +1,40 @@
+opam-version: "2.0"
+maintainer: "christian.doczkal@mpi-sp.org"
+
+homepage: "https://github.com/coq-community/graph-theory"
+dev-repo: "git+https://github.com/coq-community/graph-theory.git"
+bug-reports: "https://github.com/coq-community/graph-theory/issues"
+license: "CECILL-B"
+
+synopsis: "General graph theory definitions and results in Coq and MathComp"
+description: """
+Formalized general graph theory definitions and results using Coq and
+the Mathematical Components library, including various standard results
+from the literature (e.g., Menger's Theorem and Hall's Marriage Theorem)."""
+
+build: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+  "dune" {>= "3.5"}
+  "coq" {= "dev"}
+  "coq-mathcomp-ssreflect" {>= "2.5.0"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-finmap" 
+  "coq-hierarchy-builder" {>= "1.5.0"}
+]
+
+tags: [
+  "category:Computer Science/Graph Theory"
+  "keyword:graph theory"
+  "keyword:minors"
+  "keyword:treewidth"
+  "keyword:algebra"
+  "logpath:GraphTheory.core"
+]
+authors: [
+  "Christian Doczkal"
+  "Damien Pous"
+]
+
+url {
+  src: "git+https://github.com/coq-community/graph-theory.git#master"
+}

extra-dev/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.dev/opam

@@ -0,0 +1,31 @@
+opam-version: "2.0"
+synopsis: "HOL-Light definition of real numbers using N"
+description: """
+This library contains an automatic translation of the HOL-Light
+definition of real numbers using https://github.com/Deducteam/hol2dk
+with the HOL-Light type of natural numbers mapped to the Rocq type N.
+"""
+homepage: "https://github.com/Deducteam/coq-hol-light-real-with-N"
+dev-repo: "git+https://github.com/Deducteam/coq-hol-light-real-with-N.git"
+bug-reports: "https://github.com/Deducteam/coq-hol-light-real-with-N/issues"
+doc: "https://github.com/Deducteam/coq-hol-light-real-with-N"
+maintainer: "frederic.blanqui@inria.fr"
+authors: ["https://github.com/Deducteam/coq-hol-light-real-with-N/blob/main/AUTHORS.md"]
+license: "CeCILL-2.1"
+depends: [
+  "rocq-core" {= "dev"}
+  "rocq-stdlib" {= "dev"}
+]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+tags: [
+  "logpath:HOLLight_Real_With_N"
+  "date:2025-07-11"
+  "category:Mathematics/Arithmetic and Number Theory/Miscellaneous"
+  "category:Mathematics/Real Numbers"
+  "keyword:HOL-Light"
+]
+
+url {
+  src: "git+https://github.com/Deducteam/coq-hol-light-real-with-N.git#main"
+}

extra-dev/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.dev/opam

@@ -0,0 +1,31 @@
+opam-version: "2.0"
+synopsis: "HOL-Light definition of real numbers using nat"
+description: """
+This library contains an automatic translation of the HOL-Light
+definition of real numbers using https://github.com/Deducteam/hol2dk
+with the HOL-Light type of natural numbers mapped to the Rocq type nat.
+"""
+homepage: "https://github.com/Deducteam/coq-hol-light-real-with-nat"
+dev-repo: "git+https://github.com/Deducteam/coq-hol-light-real-with-nat.git"
+bug-reports: "https://github.com/Deducteam/coq-hol-light-real-with-nat/issues"
+doc: "https://github.com/Deducteam/coq-hol-light-real-with-nat"
+maintainer: "frederic.blanqui@inria.fr"
+authors: ["https://github.com/Deducteam/coq-hol-light-real-with-nat/blob/main/AUTHORS.md"]
+license: "CeCILL-2.1"
+depends: [
+  "rocq-core" {= "dev"}
+  "rocq-stdlib" {= "dev"}
+]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+tags: [
+  "keyword:HOL-Light"
+  "category:Math/Arith/Misc"
+  "category:Math/Arith/Real numbers"
+  "date:2025-01-18"
+  "logpath:HOLLight_Real_With_nat"
+]
+
+url {
+  src: "git+https://github.com/Deducteam/coq-hol-light-real-with-nat.git#main"
+}

extra-dev/packages/coq-kruskal-almostfull/coq-kruskal-almostfull.dev/opam

@@ -0,0 +1,28 @@
+opam-version: "2.0"
+synopsis: "Base Coq library for manipulating Almost Full relations"
+description: """
+   This library formalizes ground results about Almost Full relations (AF) in Coq 8.14+, up to Dickson's lemma.
+"""  
+maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] 
+authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)"
+license: "MPL-2.0"
+homepage: "https://github.com/DmxLarchey/Kruskal-AlmostFull/"
+bug-reports: "https://github.com/DmxLarchey/Kruskal-AlmostFull/issues"
+dev-repo: "git+https://github.com:DmxLarchey/Kruskal-AlmostFull/"
+
+build: [
+  [make "-j%{jobs}%" "type"]
+]
+install: [
+  [make "install"]
+]
+
+depends: [
+  "coq" {= "dev"}
+  "coq-kruskal-trees" {>= "1.5"}
+  "coq-kruskal-finite" {>= "1.5"}
+]
+
+url {
+  src: "git+https://github.com/DmxLarchey/Kruskal-AlmostFull.git#main"
+}

extra-dev/packages/coq-kruskal-fan/coq-kruskal-fan.dev/opam

@@ -0,0 +1,30 @@
+opam-version: "2.0"
+synopsis: "Extending Coq library for manipulating Almost Full relations with the FAN theorem"
+description: """
+   This library formalizes additional tools for AF relations, the FAN theorem for inductive bars
+   and a constructive variant of König's lemma.
+"""  
+maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] 
+authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)"
+license: "MPL-2.0"
+homepage: "https://github.com/DmxLarchey/Kruskal-Higman/"
+bug-reports: "https://github.com/DmxLarchey/Kruskal-Higman/issues"
+dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Higman/"
+
+build: [
+  [make "-j%{jobs}%" "type"]
+]
+install: [
+  [make "install"]
+]
+
+depends: [
+  "coq" {= "dev"}
+  "coq-kruskal-trees" {}
+  "coq-kruskal-finite" {}
+  "coq-kruskal-almostfull" {>= "1.2"}
+]
+
+url {
+  src: "git+https://github.com/DmxLarchey/Kruskal-Fan.git#main"
+}

extra-dev/packages/coq-kruskal-finite/coq-kruskal-finite.dev/opam

@@ -0,0 +1,30 @@
+opam-version: "2.0"
+synopsis: "Coq library for manipulating finiteness, finite choice and decision as used in proof of Kruskal's tree theorem"
+description: """
+   Tools to facilitate proofs of finiteness (ie listability), finite choice principles 
+   and finite decidability.
+"""  
+maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] 
+authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)"
+license: "MPL-2.0"
+homepage: "https://github.com/DmxLarchey/Kruskal-Finite/"
+bug-reports: "https://github.com/DmxLarchey/Kruskal-Finite/issues"
+dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Finite/"
+
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+
+depends: [
+  "coq" {= "dev"}
+  "coq-kruskal-trees" {>= "1.3"} 
+]
+
+#url { git: "https://github.com/DmxLarchey/Kruskal-Finite.git" }
+
+url {
+  src: "git+https://github.com/DmxLarchey/Kruskal-Finite.git#main"
+}

extra-dev/packages/coq-kruskal-higman/coq-kruskal-higman.dev/opam

@@ -0,0 +1,30 @@
+opam-version: "2.0"
+synopsis: "Extending Coq library for manipulating Almost Full relations with Higman's lemma"
+description: """
+   This library formalizes additional tools for AF relations, eg quasi morphisms applied to Higman's lemma.
+"""  
+maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] 
+authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)"
+license: "MPL-2.0"
+homepage: "https://github.com/DmxLarchey/Kruskal-Higman/"
+bug-reports: "https://github.com/DmxLarchey/Kruskal-Higman/issues"
+dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Higman/"
+
+build: [
+  [make "-j%{jobs}%" "type"]
+]
+install: [
+  [make "install"]
+]
+
+depends: [
+  "coq" {= "dev"}
+  "coq-kruskal-trees" {}
+  "coq-kruskal-finite" {}
+  "coq-kruskal-almostfull" {}
+  "coq-kruskal-fan" {}
+]
+
+url {
+  src: "git+https://github.com/DmxLarchey/Kruskal-Higman.git#main"
+}

extra-dev/packages/coq-kruskal-theorems/coq-kruskal-theorems.dev/opam

@@ -0,0 +1,31 @@
+opam-version: "2.0"
+synopsis: "Extending the Coq library for manipulating Almost Full relations with various forms of Kruskal's tree theorem"
+description: """
+   This library formalizes the high-level variants of Higman's theorem (for trees of bounded arity)
+   and Kruskal's theorem (for rose trees), depending on how these datatypes are implemented. Also,
+   Vazsonyi's conjecture to illustrate the expressive power of Kruskal's and Higman's theorem.
+"""  
+maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] 
+authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)"
+license: "MPL-2.0"
+homepage: "https://github.com/DmxLarchey/Kruskal-Theorems/"
+bug-reports: "https://github.com/DmxLarchey/Kruskal-Theorems/issues"
+dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Theorems/"
+
+build: [
+  [make "-j%{jobs}%" "type"]
+]
+install: [
+  [make "install"]
+]
+
+depends: [
+  "coq" {= "dev"}
+  "coq-kruskal-almostfull"
+  "coq-kruskal-higman" {>= "1.2"}
+  "coq-kruskal-veldman" {>= "1.2"}
+]
+
+url {
+  src: "git+https://github.com/DmxLarchey/Kruskal-Theorems.git#main"
+}