rocq-prover · JasonGross · Aug 6, 2026 · Aug 1, 2026 · Aug 6, 2026 · Aug 6, 2026
diff --git a/extra-dev/packages/coq-coinduction/coq-coinduction.dev/opam b/extra-dev/packages/coq-coinduction/coq-coinduction.dev/opam
@@ -1,35 +1,14 @@
 opam-version: "2.0"
-maintainer: "palmskog@gmail.com"
+maintainer: "damien.pous@ens-lyon.fr"
 
 homepage: "https://github.com/damien-pous/coinduction"
 dev-repo: "git+https://github.com/damien-pous/coinduction.git"
 bug-reports: "https://github.com/damien-pous/coinduction/issues"
 license: "LGPL-3.0-or-later"
 
-synopsis: "A library and plugin for doing proofs by (enhanced) coinduction"
-description: """
-Coinductive predicates are greatest fixpoints of monotone functions.
-The `companion' makes it possible to enhance the associated coinduction scheme.
-This library provides a formalisation on enhancements based on the companion, as well as tactics in making it straightforward to perform proofs by enhanced coinduction.
-"""
-
-build: [make "-j%{jobs}%"]
-install: [make "install"]
-depends: [
-  "ocaml"
-  "coq" {= "dev"}
-]
-
-tags: [
-  "keyword:coinduction"
-  "keyword:up to techniques"
-  "keyword:companion"
-  "logpath:Coinduction"
-]
+depends: [ "rocq-coinduction" { = version } ]
 authors: [
   "Damien Pous"
 ]
 
-url {
-  src: "git+https://github.com/damien-pous/coinduction.git#master"
-}
+synopsis: "Compatibility package for rocq-coinduction"
diff --git a/extra-dev/packages/coq-color/coq-color.dev/opam b/extra-dev/packages/coq-color/coq-color.dev/opam
@@ -1,5 +1,12 @@
 opam-version: "2.0"
-maintainer: "Matej Košík <matej.kosik@inria.fr>"
+maintainer: "frederic.blanqui@inria.fr"
+
+homepage: "https://github.com/fblanqui/color/"
+dev-repo: "git+https://github.com/fblanqui/color.git"
+bug-reports: "https://github.com/fblanqui/color/issues"
+license: "CeCILL-2.1"
+
+depends: [ "rocq-color" { = version } ]
 authors: [
   "Frédéric Blanqui"
   "Adam Koprowski"
@@ -16,99 +23,5 @@ authors: [
   "Lianyi Zhang"
   "Sorin Stratulat"
 ]
-license: "CeCILL"
-homepage: "http://color.inria.fr/"
-bug-reports: "color@inria.fr"
-build: [
-  [make "-j%{jobs}%"]
-]
-install: [make "-f" "rocq.mk" "install"]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/CoLoR"]
-depends: [
-  "ocaml"
-  "coq" {= "dev"}
-  "coq-bignums" {= "dev"}
-]
-tags: [
-  "date:2017-01-11"
-
-  "logpath:CoLoR"
-
-  "category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms"
-  "category:Computer Science/Data Types and Data Structures"
-  "category:Computer Science/Lambda Calculi"
-  "category:Mathematics/Algebra"
-  "category:Mathematics/Combinatorics and Graph Theory"
-  "category:Mathematics/Logic/Type theory"
-  "category:Miscellaneous/Extracted Programs/Type checking unification and normalization"
-
-  "keyword:rewriting"
-  "keyword:termination"
-  "keyword:lambda calculus"
-
-  "keyword:list"
-  "keyword:multiset"
-  "keyword:polynomial"
-  "keyword:vectors"
-  "keyword:matrices"
-  "keyword:FSet"
-  "keyword:FMap"
-
-  "keyword:term"
-  "keyword:context"
-  "keyword:substitution"
-  "keyword:universal algebra"
-
-  "keyword:varyadic term"
-  "keyword:string"
-
-  "keyword:alpha-equivalence"
-  "keyword:de Bruijn indices"
-  "keyword:simple types"
 
-  "keyword:matching"
-  "keyword:unification"
-
-  "keyword:relation"
-  "keyword:ordering"
-  "keyword:quasi-ordering"
-  "keyword:lexicographic ordering"
-
-  "keyword:ring"
-  "keyword:semiring"
-
-  "keyword:well-foundedness"
-  "keyword:noetherian"
-  "keyword:finitely branching"
-  "keyword:dependent choice"
-  "keyword:infinite sequences"
-
-  "keyword:non-termination"
-  "keyword:loop"
-
-  "keyword:graph"
-  "keyword:path"
-  "keyword:transitive closure"
-  "keyword:strongly connected components"
-  "keyword:topological ordering"
-
-  "keyword:rpo"
-  "keyword:horpo"
-  "keyword:dependency pair"
-  "keyword:dependency graph"
-  "keyword:semantic labeling"
-
-  "keyword:reducibility"
-  "keyword:Girard"
-
-  "keyword:fixpoint theorem"
-  "keyword:Tarski"
-
-  "keyword:pigeon-hole principle"
-  "keyword:Ramsey theorem"
-]
-synopsis: "A library on rewriting theory and termination"
-flags: light-uninstall
-url {
-  src: "git+https://github.com/fblanqui/color.git#master"
-}
+synopsis: "Compatibility package for rocq-color"
diff --git a/extra-dev/packages/coq-coqeal/coq-coqeal.dev/opam b/extra-dev/packages/coq-coqeal/coq-coqeal.dev/opam
@@ -17,11 +17,16 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.20" & < "9.1~") | (= "dev")}
+  "coq" {= "dev"}
   "coq-bignums"
   "coq-elpi" {>= "2.4.1" | = "dev"}
   "coq-hierarchy-builder" {>= "1.4.0"}
-  "coq-mathcomp-ssreflect" {>= "2.3"}
+  # 6 of the 52 .v files require `all_boot`, all of them under theory/, which
+  # `build: [make]` compiles. That umbrella ships from rocq-mathcomp-boot, and no
+  # mathcomp below 2.5.0 carries it -- so 2.3 was an impossible floor. The bare
+  # coq-mathcomp-algebra below does not close the hole on its own; it only reaches
+  # ssreflect through algebra's own {= version} lock, which at 2.4.0 locks downward.
+  "coq-mathcomp-ssreflect" {>= "2.5.0"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-multinomials" {>= "2.0"}
   "coq-mathcomp-real-closed" {>= "2.0"}

diff --git a/extra-dev/packages/coq-ctree/coq-ctree.dev/opam b/extra-dev/packages/coq-ctree/coq-ctree.dev/opam
@@ -0,0 +1,19 @@
+opam-version: "2.0"
+maintainer: "Yannick Zakowski"
+
+homepage: "https://github.com/vellvm/ctrees"
+dev-repo: "git+https://github.com/vellvm/ctrees.git"
+bug-reports: "https://github.com/vellvm/ctrees/issues"
+license: "MIT"
+
+depends: [ "rocq-ctree" {= version} ]
+
+authors: [
+  "Nicolas Chappe"
+  "Paul He"
+  "Ludovic Henrio"
+  "Yannick Zakowski"
+  "Steve Zdancewic"
+]
+
+synopsis: "Compatibility package for rocq-ctree"
diff --git a/extra-dev/packages/coq-hol-light/coq-hol-light.dev/opam b/extra-dev/packages/coq-hol-light/coq-hol-light.dev/opam
@@ -0,0 +1,61 @@
+opam-version: "2.0"
+synopsis: "HOL-Light library in Coq"
+description: """
+This library contains an automatic translation in Coq of (for the moment) some
+small part the HOL-Light library using https://github.com/Deducteam/hol2dk.
+"""
+homepage: "https://github.com/Deducteam/coq-hol-light"
+dev-repo: "git+https://github.com/Deducteam/coq-hol-light.git"
+bug-reports: "https://github.com/Deducteam/coq-hol-light/issues"
+doc: "https://github.com/Deducteam/coq-hol-light"
+maintainer: "frederic.blanqui@inria.fr"
+authors: ["Frédéric Blanqui"]
+license: "CeCILL-2.1"
+depends: [
+  "rocq-core" {= "dev"}
+  "coq-hol-light-real-with-N" {>= "2.0.0"}
+  "coq-fourcolor-reals" {>= "1.4.0"}
+]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+tags: [
+  "logpath:HOLLight"
+  "date:2025-03-13"
+  "category:Mathematics/Arithmetic and Number Theory/Miscellaneous"
+  "category:Mathematics/Real Numbers"
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword:HOL-Light"
+  "keyword:list"
+  "keyword:basic set theory"
+  "keyword:arithmetic"
+  "keyword:integer"
+  "keyword:real"
+  "keyword:complex"
+  "keyword:permutation"
+  "keyword:group"
+  "keyword:matroid"
+  "keyword:binomial"
+  "keyword:topology"
+  "keyword:metric"
+  "keyword:space"
+  "keyword:analysis"
+  "keyword:homology"
+  "keyword:vector"
+  "keyword:linear"
+  "keyword:algebra"
+  "keyword:convex"
+  "keyword:path"
+  "keyword:polytope"
+  "keyword:Brouwer"
+  "keyword:degree"
+  "keyword:derivative"
+  "keyword:Clifford"
+  "keyword:integration"
+  "keyword:measure"
+  "keyword:Lebesgue"
+  "keyword:transcendental"
+]
+
+url {
+  src: "git+https://github.com/Deducteam/coq-hol-light.git#main"
+}
diff --git a/extra-dev/packages/coq-infotheo/coq-infotheo.dev/opam b/extra-dev/packages/coq-infotheo/coq-infotheo.dev/opam
@@ -0,0 +1,22 @@
+opam-version: "2.0"
+maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
+
+homepage: "https://github.com/affeldt-aist/infotheo"
+dev-repo: "git+https://github.com/affeldt-aist/infotheo.git"
+bug-reports: "https://github.com/affeldt-aist/infotheo/issues"
+license: "LGPL-2.1-or-later"
+
+depends: [ "rocq-infotheo" { = version } ]
+authors: [
+  "Reynald Affeldt, AIST"
+  "Manabu Hagiwara, Chiba U. (previously AIST)"
+  "Jonas Senizergues, ENS Cachan (internship at AIST)"
+  "Jacques Garrigue, Nagoya U."
+  "Kazuhiko Sakaguchi, Tsukuba U."
+  "Taku Asai, Nagoya U. (M2)"
+  "Takafumi Saikawa, Nagoya U."
+  "Naruomi Obata, Titech (M2)"
+  "Alessandro Bruni, IT-University of Copenhagen"
+]
+
+synopsis: "Compatibility package for rocq-infotheo"
diff --git a/extra-dev/packages/coq-libvalidsdp/coq-libvalidsdp.dev/opam b/extra-dev/packages/coq-libvalidsdp/coq-libvalidsdp.dev/opam
@@ -9,22 +9,48 @@ dev-repo: "git+https://github.com/validsdp/validsdp.git"
 bug-reports: "https://github.com/validsdp/validsdp/issues"
 license: "LGPL-2.1-or-later"
 
+# Resynced from upstream's own libvalidsdp opam file on validsdp master
+# (a8caf102, coq-libvalidsdp.opam), which is maintained and which this row had
+# drifted years behind. The previous build: ran `./autogen.sh && ./configure`
+# first; upstream deleted autoconf, nothing matching autogen/configure/*.ac/*.am
+# exists on master, and running that step verbatim gives rc=127
+# `./autogen.sh: not found`. That is why this row has never compiled a .v file.
 build: [
-  ["sh" "-c" "cd libvalidsdp && ./autogen.sh && ./configure"]
   [make "-C" "libvalidsdp" "-j%{jobs}%"]
 ]
 install: [make "-C" "libvalidsdp" "install"]
+
 depends: [
-  "ocaml"
-  "coq" {>= "8.14"}
+  # Upstream writes this as a menu, `{((>= "9.0" & < "9.2~") | (= "dev"))}`,
+  # which permits a dev prover without ever requiring one -- the shape #59 fixed
+  # on rocq-infotheo.dev and rocq-laproof.dev. A .dev row tracking master has to
+  # require dev outright.
+  #
+  # Keep the package name `coq`; do NOT rename it to `rocq-core`. libvalidsdp's
+  # Makefile builds via `$(COQBIN)coq_makefile` with COQBIN derived from
+  # `which coqc`, and rocq-core ships neither binary -- they live in coq-core,
+  # whose synopsis is "Compatibility binaries for Coq after the Rocq renaming".
+  # The chain coq.dev -> coq-core {= version} -> rocq-runtime {= version} pins
+  # rocq master exactly as rocq-core {= "dev"} would, while keeping the binaries
+  # the build actually invokes.
+  "coq" {= "dev"}
   "coq-bignums"
   "coq-flocq" {>= "3.3.0"}
   "coq-coquelicot" {>= "3.0"}
+  # Upstream caps this `& < "5~"`. That cap is NOT carried here: opam versions
+  # order `dev` above every numeric version, so an upper bound is the one thing
+  # that can exclude dev, and `< "5~"` would forbid coq-interval.dev outright.
+  # A bare floor permits both a released interval and the dev one.
   "coq-interval" {>= "4.0.0"}
-  "coq-mathcomp-field" {>= "1.13"}
-  "coq-mathcomp-analysis" {>= "0.3.5"}
-  "ocamlfind" {build}
-  "conf-autoconf" {build}
+  # Upstream: `{(>= "2.3" & < "2.5~") | (= "dev")}` -- a menu whose numeric arm
+  # is the one the solver actually takes (#38/#48). Pinned to dev here, matching
+  # what #58 did to rocq-mathcomp-classical.dev. coq-mathcomp-field.dev is a
+  # pure compat shim, `depends: ["rocq-mathcomp-field" {= version}]`, so this
+  # resolves to rocq-mathcomp-field.dev -- which is what the source port was
+  # measured against.
+  "coq-mathcomp-field" {= "dev"}
+  # Replaces coq-mathcomp-analysis, which upstream dropped for this package.
+  "coq-mathcomp-reals-stdlib" {>= "1.8.0"}
 ]
 synopsis: "LibValidSDP"
 description: """
@@ -49,6 +75,11 @@ authors: [
   "Pierre Roux <pierre.roux@onera.fr>"
   "Érik Martin-Dorel <erik.martin-dorel@irit.fr>"
 ]
+# NOT repointed at any fork. Upstream master does not yet carry the Rocq dev
+# port -- a clean clone of master gives 0/19, dying at libvalidsdp/misc.v:80 --
+# so this row still goes red at dev until the upstream PR lands. It goes red
+# mid-compile now instead of at rc=127 in build step 1, which is the point of
+# the resync: it is ready the moment upstream moves.
 url {
   src: "git+https://github.com/validsdp/validsdp.git#master"
 }
diff --git a/extra-dev/packages/coq-mathcomp-cad/coq-mathcomp-cad.dev/opam b/extra-dev/packages/coq-mathcomp-cad/coq-mathcomp-cad.dev/opam
@@ -0,0 +1,47 @@
+# 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/cad"
+dev-repo: "git+https://github.com/math-comp/cad.git"
+bug-reports: "https://github.com/math-comp/cad/issues"
+license: "LGPL-3.0-or-later"
+
+synopsis: "Formal Proof of Cylindrical Algebraic Decomposition"
+description: """
+This library contains a formal proof of Collins' Cylindical
+Aglebraic Decomposition, using the Mathematical Components Library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.18"}
+  "coq-hierarchy-builder" 
+  "coq-mathcomp-ssreflect" {= "2.2.0" }
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-fingroup" 
+  "coq-mathcomp-solvable" 
+  "coq-mathcomp-field" 
+  "coq-mathcomp-bigenough" {>= "1.0.1"}
+  "coq-mathcomp-finmap" {>= "1.0.1"}
+  "coq-mathcomp-multinomials" {>= "2.2.0"}
+  "coq-mathcomp-real-closed" {>= "2.0.1"}
+  "coq-mathcomp-classical" {>= "1.1.0"}
+  "coq-mathcomp-analysis" {>= "1.1.0"}
+]
+
+tags: [
+  "keyword:CAD"
+  "logpath:SemiAlgebraic"
+]
+authors: [
+  "Cyril Cohen"
+  "Boris Djalal"
+  "Quentin Vermande"
+]
+
+url {
+  src: "git+https://github.com/math-comp/cad.git#master"
+}