diff --git a/extra-dev/packages/coq-coinduction/coq-coinduction.dev/opam b/extra-dev/packages/coq-coinduction/coq-coinduction.dev/opam index 2beddbfe87..749e0fdfd8 100644 --- 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 index 26bfeb847e..06d44cf327 100644 --- 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 " +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 index 89af88fdab..39b7c831ed 100644 --- 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 new file mode 100644 index 0000000000..4f8bbb2f49 --- /dev/null +++ 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 new file mode 100644 index 0000000000..a83933350a --- /dev/null +++ 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 new file mode 100644 index 0000000000..8ccec15734 --- /dev/null +++ b/extra-dev/packages/coq-infotheo/coq-infotheo.dev/opam @@ -0,0 +1,22 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " + +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 index b409bbc1e6..883f973737 100644 --- 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 " "Érik Martin-Dorel " ] +# 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 new file mode 100644 index 0000000000..f9e071ce8c --- /dev/null +++ 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 " + +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" +} diff --git a/extra-dev/packages/coq-mathcomp-word/coq-mathcomp-word.dev/opam b/extra-dev/packages/coq-mathcomp-word/coq-mathcomp-word.dev/opam index 57fa7005e3..c12002a2c7 100644 --- a/extra-dev/packages/coq-mathcomp-word/coq-mathcomp-word.dev/opam +++ b/extra-dev/packages/coq-mathcomp-word/coq-mathcomp-word.dev/opam @@ -10,7 +10,17 @@ depends: [ "dune" {>= "2.8"} "coq-core" {= "dev"} "coq-stdlib" - "coq-mathcomp-ssreflect" {(>= "2.4" & < "2.7~")} + # Pinned rather than a menu on purpose. The old range admitted 2.4.0, 2.5.0 + # and 2.6.0, and a range is excluded only if every member is: 2.4.0 and + # 2.5.0 are capped below a dev prover, but 2.6.0 reaches + # rocq-mathcomp-boot.2.6.0, which declares "rocq-core" {>= "9.0"} with no + # upper bound. So the dev prover above did not on its own exclude released + # mathcomp; the top of the range decided it. + "coq-mathcomp-ssreflect" {= "dev"} + # Left unconstrained on purpose, not by oversight. The pin above closes it: + # algebra 1.6 to 2.3.0 reach ssreflect through coq-mathcomp-fingroup + # {= version}, and 2.4.0 onwards are shims over rocq-mathcomp-algebra, whose + # {= version} locks on order and finite-group land on the same boot. "coq-mathcomp-algebra" ] synopsis: "Yet Another Coq Library on Machine Words" diff --git a/extra-dev/packages/coq-pil/coq-pil.dev/opam b/extra-dev/packages/coq-pil/coq-pil.dev/opam new file mode 100644 index 0000000000..8a97ce27c0 --- /dev/null +++ b/extra-dev/packages/coq-pil/coq-pil.dev/opam @@ -0,0 +1,17 @@ +opam-version: "2.0" +maintainer: "feree@irif.fr" + +homepage: "https://github.com/hferee/rocq-pil" +dev-repo: "git+https://github.com/hferee/rocq-pil.git" +bug-reports: "https://github.com/hferee/rocq-pil/issues" +doc: "https://hferee.github.io/UIML" +license: "CECILL-2.1" + +depends: [ "rocq-pil" { = version } ] +authors: [ + "Hugo Férée" + "Sam van Gool" + "Yago Iglesias Vasquez" +] + +synopsis: "Compatibility package for rocq-pil" diff --git a/extra-dev/packages/coq-pprint/coq-pprint.dev/opam b/extra-dev/packages/coq-pprint/coq-pprint.dev/opam new file mode 100644 index 0000000000..16a4ec1a62 --- /dev/null +++ b/extra-dev/packages/coq-pprint/coq-pprint.dev/opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +synopsis: "A modern combinator pretty-printing library for Coq" +description: """ +A combinator pretty-printing library, in the style of Wadler's "A Prettier Printer". +- Handles utf-8 strings. +- Supports generic _annotations_ on text (colors, italics, etc). +- Well documented.""" +maintainer: ["Mathis Bouverot-Dupuis (mathis.bouverot@ens.psl.eu)"] +authors: ["Mathis Bouverot-Dupuis"] +license: "MIT" +homepage: "https://github.com/MathisBD/coq-pprint" +bug-reports: "https://github.com/MathisBD/coq-pprint/issues" +dev-repo: "git+https://github.com/MathisBD/coq-pprint.git" +depends: [ + "dune" {>= "3.13"} + "coq" {= "dev"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] + +url { + src: "git+https://github.com/MathisBD/coq-pprint.git#master" +} diff --git a/extra-dev/packages/coq-record-update/coq-record-update.dev/opam b/extra-dev/packages/coq-record-update/coq-record-update.dev/opam index e96dd79fc6..32b2fe2b98 100644 --- a/extra-dev/packages/coq-record-update/coq-record-update.dev/opam +++ b/extra-dev/packages/coq-record-update/coq-record-update.dev/opam @@ -19,7 +19,13 @@ simple typeclass that lists out the record fields.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq-core" {(>= "8.17" & < "9.3") | (= "dev")} + # The `meta.yml` header above describes tchajed/coq-record-update's own + # generated opam file, not this one -- this row is absent at upstream/master + # and was added by bf05c0086, so nothing regenerates it. Keep `coq-core` + # rather than `rocq-core`: the build is a coq_makefile Makefile that calls + # coqc, and at dev those binaries live in coq-core, whose whole synopsis is + # "compatibility binaries ... like coqc coqtop". + "coq-core" {= "dev"} ("coq-stdlib" {>= "8.17" & < "9.0"} | "rocq-stdlib" {(>= "9.0" & < "9.2") | (= "dev")}) ] diff --git a/extra-dev/packages/coq-riscv/coq-riscv.dev/opam b/extra-dev/packages/coq-riscv/coq-riscv.dev/opam index 9e26deceff..870115d793 100644 --- a/extra-dev/packages/coq-riscv/coq-riscv.dev/opam +++ b/extra-dev/packages/coq-riscv/coq-riscv.dev/opam @@ -11,9 +11,16 @@ build: [ ] install: [make "EXTERNAL_DEPENDENCIES=1" "install"] depends: [ - "coq" {>= "8.18~" | = "dev"} - ("coq-coqutil" {>= "0.0.7" | = "dev"} | "coq-fiat-crypto-with-bedrock") - "coq-record-update" {>= "0.3.0" | = "dev"} + "coq" {= "dev"} + # Upstream's disjunction, kept as a disjunction: riscv-coq builds against + # coqutil, or against coq-fiat-crypto-with-bedrock, which vendors it. Both + # arms are pinned rather than only the first. The second pin is redundant + # today -- coq-fiat-crypto-with-bedrock publishes no version but .dev in this + # archive -- and is written anyway so that publishing a released one later + # cannot quietly reintroduce a released dependency on a row whose whole + # purpose is to track master. + ("coq-coqutil" {= "dev"} | "coq-fiat-crypto-with-bedrock" {= "dev"}) + "coq-record-update" {= "dev"} ] dev-repo: "git+https://github.com/mit-plv/riscv-coq.git" synopsis: "RISC-V Specification in Coq, somewhat experimental" diff --git a/extra-dev/packages/coq-sflib/coq-sflib.dev/opam b/extra-dev/packages/coq-sflib/coq-sflib.dev/opam new file mode 100644 index 0000000000..bda70b6196 --- /dev/null +++ b/extra-dev/packages/coq-sflib/coq-sflib.dev/opam @@ -0,0 +1,40 @@ +opam-version: "2.0" +synopsis: "A collection of useful Rocq lemmas and tactics" +description: + "This package provides useful Rocq lemmas and tactics for proof automation and rewriting." +maintainer: ["yeji.han@sf.snu.ac.kr"] +authors: [ + "Jeehoon Kang " + "Minki Cho " + "Jaehyung Lee " + "Yeji Han " + "Gil Hur " +] +license: "BSD-2-Clause" +homepage: "https://github.com/snu-sf/sflib" +bug-reports: "https://github.com/snu-sf/sflib/issues" +depends: [ + "coq-core" {= "dev"} + "rocq-stdlib" {= "dev"} + "dune" {>= "3.8" & >= "3.8"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/snu-sf/sflib.git" + +url { + src: "git+https://github.com/snu-sf/sflib.git#master" +} diff --git a/extra-dev/packages/coq-ssprove/coq-ssprove.dev/opam b/extra-dev/packages/coq-ssprove/coq-ssprove.dev/opam new file mode 100644 index 0000000000..12ebaf268a --- /dev/null +++ b/extra-dev/packages/coq-ssprove/coq-ssprove.dev/opam @@ -0,0 +1,13 @@ +opam-version: "2.0" +maintainer: "philipp@haselwarter.org" + +homepage: "https://github.com/SSProve/ssprove" +dev-repo: "git+https://github.com/SSProve/ssprove.git" +bug-reports: "https://github.com/SSProve/ssprove/issues" +doc: "https://SSProve.github.io/ssprove/index.html" +license: "MIT" + +depends: [ "rocq-ssprove" { = version } ] +authors: ["SSProve team"] + +synopsis: "Compatibility package for rocq-ssprove" diff --git a/extra-dev/packages/coq-trocq-hott-examples/coq-trocq-hott-examples.dev/opam b/extra-dev/packages/coq-trocq-hott-examples/coq-trocq-hott-examples.dev/opam new file mode 100644 index 0000000000..d195321123 --- /dev/null +++ b/extra-dev/packages/coq-trocq-hott-examples/coq-trocq-hott-examples.dev/opam @@ -0,0 +1,41 @@ +opam-version: "2.0" +maintainer: "Cyril Cohen " + +homepage: "https://github.com/coq-community/trocq" +dev-repo: "git+https://github.com/coq-community/trocq.git" +bug-reports: "https://github.com/coq-community/trocq/issues" +license: "LGPL-3.0-or-later" + +synopsis: "A modular parametricity plugin for proof transfer in Coq: examples" +description: """ +Tests for applications of Trocq +""" + +build: [make "-C" "examples/hott" "-j%{jobs}%"] +install: [make "-C" "examples/hott" "install"] +depends: [ + "coq" {= "dev"} + "coq-trocq-hott" +] + +tags: [ + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "category:Miscellaneous/Coq Extensions" + "keyword:automation" + "keyword:elpi" + "keyword:proof transfer" + "keyword:isomorphism" + "keyword:univalence" + "keyword:parametricity" + "logpath:Trocq" +] +authors: [ + "Cyril Cohen" + "Enzo Crance" + "Lucie Lahaye" + "Assia Mahboubi" +] + +url { + src: "git+https://github.com/coq-community/trocq.git#master" +} diff --git a/extra-dev/packages/coq-trocq-hott/coq-trocq-hott.dev/opam b/extra-dev/packages/coq-trocq-hott/coq-trocq-hott.dev/opam new file mode 100644 index 0000000000..cace06a4c7 --- /dev/null +++ b/extra-dev/packages/coq-trocq-hott/coq-trocq-hott.dev/opam @@ -0,0 +1,67 @@ +# 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: "Enzo Crance " + +homepage: "https://github.com/coq-community/trocq" +dev-repo: "git+https://github.com/coq-community/trocq.git" +bug-reports: "https://github.com/coq-community/trocq/issues" +license: "LGPL-3.0-or-later" + +synopsis: "A modular parametricity plugin for proof transfer in Coq" +description: """ +Trocq is a modular parametricity plugin for Coq. It can be used to +achieve proof transfer by both translating a user goal into another, +related, variant, and computing a proof that proves the corresponding implication. + +The plugin features a hierarchy of structures on relations, whose +instances are computed from registered user-defined proof via +parametricity. This hierarchy ranges from structure-less relations +to an original formulation of type equivalence. The resulting +framework generalizes [raw +parametricity](https://arxiv.org/abs/1209.6336), [univalent +parametricity](https://doi.org/10.1145/3429979) and +[CoqEAL](https://github.com/coq-community/coqeal), and includes them +in a unified framework. + +The plugin computes a parametricity translation "à la carte", by +performing a fine-grained analysis of the requires properties for a +given proof of relatedness. In particular, it is able to prove +implications without resorting to full-blown type equivalence, +allowing this way to perform proof transfer without necessarily +pulling in the univalence axiom. + +The plugin is implemented in Coq-Elpi and the code of the +parametricity translation is fairly close to a pen-and-paper +sequent-style presentation.""" + +build: [make "-j%{jobs}%" "hott"] +install: [make "install" "-C" "hott"] +depends: [ + "coq" {= "dev"} + "coq-elpi" {>= "3.4.0"} + "coq-hott" +] + +tags: [ + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "category:Miscellaneous/Coq Extensions" + "keyword:automation" + "keyword:elpi" + "keyword:proof transfer" + "keyword:isomorphism" + "keyword:univalence" + "keyword:parametricity" + "logpath:Trocq" +] +authors: [ + "Cyril Cohen" + "Enzo Crance" + "Lucie Lahaye" + "Assia Mahboubi" +] + +url { + src: "git+https://github.com/coq-community/trocq.git#master" +} diff --git a/extra-dev/packages/coq-trocq-std-examples/coq-trocq-std-examples.dev/opam b/extra-dev/packages/coq-trocq-std-examples/coq-trocq-std-examples.dev/opam new file mode 100644 index 0000000000..9658f37bf9 --- /dev/null +++ b/extra-dev/packages/coq-trocq-std-examples/coq-trocq-std-examples.dev/opam @@ -0,0 +1,50 @@ +opam-version: "2.0" +maintainer: "Cyril Cohen " + +homepage: "https://github.com/coq-community/trocq" +dev-repo: "git+https://github.com/coq-community/trocq.git" +bug-reports: "https://github.com/coq-community/trocq/issues" +license: "LGPL-3.0-or-later" + +synopsis: "A modular parametricity plugin for proof transfer in Coq: examples" +description: """ +Tests for applications of Trocq +""" + +build: [make "-C" "examples/std" "-j%{jobs}%"] +install: [make "-C" "examples/std" "install"] +depends: [ + "coq" {= "dev"} + # NEW dependency, not a bumped bound: this recipe declared no ssreflect at all. + # 3 of the 15 .v files under examples/std require `all_boot` (int_to_Zp.v, + # flt3_step.v, square_and_cube_mod7.v), and examples/std is exactly what + # `build: [make -C examples/std]` compiles. `all_boot` ships from + # rocq-mathcomp-boot, which exists only at 2.5.0 and above. The bare + # coq-mathcomp-algebra below cannot express this: it reaches ssreflect through + # its own {= version} lock, which pins downward rather than lifting a floor. + "coq-mathcomp-ssreflect" {>= "2.5.0"} + "coq-mathcomp-algebra" + "coq-trocq-std" +] + +tags: [ + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "category:Miscellaneous/Coq Extensions" + "keyword:automation" + "keyword:elpi" + "keyword:proof transfer" + "keyword:isomorphism" + "keyword:univalence" + "keyword:parametricity" + "logpath:Trocq" +] +authors: [ + "Cyril Cohen" + "Enzo Crance" + "Lucie Lahaye" + "Assia Mahboubi" +] + +url { + src: "git+https://github.com/coq-community/trocq.git#master" +} diff --git a/extra-dev/packages/coq-trocq-std/coq-trocq-std.dev/opam b/extra-dev/packages/coq-trocq-std/coq-trocq-std.dev/opam new file mode 100644 index 0000000000..ba18d90f9b --- /dev/null +++ b/extra-dev/packages/coq-trocq-std/coq-trocq-std.dev/opam @@ -0,0 +1,67 @@ +# 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: "Enzo Crance " + +homepage: "https://github.com/coq-community/trocq" +dev-repo: "git+https://github.com/coq-community/trocq.git" +bug-reports: "https://github.com/coq-community/trocq/issues" +license: "LGPL-3.0-or-later" + +synopsis: "A modular parametricity plugin for proof transfer in Coq" +description: """ +Trocq is a modular parametricity plugin for Coq. It can be used to +achieve proof transfer by both translating a user goal into another, +related, variant, and computing a proof that proves the corresponding implication. + +The plugin features a hierarchy of structures on relations, whose +instances are computed from registered user-defined proof via +parametricity. This hierarchy ranges from structure-less relations +to an original formulation of type equivalence. The resulting +framework generalizes [raw +parametricity](https://arxiv.org/abs/1209.6336), [univalent +parametricity](https://doi.org/10.1145/3429979) and +[CoqEAL](https://github.com/coq-community/coqeal), and includes them +in a unified framework. + +The plugin computes a parametricity translation "à la carte", by +performing a fine-grained analysis of the requires properties for a +given proof of relatedness. In particular, it is able to prove +implications without resorting to full-blown type equivalence, +allowing this way to perform proof transfer without necessarily +pulling in the univalence axiom. + +The plugin is implemented in Coq-Elpi and the code of the +parametricity translation is fairly close to a pen-and-paper +sequent-style presentation.""" + +build: [make "-j%{jobs}%" "std"] +install: [make "install" "-C" "std"] +depends: [ + "coq" {= "dev"} + "coq-elpi" {>= "3.4.0"} +] + +tags: [ + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "category:Miscellaneous/Coq Extensions" + "keyword:automation" + "keyword:elpi" + "keyword:proof transfer" + "keyword:isomorphism" + "keyword:univalence" + "keyword:parametricity" + "logpath:Trocq" +] +authors: [ + "Samy Avrillon" + "Cyril Cohen" + "Enzo Crance" + "Lucie Lahaye" + "Assia Mahboubi" +] + +url { + src: "git+https://github.com/coq-community/trocq.git#master" +} diff --git a/extra-dev/packages/coq-validsdp/coq-validsdp.dev/opam b/extra-dev/packages/coq-validsdp/coq-validsdp.dev/opam index afe9f59304..f2c9980361 100644 --- a/extra-dev/packages/coq-validsdp/coq-validsdp.dev/opam +++ b/extra-dev/packages/coq-validsdp/coq-validsdp.dev/opam @@ -9,26 +9,59 @@ 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 opam file on validsdp master (a8caf102, +# coq-validsdp.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" "./autogen.sh && ./configure"] [make "-j%{jobs}%"] ] +run-test: [make "-j%{jobs}%" "test"] install: [make "install"] depends: [ + # ocaml/ocamlfind stay: unlike libvalidsdp, this package builds an OCaml + # plugin (plugins/soswitness). conf-autoconf goes with the deleted step above. "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`. validsdp'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"} + # 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"} + # 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"} + # New upstream dependency. + "coq-mathcomp-reals-stdlib" {>= "1.8.0"} "coq-libvalidsdp" {= "dev"} - "coq-mathcomp-multinomials" {>= "1.2"} - "coq-coqeal" {>= "1.1.0"} - "coq-paramcoq" {>= "1.1.0"} - "osdp" {>= "1.0"} + "coq-mathcomp-multinomials" {>= "2.0"} + "coq-coqeal" {>= "2.1"} + # coq-paramcoq dropped: absent from upstream's depends: list. (Why it is no + # longer needed is not established here -- only that upstream stopped + # declaring it.) + "osdp" {>= "1.1.1"} "ocamlfind" {build} - "conf-autoconf" {build} ] synopsis: "ValidSDP" description: """ diff --git a/extra-dev/packages/coq-vcfloat/coq-vcfloat.dev/opam b/extra-dev/packages/coq-vcfloat/coq-vcfloat.dev/opam new file mode 100644 index 0000000000..3b37a7df5f --- /dev/null +++ b/extra-dev/packages/coq-vcfloat/coq-vcfloat.dev/opam @@ -0,0 +1,52 @@ +# the _real_ opam file for coq-vcfloat is at [adjusted for version number] +# https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-vcfloat/coq-vcfloat.2.1.1/opam +opam-version: "2.0" +synopsis: "VCFloat: Floating Point Round-off Error Analysis" +description: "VCFloat is a tool for Coq proofs about floating-point round-off error." +authors: [ + "Andrew W. Appel" + "Ariel E. Kellison" + "Tahina Ramananandro" + "Paul Mountcastle" + "Benoit Meister" + "Richard Lethin" +] +homepage: "https://verinum.org/vcfloat/" +maintainer: "Andrew W. Appel " +dev-repo: "git+https://github.com/VeriNum/vcfloat" +bug-reports: "https://github.com/VeriNum/vcfloat/issues" +license: "LGPL-3.0-or-later" + +build: [ + [ make "-C" "vcfloat" "-j%{jobs}%" "vcfloat2" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.13~"}] +] +install: [ + [make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.13~"}] +] +run-test: [ + [make "-C" "vcfloat" "-j%{jobs}%" "tests" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.13~"}] +] +depends: [ + # Not a floor-or-dev menu like the rows tightened in f902bba36: the released + # arm is a capped interval that genuinely selects, admitting every Coq from + # 8.16 up to but not including 8.19. This row exists to build vcfloat master + # against Rocq master, so a solver falling back to 8.18 does not degrade + # gracefully -- it tests something nobody asked for and reports it as the dev + # build. Deleting the released arm leaves the arm that was already here. + "coq" {= "dev"} + "coq-flocq" {>= "4.1.1" & < "5.0"} + "coq-interval" {>= "4.8.0"} + "coq-compcert" {>= "3.12"} + "coq-bignums" +] +tags: [ + "date:2023-08-31" + "keyword:decision procedure" + "keyword:floating-point arithmetic" + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "logpath:VCFloat" + ] + +url { + src: "git+https://github.com/VeriNum/vcfloat.git#master" +} diff --git a/extra-dev/packages/coq-vst-lib/coq-vst-lib.dev/opam b/extra-dev/packages/coq-vst-lib/coq-vst-lib.dev/opam new file mode 100644 index 0000000000..50853b7121 --- /dev/null +++ b/extra-dev/packages/coq-vst-lib/coq-vst-lib.dev/opam @@ -0,0 +1,35 @@ +# the _real_ opam file for coq-vst-lib is at [adjusted for version number] +# https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-vst-lib/coq-vst-lib.2.12/opam +opam-version: "2.0" +synopsis: "VSTlib: VST-verified C library for VST-verified clients" +description: "These program modules, in the form of Verified Software Units, +may be linked with client-module code (at the .c/.o level) and proofs (at the .v level)." +authors: [ + "Andrew W. Appel" +] +maintainer: "Andrew W. Appel " +homepage: "http://" +dev-repo: "git+https://github.com/PrincetonUniversity/VST" +bug-reports: "https://github.com/PrincetonUniversity/VST/issues" +license: "BSD-2-Clause" + +build: [ + [ make "-j%{jobs}%" "proof-only"] +] +install: [ + [ make "install" "INSTALLDIR=%{lib}%/coq/user-contrib/VSTlib"] +] +run-test: [ + [ make "-j%{jobs}%" "test-only"] +] +depends: [ + "coq" {= "dev"} + "coq-compcert" {>= "3.11"} + "coq-flocq" {>= "4.1.0" & < "5.0"} + "coq-vcfloat" {>= "2.0"} + "coq-vst" {>= "2.11.1"} +] + +url { + src: "git+https://github.com/PrincetonUniversity/VST.git#master" +} diff --git a/extra-dev/packages/rocq-categories/rocq-categories.dev/opam b/extra-dev/packages/rocq-categories/rocq-categories.dev/opam new file mode 100644 index 0000000000..20319ebc21 --- /dev/null +++ b/extra-dev/packages/rocq-categories/rocq-categories.dev/opam @@ -0,0 +1,40 @@ +opam-version: "2.0" +maintainer: "Damien Pous " + +homepage: "https://github.com/damien-pous/categories" +dev-repo: "git+https://github.com/damien-pous/categories.git" +bug-reports: "https://github.com/damien-pous/categories/issues" +license: "LGPL-3.0-or-later" + +synopsis: "A library for category theory" +description: """ +Library about category theory, with hom-setoids. +Hierarchy of structures implemented with Hierarchy Builder. +Inference of MacLane morphisms and decision procedure for monoidal categories. +""" + +build: [ + [make "-j%{jobs}%" ] +] +install: [make "install"] +depends: [ + "rocq-core" {= "dev"} + "rocq-stdlib" {= "dev"} + "rocq-partial-orders" {= "dev"} +] + +tags: [ + "keyword:category theory" + "keyword:monoidal categories" + "keyword:MacLane's coherence theorem" + "keyword:string diagrams" + "keyword:setoid" + "date:2026-05-07" +] +authors: [ + "Damien Pous " +] + +url { + src: "git+https://github.com/damien-pous/categories.git#main" +} diff --git a/extra-dev/packages/rocq-ceres-bytestring/rocq-ceres-bytestring.dev/opam b/extra-dev/packages/rocq-ceres-bytestring/rocq-ceres-bytestring.dev/opam new file mode 100644 index 0000000000..910938d6be --- /dev/null +++ b/extra-dev/packages/rocq-ceres-bytestring/rocq-ceres-bytestring.dev/opam @@ -0,0 +1,35 @@ +opam-version: "2.0" +synopsis: "Library for serialization via S-expressions using bytestrings" +maintainer: ["The Peregrine team"] +authors: ["Li-yao Xia"] +license: "MIT" +homepage: "https://github.com/peregrine-project/rocq-ceres-bytestring" +bug-reports: + "https://github.com/peregrine-project/rocq-ceres-bytestring/issues" +depends: [ + "dune" {>= "2.8"} + "coq" {= "dev"} + "rocq-metarocq-utils" {>= "1.4~"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: + "git+https://github.com/peregrine-project/rocq-ceres-bytestring.git" +run-test: [ "dune" "build" "-p" name "test" "tutorial" ] + +url { + src: "git+https://github.com/peregrine-project/rocq-ceres-bytestring.git#master" +} diff --git a/extra-dev/packages/rocq-coinduction/rocq-coinduction.dev/opam b/extra-dev/packages/rocq-coinduction/rocq-coinduction.dev/opam new file mode 100644 index 0000000000..a0cf842b53 --- /dev/null +++ b/extra-dev/packages/rocq-coinduction/rocq-coinduction.dev/opam @@ -0,0 +1,40 @@ +opam-version: "2.0" +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: "GNU LGPL" + +synopsis: "A library 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: [ + "rocq-core" {= "dev"} + "rocq-stdlib" {= "dev"} +] + +tags: [ + "keyword:coinduction" + "keyword:up to techniques" + "keyword:companion" + "keyword:bisimilarity" + "logpath:Coinduction" +] +authors: [ + "Damien Pous" +] + +conflicts: [ "coq-coinduction" { != version } ] + +url { + src: "git+https://github.com/damien-pous/coinduction.git#master" +} diff --git a/extra-dev/packages/rocq-color/rocq-color.dev/opam b/extra-dev/packages/rocq-color/rocq-color.dev/opam new file mode 100644 index 0000000000..c8cbc913a6 --- /dev/null +++ b/extra-dev/packages/rocq-color/rocq-color.dev/opam @@ -0,0 +1,116 @@ +opam-version: "2.0" +synopsis: "A library on rewriting theory and termination" +homepage: "https://github.com/fblanqui/color/" +license: "CeCILL-2.1" +bug-reports: "https://github.com/fblanqui/color/issues" +dev-repo: "git+https://github.com/fblanqui/color.git" +depends: [ + "ocaml" + "rocq-core" {= "dev"} + "rocq-bignums" {= "dev"} +] +build: [make "-j%{jobs}%"] +install: [make "-f" "rocq.mk" "install"] +flags: light-uninstall +remove: ["rm" "-R" "%{lib}%/coq/user-contrib/CoLoR"] +maintainer: "frederic.blanqui@inria.fr" +authors: [ + "Frédéric Blanqui" + "Adam Koprowski" + "Sébastien Hinderer" + "Pierre-Yves Strub" + "Sidi Ould Biha" + "Solange Coupet-Grimal" + "William Delobel" + "Hans Zantema" + "Stéphane Leroux" + "Léo Ducas" + "Johannes Waldmann" + "Qiand Wang" + "Lianyi Zhang" + "Sorin Stratulat" +] +tags: [ + "date:2026-07-07" + + "logpath:CoLoR" + + "category:Computer Science/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:polynom" + "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-founded" + "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 component" + "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" +] + +conflicts: [ "coq-color" { != version } ] + +url { + src: "git+https://github.com/fblanqui/color.git#master" +} diff --git a/extra-dev/packages/rocq-concert-examples/rocq-concert-examples.dev/opam b/extra-dev/packages/rocq-concert-examples/rocq-concert-examples.dev/opam new file mode 100644 index 0000000000..814bafed42 --- /dev/null +++ b/extra-dev/packages/rocq-concert-examples/rocq-concert-examples.dev/opam @@ -0,0 +1,26 @@ +opam-version: "2.0" +name: "rocq-concert-examples" +synopsis: "A framework for smart contract verification in Rocq" +description: """ +A framework for smart contract verification in Rocq +""" +maintainer: "Danil Annenkov " +authors: "The COBRA team" +license: "MIT" +homepage: "https://github.com/AU-COBRA/ConCert" +dev-repo: "git+https://github.com/AU-COBRA/ConCert.git" +bug-reports: "https://github.com/AU-COBRA/ConCert/issues" +doc: "https://au-cobra.github.io/ConCert/toc.html" + +depends: [ + "rocq-concert" {= version} +] + +build: [ + ["dune" "subst"] {dev} + ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc} "--stop-on-first-error"] +] + +url { + src: "git+https://github.com/AU-COBRA/ConCert.git#master" +} diff --git a/extra-dev/packages/rocq-concert/rocq-concert.dev/opam b/extra-dev/packages/rocq-concert/rocq-concert.dev/opam new file mode 100644 index 0000000000..3131a0eb7c --- /dev/null +++ b/extra-dev/packages/rocq-concert/rocq-concert.dev/opam @@ -0,0 +1,33 @@ +opam-version: "2.0" +name: "rocq-concert" +synopsis: "A framework for smart contract verification in Rocq" +description: """ +A framework for smart contract verification in Rocq +""" +maintainer: "Danil Annenkov " +authors: "The COBRA team" +license: "MIT" +homepage: "https://github.com/AU-COBRA/ConCert" +dev-repo: "git+https://github.com/AU-COBRA/ConCert.git" +bug-reports: "https://github.com/AU-COBRA/ConCert/issues" +doc: "https://au-cobra.github.io/ConCert/toc.html" + +depends: [ + "rocq-core" {= "dev"} + "rocq-stdlib" {= "dev"} + "rocq-bignums" {>= "9"} + "coq-quickchick" {>= "2.0.4"} + "rocq-metarocq-erasure" {>= "1.5.1"} + "rocq-rust-extraction" {>= "0.2.1"} + "rocq-elm-extraction" {>= "0.2.1"} + "rocq-stdpp" {>= "1.13.0"} +] + +build: [ + ["dune" "subst"] {dev} + ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc} "--stop-on-first-error"] +] + +url { + src: "git+https://github.com/AU-COBRA/ConCert.git#master" +} diff --git a/extra-dev/packages/rocq-ctree/rocq-ctree.dev/opam b/extra-dev/packages/rocq-ctree/rocq-ctree.dev/opam new file mode 100644 index 0000000000..25c38a807e --- /dev/null +++ b/extra-dev/packages/rocq-ctree/rocq-ctree.dev/opam @@ -0,0 +1,55 @@ +opam-version: "2.0" +synopsis: + "Library for representing recursive, non-deterministic and impure programs with equational reasoning" +maintainer: ["Yannick Zakowski"] +authors: [ + "Nicolas Chappe" + "Paul He" + "Ludovic Henrio" + "Yannick Zakowski" + "Steve Zdancewic" +] +license: "MIT" +tags: [ + "category:CS/Semantics and Compilation/Semantics" + "category:CS/Concurrency/Theory of concurrent systems" + "keyword:simulation" + "keyword:bisimilarity" + "keyword:coinduction up-to" + "keyword:process algebra" + "keyword:cooperative multithreading" + "logpath:CTree" +] +homepage: "https://github.com/vellvm/ctrees" +bug-reports: "https://github.com/vellvm/ctrees/issues" +depends: [ + "dune" {>= "3.8" & < "3.24"} + "rocq-core" {= "dev"} + "rocq-stdlib" {= "dev"} + "coq-ext-lib" {>= "0.11.3"} + "rocq-coinduction" {>= "1.21"} + "rocq-relation-algebra" {>= "1.8.0"} + "rocq-equations" {>= "1.3.1"} + "coq-itree" {>= "5.0"} + "odoc" {with-doc} +] +conflicts: [ "coq-ctree" {!= version} ] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/vellvm/ctrees.git" + +url { + src: "git+https://github.com/vellvm/ctrees.git#dev" +} diff --git a/extra-dev/packages/rocq-elm-extraction/rocq-elm-extraction.dev/opam b/extra-dev/packages/rocq-elm-extraction/rocq-elm-extraction.dev/opam new file mode 100644 index 0000000000..a4d67a0a27 --- /dev/null +++ b/extra-dev/packages/rocq-elm-extraction/rocq-elm-extraction.dev/opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +name: "rocq-elm-extraction" +synopsis: "Rocq extraction to Elm" +description: """ +A framework for extracting Rocq programs to Elm +""" +maintainer: "Danil Annenkov " +authors: "The COBRA team" +license: "MIT" +homepage: "https://github.com/peregrine-project/rocq-typed-extraction" +dev-repo: "git+https://github.com/peregrine-project/rocq-typed-extraction.git" +bug-reports: "https://github.com/peregrine-project/rocq-typed-extraction/issues" +doc: "https://peregrine-project.github.io/rocq-typed-extraction/toc.html" + +depends: [ + "rocq-typed-extraction-common" {= version} +] + +build: [ + ["bash" "./configure.sh"] + [make "-j" "%{jobs}%" "-C" "elm"] +] + +install: [ + [make "-C" "elm" "install"] +] + +tags: [ + "keyword:elm" + "keyword:extraction" + "logpath:TypedExtraction" +] + +url { + src: "git+https://github.com/peregrine-project/rocq-typed-extraction.git#master" +} diff --git a/extra-dev/packages/rocq-elpi-json/rocq-elpi-json.dev/opam b/extra-dev/packages/rocq-elpi-json/rocq-elpi-json.dev/opam new file mode 100644 index 0000000000..1889c2cac0 --- /dev/null +++ b/extra-dev/packages/rocq-elpi-json/rocq-elpi-json.dev/opam @@ -0,0 +1,34 @@ +opam-version: "2.0" +synopsis: "Yojson bindings for rocq-elpi" +description: "This package provides basic support for reading and writing json files from Elpi programs running in Rocq" +maintainer: ["Enrico Tassi "] +authors: ["Enrico Tassi "] +license: "LGPL-2.1-or-later" +homepage: "https://github.com/LPCIC/coq-elpi/apps/json/" +bug-reports: "https://github.com/LPCIC/coq-elpi/issues" +depends: [ + "dune" {>= "3.13" & < "3.24"} + "rocq-elpi" {= "dev"} + "yojson" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "etc/with-rocq-wrap.sh" {!coq-core:installed} + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" + +url { + src: "git+https://github.com/LPCIC/coq-elpi.git#master" +} diff --git a/extra-dev/packages/rocq-elpi-xml/rocq-elpi-xml.dev/opam b/extra-dev/packages/rocq-elpi-xml/rocq-elpi-xml.dev/opam new file mode 100644 index 0000000000..50055cb083 --- /dev/null +++ b/extra-dev/packages/rocq-elpi-xml/rocq-elpi-xml.dev/opam @@ -0,0 +1,34 @@ +opam-version: "2.0" +synopsis: "Xml-light bindings for rocq-elpi" +description: "This package provides basic support for reading xml files from Elpi programs running in Rocq" +maintainer: ["Enrico Tassi "] +authors: ["Enrico Tassi "] +license: "LGPL-2.1-or-later" +homepage: "https://github.com/LPCIC/coq-elpi/apps/xml/" +bug-reports: "https://github.com/LPCIC/coq-elpi/issues" +depends: [ + "dune" {>= "3.13" & < "3.24"} + "rocq-elpi" {= "dev"} + "xml-light" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "etc/with-rocq-wrap.sh" {!coq-core:installed} + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" + +url { + src: "git+https://github.com/LPCIC/coq-elpi.git#master" +} diff --git a/extra-dev/packages/rocq-hollight-logic-unif/rocq-hollight-logic-unif.dev/opam b/extra-dev/packages/rocq-hollight-logic-unif/rocq-hollight-logic-unif.dev/opam new file mode 100644 index 0000000000..f4758f8431 --- /dev/null +++ b/extra-dev/packages/rocq-hollight-logic-unif/rocq-hollight-logic-unif.dev/opam @@ -0,0 +1,43 @@ +opam-version: "2.0" +synopsis: "HOL-Light library necessary for translating unify" +description: """ +This library contains an automatic translation in Rocq of a part of the +HOL-Light Logic library using https://github.com/Deducteam/hol2dk. +""" +homepage: "https://github.com/Deducteam/rocq-hollight-logic-unif" +dev-repo: "git+https://github.com/Deducteam/rocq-hollight-logic-unif.git" +bug-reports: "https://github.com/Deducteam/rocq-hollight-logic-unif/issues" +doc: "https://github.com/Deducteam/rocq-hollight-logic-unif" +maintainer: "antoine.gontard@inria.fr" +authors: ["Antoine Gontard"] +license: "CeCILL-2.1" +depends: [ + "rocq-core" {= "dev"} + "coq-mathcomp-classical" {>= "1.14.0"} + # The sources address mathcomp.boot.{choice,ssrbool}, which ships only from + # coq-mathcomp-ssreflect 2.5.0. No coq-mathcomp-classical floor implies that: + # every published classical version, 1.14.0 included, permits ssreflect 2.4.0, + # and rocq-mathcomp-ssreflect.2.4.0 really exists in released/. So the floor + # has to be stated on ssreflect directly. + "coq-mathcomp-ssreflect" {>= "2.5.0"} + "coq-fourcolor-reals" {>= "1.4.2"} + # Require the dev row, do not merely permit it. `>= "0.0.0"` is a floor that + # every version satisfies, and released rocq-mathcomp-hollight-real-with-N.0.0.0 + # depends on nothing tighter than "rocq-prover" {>= "9.0"} -- a floor cannot + # exclude dev, so that row is genuinely selectable here, not merely + # lower-sorting. Only the .dev recipe tracks master alongside this one. + "rocq-mathcomp-hollight-real-with-N" {= "dev"} + "rocq-equations" {>= "1.3.1+9.0"} +] +build: [make "-j%{jobs}%"] +install: [make "install"] +tags: [ + "logpath:HOLLight_Logic_Unif" + "date:2025-10-16" + "keyword:HOL-Light" + "keyword:first order logic" +] + +url { + src: "git+https://github.com/Deducteam/rocq-hollight-logic-unif.git#main" +} diff --git a/extra-dev/packages/rocq-hollight-logic/rocq-hollight-logic.dev/opam b/extra-dev/packages/rocq-hollight-logic/rocq-hollight-logic.dev/opam new file mode 100644 index 0000000000..1f4d572f5c --- /dev/null +++ b/extra-dev/packages/rocq-hollight-logic/rocq-hollight-logic.dev/opam @@ -0,0 +1,69 @@ +opam-version: "2.0" +synopsis: "HOL-Light library necessary for translating unify" +description: """ +This library contains an automatic translation in Rocq of the +HOL-Light Logic library using https://github.com/Deducteam/hol2dk. +""" +homepage: "https://github.com/Deducteam/rocq-hollight-logic" +dev-repo: "git+https://github.com/Deducteam/rocq-hollight-logic.git" +bug-reports: "https://github.com/Deducteam/rocq-hollight-logic/issues" +doc: "https://github.com/Deducteam/rocq-hollight-logic" +maintainer: "antoine.gontard@inria.fr" +authors: ["Antoine Gontard"] +license: "CeCILL-2.1" +depends: [ + "rocq-core" {= "dev"} + "coq-mathcomp-classical" {>= "1.8.0"} + # Same boot floor as rocq-hollight-logic-unif, and for the same reason: no + # coq-mathcomp-classical floor implies mathcomp.boot.*, because every classical + # version permits ssreflect 2.4.0 and that version really exists. + # + # NB this floor is only correct together with the upstream source fix, and this + # row is EXPECTED TO BE RED until Deducteam merges it: #main (881963b) still + # addresses mathcomp.ssreflect.{choice,ssrbool} in terms.v, theorems.v and + # reproduce, i.e. the sources need pre-boot paths while this floor forbids + # pre-boot mathcomp. Measured at dev: mathcomp/ssreflect/ holds only + # all_ssreflect.{v,vo,glob}, so mathcomp.ssreflect.choice has nowhere to resolve + # (mathcomp/boot/choice.vo is where it lives now). + # + # Expect a BUILD failure, not a solve failure. This floor does NOT make the row + # unsatisfiable: coq-mathcomp-classical still admits ssreflect >= 2.5.0 by two + # independent routes, and the >= 1.8.0 dep here reaches both. + # 1.14.0/1.15.0: "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") } + # -- the NUMERIC arm already contains 2.5.0, nothing is killed. + # 1.11.0..1.13.0: numeric arm capped < "2.5~" and so killed, but each carries + # `| (= "dev")`, and dev satisfies >= "2.5.0", so that arm lives. + # Either way the row SOLVES and then fails while compiling: a red with a Rocq + # error, not a clean `not installable` skip. Someone reading the red while + # expecting a skip will conclude the constraint did not take. It did. + "coq-mathcomp-ssreflect" {>= "2.5.0"} + "coq-fourcolor-reals" {>= "1.4.0"} + # Same reasoning as the unif dep below, and the same floor: released + # rocq-mathcomp-hollight-real-with-N.0.0.0's prover dep is the unbounded + # "rocq-prover" {>= "9.0"}, so `>= "0.0.0"` genuinely selects it rather than + # merely ranking it below dev. + "rocq-mathcomp-hollight-real-with-N" {= "dev"} + "rocq-equations" {>= "1.3.1+9.0"} + # Require the dev sibling, do not merely permit it. `>= "0.0.0"` also admits + # released rocq-hollight-logic-unif.0.0.0, whose own prover dep is the + # unbounded floor "rocq-prover" {>= "9.0"} -- and a floor cannot exclude dev, + # so that row is installable here. It is also the WRONG row: 0.0.0 caps + # coq-mathcomp-classical <= "1.13.0", every such classical caps ssreflect + # < "2.5~" in its numeric arm, so the >= "2.5.0" floor above leaves only the + # `| (= "dev")` arm -- i.e. 0.0.0's pre-boot sources compiled against post-boot + # mathcomp, which is exactly the breakage this floor exists to prevent. Only + # the .dev recipe carries the boot floor, so name it. + "rocq-hollight-logic-unif" {= "dev"} +] +build: [make "-j%{jobs}%"] +install: [make "install"] +tags: [ + "logpath:HOLLight_Logic" + "date:2025-10-21" + "keyword:HOL-Light" + "keyword:first order logic" +] + +url { + src: "git+https://github.com/Deducteam/rocq-hollight-logic.git#main" +} diff --git a/extra-dev/packages/rocq-infotheo/rocq-infotheo.dev/opam b/extra-dev/packages/rocq-infotheo/rocq-infotheo.dev/opam new file mode 100644 index 0000000000..8e57b340c6 --- /dev/null +++ b/extra-dev/packages/rocq-infotheo/rocq-infotheo.dev/opam @@ -0,0 +1,95 @@ +# 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: "Reynald Affeldt " + +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" + +synopsis: "Discrete probabilities and information theory for Rocq" +description: """ +Infotheo is a Rocq library for reasoning about discrete probabilities, +information theory, and linear error-correcting codes.""" + +build: [ + [make "-j%{jobs}%" ] + [make "-C" "extraction" "tests"] {with-test} +] +install: [make "install"] +depends: [ + # This is a `.dev` recipe tracking a moving branch, so it has to REQUIRE a dev + # prover, not merely permit one. The line was previously a bare "coq" with no + # constraint at all, which permits every prover in the archive down to 8.0.dev. + # + # A floor on a dependency does not fix that: a dependency's version constrains + # the prover only through whatever that dependency itself declares, and no + # choice of ssreflect forces dev here. All three post-boot arms leave dev + # optional -- + # rocq-mathcomp-boot.2.5.0 ("coq" {>= "8.20" & < "8.21~"} + # | "rocq-core" {>= "9.0" & < "9.2~"}) capped + # rocq-mathcomp-boot.2.6.0 "rocq-core" {>= "9.0"} floor only + # rocq-mathcomp-boot.dev ("coq" {>= "8.20" & < "8.21~"} + # | "rocq-core" {>= "9.0" | = "dev"}) a MENU + # -- and the last is the one that matters: `{>= "9.0" | = "dev"}` names dev as + # one option, and rocq-core.9.1.dev satisfies the other. So even ssreflect.dev + # leaves the row free to solve on 9.1 and go green having exercised no dev at + # all. That is the shape #52's promotion gate exists to catch. + "coq" {= "dev"} + # 2.4.0 is an impossible floor for these sources: 86 of the 87 .v files open + # with `From mathcomp Require Import all_boot`, and 45 also require all_order. + # Those two umbrellas ship from rocq-mathcomp-boot / rocq-mathcomp-order, and + # released/ carries neither package below 2.5.0 -- the only version dirs are + # 2.5.0, 2.6.0 and dev. (mathcomp 2.4.0 does install boot/ and order/ + # directories, so a `test -d` check passes there; both are empty.) + # + # Stating it on ssreflect is sufficient and is the whole fix: 2.5.0 pulls + # rocq-mathcomp-ssreflect {= version}, which pulls rocq-mathcomp-boot and + # rocq-mathcomp-order {= version}. Declaring boot/order here as well would add + # nothing. The sibling 2.4.0 floors below are likewise left alone: at 2.4.0 the + # core stack still locks downward (rocq-mathcomp-algebra {= version} -> + # fingroup -> ssreflect), so raising ssreflect raises all of them. + # + # Latent, not visible today: the solver takes the newest permitted version, so + # it picks 2.6.0/dev and the hole never fires. This is a pre-existing recipe + # bug rather than a port regression -- the constraint is not doing the work, + # the switch is. + "coq-mathcomp-ssreflect" { >= "2.5.0" } + "coq-mathcomp-fingroup" { >= "2.4.0" } + "coq-mathcomp-algebra" { >= "2.4.0" } + "coq-mathcomp-solvable" { >= "2.4.0" } + "coq-mathcomp-field" { (>= "2.4.0") } + "coq-mathcomp-analysis" { (>= "1.12.0") } + "coq-mathcomp-reals-stdlib" { (>= "1.12.0") } + "coq-hierarchy-builder" { (>= "1.10.0") } + "rocq-elpi" { (>= "3.0.0") } + "coq-mathcomp-algebra-tactics" { (>= "1.2.6") } + "coq-interval" { >= "4.10.0"} +] + +tags: [ + "keyword:information theory" + "keyword:probability" + "keyword:error-correcting codes" + "keyword:convexity" + "logpath:infotheo" +] +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" +] + +conflicts: [ "coq-infotheo" { != version } ] + +url { + src: "git+https://github.com/affeldt-aist/infotheo.git#master" +} diff --git a/extra-dev/packages/rocq-laproof/rocq-laproof.dev/opam b/extra-dev/packages/rocq-laproof/rocq-laproof.dev/opam new file mode 100644 index 0000000000..774dd5c86e --- /dev/null +++ b/extra-dev/packages/rocq-laproof/rocq-laproof.dev/opam @@ -0,0 +1,53 @@ +opam-version: "2.0" +synopsis: "LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs" +description: "LAProof is a package of software and Rocq proofs that verify (1) C programs for linear algebra on dense and sparse matrices correctly implement the specified floating-point algorithms; and (2) those floating-point algorithms are accurate within stated concrete bounds." +authors: [ + "Ariel E. Kellison" + "Andrew W. Appel" + "Mohit Tekriwal" + "David Bindel" +] +homepage: "https://github.com/VeriNum/LAProof" +maintainer: "Ariel E. Kellison " +dev-repo: "git+https://github.com/VeriNum/LAProof" +bug-reports: "https://github.com/VeriNum/LAProof/issues" +license: "MIT" + +build: [ + [ make "-j%{jobs}%" ] +] +install: [ + [ make "-j%{jobs}%" "install" ] +] +depends: [ + # Same fix as rocq-infotheo.dev in this series, one shape milder: this line was + # a FLOOR with no ceiling, which permits a dev prover without ever requiring + # one. `>= "9.0"` is satisfied by rocq-core.9.1.dev, a real package core-dev + # builds from a release branch, so the row could green having tested no dev. + # A `.dev` recipe tracking a moving branch has to require dev outright. + # + # The mathcomp floor below cannot substitute for this: no ssreflect version + # forces a dev prover (boot.2.6.0 is a bare floor and boot.dev's rocq-core arm + # is `{>= "9.0" | = "dev"}`, a menu 9.1 satisfies). + "coq" {= "dev"} + "coq-flocq" + "coq-interval" + "coq-vcfloat" {>= "2.4.1~"} + "coq-mathcomp-ssreflect" {>= "2.4.0~"} + "coq-mathcomp-algebra" + "coq-mathcomp-analysis" + "coq-mathcomp-algebra-tactics" + "coq-mathcomp-reals-stdlib" + "coq-mathcomp-finmap" + "coq-vst" {>= "2.16~"} + "coq-vst-lib" {>= "2.15.1~"} + "coq-libvalidsdp" {>= "1.1.1"} +] +tags: [ + "date:2025-05-08" + "logpath:LAProof" +] + +url { + src: "git+https://github.com/VeriNum/LAProof.git#main" +} diff --git a/extra-dev/packages/rocq-marble/rocq-marble.dev/opam b/extra-dev/packages/rocq-marble/rocq-marble.dev/opam new file mode 100644 index 0000000000..73c13dcf92 --- /dev/null +++ b/extra-dev/packages/rocq-marble/rocq-marble.dev/opam @@ -0,0 +1,29 @@ +name: "rocq-marble" +opam-version: "2.0" +synopsis: "Data structures based on machine integers and primitive arrays" +maintainer: "François Pottier " +authors: "François Pottier " +homepage: "https://gitlab.inria.fr/fpottier/marble" +dev-repo: "git+https://gitlab.inria.fr/fpottier/marble/" +bug-reports: "https://gitlab.inria.fr/fpottier/marble/issues" +license: "LGPL-2.1-only" +build: [ + [ "dune" "build" "-p" name "-j" jobs "@install" ] +] +tags: [ + "date:DATEDASH" + "logpath:marble" +] +depends: [ + "rocq-core" {= "dev"} + "rocq-stdlib" {= "dev"} + "rocq-equations" + "rocq-stdpp" { (>= "1.13.0")} + "dune" { >= "3.21" } + "rocq-listz" +] +x-maintenance-intent: ["(latest)"] + +url { + src: "git+https://gitlab.inria.fr/fpottier/marble.git#main" +} diff --git a/extra-dev/packages/rocq-mathcomp-boot/rocq-mathcomp-boot.dev/opam b/extra-dev/packages/rocq-mathcomp-boot/rocq-mathcomp-boot.dev/opam index 09c822553c..439927efac 100644 --- a/extra-dev/packages/rocq-mathcomp-boot/rocq-mathcomp-boot.dev/opam +++ b/extra-dev/packages/rocq-mathcomp-boot/rocq-mathcomp-boot.dev/opam @@ -16,7 +16,11 @@ depends: [ "elpi" {>= "1.17.0"} "rocq-hierarchy-builder" {>= "1.9.0"} ] -conflicts: [ "coq-mathcomp-boot" { != version } ] +conflicts: [ + "coq-mathcomp-boot" { != version } + "rocq-mathcomp-ssreflect" { < "2.5~" } + "coq-mathcomp-ssreflect" { < "2.5~" } +] tags: [ "keyword:small scale reflection" diff --git a/extra-dev/packages/rocq-mathcomp-classical/rocq-mathcomp-classical.dev/opam b/extra-dev/packages/rocq-mathcomp-classical/rocq-mathcomp-classical.dev/opam index 836b7105ee..c8ac60f99b 100644 --- a/extra-dev/packages/rocq-mathcomp-classical/rocq-mathcomp-classical.dev/opam +++ b/extra-dev/packages/rocq-mathcomp-classical/rocq-mathcomp-classical.dev/opam @@ -15,8 +15,17 @@ build: [make "-C" "classical" "-j%{jobs}%"] install: [make "-C" "classical" "install"] depends: [ "rocq-core" {= "dev"} - "rocq-mathcomp-algebra" { (>= "2.6.0" & < "2.7~") } + # Pinned rather than a menu on purpose: rocq-mathcomp-boot 2.6.0 declares + # "rocq-core" {>= "9.0"} with no upper bound, so the dev prover above does + # not on its own exclude released mathcomp. Pinning the library propagates + # through the {= version} locks to order, finite-group and boot. + "rocq-mathcomp-algebra" {= "dev"} + # Left unconstrained on purpose, not by oversight: every published finmap + # permits a dev ssreflect, and the algebra pin above already forces boot to + # dev, so finmap cannot select a released mathcomp here. "rocq-mathcomp-finmap" + # This floor never binds. The lowest published rocq-hierarchy-builder is + # 1.9.0, and rocq-mathcomp-boot requires >= 1.9.0 in any case. "rocq-hierarchy-builder" { (>= "1.8.0") } ] diff --git a/extra-dev/packages/rocq-mathcomp-finmap/rocq-mathcomp-finmap.dev/opam b/extra-dev/packages/rocq-mathcomp-finmap/rocq-mathcomp-finmap.dev/opam index f34a9643f3..9c52b529e9 100644 --- a/extra-dev/packages/rocq-mathcomp-finmap/rocq-mathcomp-finmap.dev/opam +++ b/extra-dev/packages/rocq-mathcomp-finmap/rocq-mathcomp-finmap.dev/opam @@ -17,10 +17,8 @@ which will be used to subsume notations for finite sets, eventually.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - ("coq" {>= "8.20" & < "8.21~"} - | "rocq-core" {>= "9.0"}) - ("coq-mathcomp-ssreflect" { >= "2.2" & < "2.4~" } - |"rocq-mathcomp-ssreflect" { >= "2.4" }) + "rocq-core" {= "dev"} + "rocq-mathcomp-ssreflect" {>= "2.5.0"} ] conflicts: [ "coq-mathcomp-finmap" { != version } ] diff --git a/extra-dev/packages/rocq-mathcomp-hollight-real-with-N/rocq-mathcomp-hollight-real-with-N.dev/opam b/extra-dev/packages/rocq-mathcomp-hollight-real-with-N/rocq-mathcomp-hollight-real-with-N.dev/opam new file mode 100644 index 0000000000..6d6457505d --- /dev/null +++ b/extra-dev/packages/rocq-mathcomp-hollight-real-with-N/rocq-mathcomp-hollight-real-with-N.dev/opam @@ -0,0 +1,30 @@ +opam-version: "2.0" +synopsis: "HOL-Light definition of real numbers in Rocq using N and MathComp" +description: """ +This library contains an automatic translation in Rocq of the HOL-Light +definition of real numbers using https://github.com/Deducteam/hol2dk. +""" +homepage: "https://github.com/Deducteam/mathcomp-hollight-real-with-N" +dev-repo: "git+https://github.com/Deducteam/mathcomp-hollight-real-with-N.git" +bug-reports: "https://github.com/Deducteam/mathcomp-hollight-real-with-N/issues" +doc: "https://github.com/Deducteam/mathcomp-hollight-real-with-N" +maintainer: "frederic.blanqui@inria.fr" +authors: ["https://github.com/Deducteam/mathcomp-hollight-real-with-N/blob/main/AUTHORS.md"] +license: "CeCILL-2.1" +depends: [ + "coq-mathcomp-classical" {>= "1.8.0"} + "rocq-core" {= "dev"} +] +build: [make "-j%{jobs}%"] +install: [make "install"] +tags: [ + "logpath:MathComp_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/mathcomp-hollight-real-with-N.git#main" +} diff --git a/extra-dev/packages/rocq-mathcomp-multinomials/rocq-mathcomp-multinomials.dev/opam b/extra-dev/packages/rocq-mathcomp-multinomials/rocq-mathcomp-multinomials.dev/opam index e851a1b1b6..859857ae5e 100644 --- a/extra-dev/packages/rocq-mathcomp-multinomials/rocq-mathcomp-multinomials.dev/opam +++ b/extra-dev/packages/rocq-mathcomp-multinomials/rocq-mathcomp-multinomials.dev/opam @@ -18,7 +18,7 @@ coefficients range over commutative rings and integral domains.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "rocq-core" {>= "9.0"} + "rocq-core" {= "dev"} "rocq-mathcomp-ssreflect" {>= "2.4"} "rocq-mathcomp-algebra" "coq-mathcomp-bigenough" diff --git a/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam b/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam index ac76d93f8a..aadda046e0 100644 --- a/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam +++ b/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam @@ -18,8 +18,13 @@ build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "rocq-core" {= "dev"} - "rocq-mathcomp-ssreflect" {>= "2.4"} - "rocq-mathcomp-algebra" + # 3 of the 10 .v files require `all_boot`, all under theories/ (polyrcf.v, + # qe_rcf_th.v, realalg.v), which `build: [make]` compiles. That umbrella ships + # from rocq-mathcomp-boot, and no mathcomp below 2.5.0 carries it -- so 2.4 was + # an impossible floor. The bare algebra/field deps below cannot lift it: their + # own dependency on ssreflect is {= version}, which locks downward. + "rocq-mathcomp-ssreflect" {>= "2.5.0"} + "rocq-mathcomp-algebra" "rocq-mathcomp-field" "rocq-mathcomp-bigenough" {>= "1.0.0"} ] diff --git a/extra-dev/packages/rocq-navi/rocq-navi.dev/opam b/extra-dev/packages/rocq-navi/rocq-navi.dev/opam new file mode 100644 index 0000000000..8748fc97a0 --- /dev/null +++ b/extra-dev/packages/rocq-navi/rocq-navi.dev/opam @@ -0,0 +1,39 @@ +opam-version: "2.0" +maintainer: "Yoshihiro Imai" + +homepage: "https://github.com/affeldt-aist/rocqnavi" +dev-repo: "git+https://github.com/yoshihiro503/rocqnavi.git" +bug-reports: "https://github.com/affeldt-aist/rocqnavi/issues" + +license: "GPL-2.0-or-later" +synopsis: "Extension of coq2html Document Generator" + +description: """ +Extension of coq2html Document Generator""" + +build: [make] +install: [make "BINDIR=%{bin}%" "install"] +depends: [ + "ocaml" {>= "4.14"} + "ocamlfind" + "dune-glob" # Parsing glob syntax like "*_unnamed_mixin_*" + "yojson" + "coq-lsp" {with-test} + "rocq-hierarchy-builder" {with-test} +] + +tags: [ + "category:Tools/Document Generator" + "keyword:document" + "keyword:html" + "logpath:" +] +authors: [ + "Xavier Leroy " + "Reynald Affeldt " + "Yoshihiro Imai " +] + +url { + src: "git+https://github.com/affeldt-aist/rocqnavi.git#mca2html" +} diff --git a/extra-dev/packages/rocq-num-analysis-algebra/rocq-num-analysis-algebra.dev/opam b/extra-dev/packages/rocq-num-analysis-algebra/rocq-num-analysis-algebra.dev/opam new file mode 100644 index 0000000000..d61bd82d01 --- /dev/null +++ b/extra-dev/packages/rocq-num-analysis-algebra/rocq-num-analysis-algebra.dev/opam @@ -0,0 +1,74 @@ +opam-version: "2.0" + +name: "rocq-num-analysis-algebra" +synopsis: "Algebraic structures for numerical analysis in Rocq" +description: """ +This library is based on Coquelicot and provides additional support about +commutative monoids, Abelian groups, rings, module spaces, and affine spaces. +This includes support for functions to a given algebraic structure, iterated +operations (sum, linear combination, barycenter), morphisms, algebraic +substructures, and the specific case of finite dimension. +It is based on classical logic. +""" + +homepage: "https://lipn.univ-paris13.fr/rocq-num-analysis/" +dev-repo: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git" +bug-reports: "https://lipn.univ-paris13.fr/rocq-num-analysis/issues" +doc: "https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.2/" +maintainer: "MILC project " +authors: [ + "Sylvie Boldo" + "François Clément" + "Vincent Martin" + "Micaela Mayero" + "Florian Faissole" + "Houda Mouhcine" + "Louise Leclerc" + "Stéphane Aubry" +] +license: "LGPL-3.0-or-later" + +depends: [ + # Copied verbatim from the released 2.2.0 depends:, where both caps are + # correct. On a `.dev` row tracking master they are not: opam sorts `dev` + # above every numeric version, so `< "9.2~"` excludes it while + # rocq-core.9.1.dev sits inside the interval. Do not re-sync this block + # from 2.2.0 -- a released row bounds, a dev row pins. + (("coq-core" {= "dev"} & "coq-stdlib" {= "dev"}) | + ("rocq-core" {= "dev"} & "rocq-stdlib" {= "dev"})) + "coq-coquelicot" {>= "3.4" & < "3.5~"} + "rocq-num-analysis-subset" {= version} +] + +build: [ make "-C" "Algebra" "-j%{jobs}%" ] +install: [ make "-C" "Algebra" "install" ] +remove: [ make "-C" "Algebra" "uninstall" ] + +tags: [ + "category:Mathematics/Algebra" + + "date:2026-03" + + "logpath:NumAnalysis.Algebra" + + "keyword:algebra" + "keyword:algebraic structure hierarchy" + "keyword:functions to an algebraic structure" + "keyword:algebraic substructure" + "keyword:morphism" + "keyword:monoid" + "keyword:group" + "keyword:ring" + "keyword:module space" + "keyword:affine space" + "keyword:dimension theorem" + "keyword:incomplete basis theorem" + "keyword:dual basis" + "keyword:predual basis" + "keyword:rank-nullity theorem" + "keyword:binomial coefficient" +] + +url { + src: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git#master" +} diff --git a/extra-dev/packages/rocq-num-analysis-fem/rocq-num-analysis-fem.dev/opam b/extra-dev/packages/rocq-num-analysis-fem/rocq-num-analysis-fem.dev/opam new file mode 100644 index 0000000000..344c86228a --- /dev/null +++ b/extra-dev/packages/rocq-num-analysis-fem/rocq-num-analysis-fem.dev/opam @@ -0,0 +1,58 @@ +opam-version: "2.0" + +name: "rocq-num-analysis-fem" +synopsis: "The finite element method" +description: """ +This library provides support for finite elements, including the simplicial +Lagrange finite element family. It is based on classical logic. +""" + +homepage: "https://lipn.univ-paris13.fr/rocq-num-analysis/" +dev-repo: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git" +bug-reports: "https://lipn.univ-paris13.fr/rocq-num-analysis/issues" +doc: "https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.2/" +maintainer: "MILC project " +authors: [ + "Sylvie Boldo" + "François Clément" + "Vincent Martin" + "Micaela Mayero" + "Florian Faissole" + "Houda Mouhcine" + "Louise Leclerc" + "Stéphane Aubry" +] +license: "LGPL-3.0-or-later" + +depends: [ + # Copied verbatim from the released 2.2.0 depends:, where both caps are + # correct. On a `.dev` row tracking master they are not: opam sorts `dev` + # above every numeric version, so `< "9.2~"` excludes it while + # rocq-core.9.1.dev sits inside the interval. Do not re-sync this block + # from 2.2.0 -- a released row bounds, a dev row pins. + (("coq-core" {= "dev"} & "coq-stdlib" {= "dev"}) | + ("rocq-core" {= "dev"} & "rocq-stdlib" {= "dev"})) + "rocq-num-analysis-algebra" {= version} +] + +build: [ make "-C" "FEM" "-j%{jobs}%" ] +install: [ make "-C" "FEM" "install" ] +remove: [ make "-C" "FEM" "uninstall" ] + +tags: [ + "category:Mathematics/Real Calculus and Topology" + + "date:2026-03" + + "logpath:NumAnalysis.FEM" + + "keyword:multi-index" + "keyword:multi-variate polynomial" + "keyword:Lagrange polynomial" + "keyword:finite element" + "keyword:simplicial Lagrange finite element" +] + +url { + src: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git#master" +} diff --git a/extra-dev/packages/rocq-num-analysis-lax-milgram/rocq-num-analysis-lax-milgram.dev/opam b/extra-dev/packages/rocq-num-analysis-lax-milgram/rocq-num-analysis-lax-milgram.dev/opam new file mode 100644 index 0000000000..37ed086b32 --- /dev/null +++ b/extra-dev/packages/rocq-num-analysis-lax-milgram/rocq-num-analysis-lax-milgram.dev/opam @@ -0,0 +1,59 @@ +opam-version: "2.0" + +name: "rocq-num-analysis-lax-milgram" +synopsis: "Lax-Milgram theorem" +description: """ +This library provides support for the proof of the Lax-Milgram theorem. +It is based on classical logic. +""" + +homepage: "https://lipn.univ-paris13.fr/rocq-num-analysis/" +dev-repo: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git" +bug-reports: "https://lipn.univ-paris13.fr/rocq-num-analysis/issues" +doc: "https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.2/" +maintainer: "MILC project " +authors: [ + "Sylvie Boldo" + "François Clément" + "Vincent Martin" + "Micaela Mayero" + "Florian Faissole" + "Houda Mouhcine" + "Louise Leclerc" + "Stéphane Aubry" +] +license: "LGPL-3.0-or-later" + +depends: [ + # Copied verbatim from the released 2.2.0 depends:, where both caps are + # correct. On a `.dev` row tracking master they are not: opam sorts `dev` + # above every numeric version, so `< "9.2~"` excludes it while + # rocq-core.9.1.dev sits inside the interval. Do not re-sync this block + # from 2.2.0 -- a released row bounds, a dev row pins. + (("coq-core" {= "dev"} & "coq-stdlib" {= "dev"}) | + ("rocq-core" {= "dev"} & "rocq-stdlib" {= "dev"})) + "rocq-num-analysis-algebra" {= version} +] + +build: [ make "-C" "LM" "-j%{jobs}%" ] +install: [ make "-C" "LM" "install" ] +remove: [ make "-C" "LM" "uninstall" ] + +tags: [ + "category:Mathematics/Real Calculus and Topology" + + "date:2026-03" + + "logpath:NumAnalysis.LM" + + "keyword:fixed point theorem (in a Banach space)" + "keyword:orthogonal projection" + "keyword:orthogonal complement" + "keyword:Riesz-Fréchet representation theorem" + "keyword:Lax-Milgram theorem" + "keyword:Céa's lemma" +] + +url { + src: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git#master" +} diff --git a/extra-dev/packages/rocq-num-analysis-lebesgue/rocq-num-analysis-lebesgue.dev/opam b/extra-dev/packages/rocq-num-analysis-lebesgue/rocq-num-analysis-lebesgue.dev/opam new file mode 100644 index 0000000000..3fb2b7d285 --- /dev/null +++ b/extra-dev/packages/rocq-num-analysis-lebesgue/rocq-num-analysis-lebesgue.dev/opam @@ -0,0 +1,69 @@ +opam-version: "2.0" + +name: "rocq-num-analysis-lebesgue" +synopsis: "Lebesgue integral" +description: """ +This library provides support for the Lebesgue integral of nonnegative +measurable functions, and for the Bochner integral for functions to a Banach +space. It is based on classical logic. +""" + +homepage: "https://lipn.univ-paris13.fr/rocq-num-analysis/" +dev-repo: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git" +bug-reports: "https://lipn.univ-paris13.fr/rocq-num-analysis/issues" +doc: "https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.2/" +maintainer: "MILC project " +authors: [ + "Sylvie Boldo" + "François Clément" + "Vincent Martin" + "Micaela Mayero" + "Florian Faissole" + "Houda Mouhcine" + "Louise Leclerc" + "Stéphane Aubry" +] +license: "LGPL-3.0-or-later" + +depends: [ + # Copied verbatim from the released 2.2.0 depends:, where both caps are + # correct. On a `.dev` row tracking master they are not: opam sorts `dev` + # above every numeric version, so `< "9.2~"` excludes it while + # rocq-core.9.1.dev sits inside the interval. Do not re-sync this block + # from 2.2.0 -- a released row bounds, a dev row pins. + (("coq-core" {= "dev"} & "coq-stdlib" {= "dev"}) | + ("rocq-core" {= "dev"} & "rocq-stdlib" {= "dev"})) + "coq-coquelicot" {>= "3.4" & < "3.5~"} + "coq-flocq" {>= "4.2" & < "4.3~"} + "rocq-num-analysis-subset" {= version} +] + +build: [ make "-C" "Lebesgue" "-j%{jobs}%" ] +install: [ make "-C" "Lebesgue" "install" ] +remove: [ make "-C" "Lebesgue" "uninstall" ] + +tags: [ + "category:Mathematics/Real Calculus and Topology" + + "date:2026-03" + + "logpath:NumAnalysis.Lebesgue" + + "keyword:sigma-algebra" + "keyword:monotone class theorem" + "keyword:Dynkin pi-lambda theorem" + "keyword:measure theory" + "keyword:Lebesgue measure" + "keyword:simple function" + "keyword:adapted sequence" + "keyword:Beppo Levi (monotone convergence) theorem" + "keyword:Fatou lemma" + "keyword:Lebesgue (dominated convergence) theorem" + "keyword:Lebesgue induction principle" + "keyword:Tonelli theorem" + "keyword:Bochner integral" +] + +url { + src: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git#master" +} diff --git a/extra-dev/packages/rocq-num-analysis-subset/rocq-num-analysis-subset.dev/opam b/extra-dev/packages/rocq-num-analysis-subset/rocq-num-analysis-subset.dev/opam new file mode 100644 index 0000000000..8af1fde900 --- /dev/null +++ b/extra-dev/packages/rocq-num-analysis-subset/rocq-num-analysis-subset.dev/opam @@ -0,0 +1,62 @@ +opam-version: "2.0" + +name: "rocq-num-analysis-subset" +synopsis: "Subsets for numerical analysis in Rocq" +description: """ +This library provides support about subsets, functions, homogeneous binary +relations, and finite families. It is based on classical logic. +Some complements about logic and natural numbers are also provided. +""" + +homepage: "https://lipn.univ-paris13.fr/rocq-num-analysis/" +dev-repo: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git" +bug-reports: "https://lipn.univ-paris13.fr/rocq-num-analysis/issues" +doc: "https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.2/" +maintainer: "MILC project " +authors: [ + "Sylvie Boldo" + "François Clément" + "Vincent Martin" + "Micaela Mayero" + "Florian Faissole" + "Houda Mouhcine" + "Louise Leclerc" + "Stéphane Aubry" +] +license: "LGPL-3.0-or-later" + +depends: [ + # Copied verbatim from the released 2.2.0 depends:, where both caps are + # correct. On a `.dev` row tracking master they are not: opam sorts `dev` + # above every numeric version, so `< "9.2~"` excludes it while + # rocq-core.9.1.dev sits inside the interval. Do not re-sync this block + # from 2.2.0 -- a released row bounds, a dev row pins. + (("coq-core" {= "dev"} & "coq-stdlib" {= "dev"}) | + ("rocq-core" {= "dev"} & "rocq-stdlib" {= "dev"})) + "coq-mathcomp-ssreflect" {>= "2.3" & < "2.6~"} + "coq-mathcomp-classical" {>= "1.8" & < "1.15~"} +] + +build: [ make "-C" "Subset" "-j%{jobs}%" ] +install: [ make "-C" "Subset" "install" ] +remove: [ make "-C" "Subset" "uninstall" ] + +tags: [ + "category:Mathematics/Logic/Set theory" + + "date:2026-03" + + "logpath:NumAnalysis.Requisite" + "logpath:NumAnalysis.Logic" + "logpath:NumAnalysis.Numbers" + "logpath:NumAnalysis.Subsets" + + "keyword:subset" + "keyword:function" + "keyword:homogeneous binary relation" + "keyword:operation on finite families" +] + +url { + src: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git#master" +} diff --git a/extra-dev/packages/rocq-num-analysis/rocq-num-analysis.dev/opam b/extra-dev/packages/rocq-num-analysis/rocq-num-analysis.dev/opam new file mode 100644 index 0000000000..d60cc6195b --- /dev/null +++ b/extra-dev/packages/rocq-num-analysis/rocq-num-analysis.dev/opam @@ -0,0 +1,35 @@ +opam-version: "2.0" + +name: "rocq-num-analysis" +synopsis: "Numerical analysis in Rocq" +description: """ +Meta-package grouping rocq-num-analysis-lebesgue, +rocq-num-analysis-lax-milgram and rocq-num-analysis-fem. +""" + +homepage: "https://lipn.univ-paris13.fr/rocq-num-analysis/" +dev-repo: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git" +bug-reports: "https://lipn.univ-paris13.fr/rocq-num-analysis/issues" +doc: "https://lipn.univ-paris13.fr/rocqdoc-num-analysis/2.2/" +maintainer: "MILC project " +authors: [ + "Sylvie Boldo" + "François Clément" + "Vincent Martin" + "Micaela Mayero" + "Florian Faissole" + "Houda Mouhcine" + "Louise Leclerc" + "Stéphane Aubry" +] +license: "LGPL-3.0-or-later" + +depends: [ + "rocq-num-analysis-lebesgue" {= version} + "rocq-num-analysis-lax-milgram" {= version} + "rocq-num-analysis-fem" {= version} +] + +url { + src: "git+https://depot.lipn.univ-paris13.fr/mayero/rocq-num-analysis.git#master" +} diff --git a/extra-dev/packages/rocq-partial-orders/rocq-partial-orders.dev/opam b/extra-dev/packages/rocq-partial-orders/rocq-partial-orders.dev/opam new file mode 100644 index 0000000000..8a7facaa08 --- /dev/null +++ b/extra-dev/packages/rocq-partial-orders/rocq-partial-orders.dev/opam @@ -0,0 +1,43 @@ +opam-version: "2.0" +maintainer: "Damien Pous " + +homepage: "https://github.com/damien-pous/partial-orders" +dev-repo: "git+https://github.com/damien-pous/partial-orders.git" +bug-reports: "https://github.com/damien-pous/partial-orders/issues" +license: "LGPL-3.0-or-later" + +synopsis: "A library for setoids, partial orders, complete lattices and related structures" +description: """ +Library about partial orders with more or less infimas and suprema (semi-lattices, lattices, complete partial orders, complete lattices). Duality, fixpoint theorems (BourbakiWitt, Pataraia), instances (notably, various function spaces), adjunctions/Galois connections. +Hierarchy of structures implemented with Hierarchy Builder. +Based on setoids from the beginning, as a convenient way to obtain axiom-free quotients. +""" + +build: [ + [make "-j%{jobs}%" ] +] +install: [make "install"] +depends: [ + "rocq-core" {= "dev"} + "rocq-stdlib" {= "dev"} + "rocq-mathcomp-ssreflect" + "rocq-hierarchy-builder" +] + +tags: [ + "keyword:partial order" + "keyword:setoid" + "keyword:lattice" + "keyword:CPO" + "keyword:Pataraia" + "keyword:BourbakiWitt" + "logpath:PartialOrders" + "date:2026-05-07" +] +authors: [ + "Damien Pous " +] + +url { + src: "git+https://github.com/damien-pous/partial-orders.git#main" +} diff --git a/extra-dev/packages/rocq-pil/rocq-pil.dev/opam b/extra-dev/packages/rocq-pil/rocq-pil.dev/opam new file mode 100644 index 0000000000..43f2bf95db --- /dev/null +++ b/extra-dev/packages/rocq-pil/rocq-pil.dev/opam @@ -0,0 +1,45 @@ +opam-version: "2.0" +synopsis: "Rocq library for Propositional Intuitionistic Logic & Pitts Interpolation Library" + +homepage: "https://github.com/hferee/rocq-pil" +dev-repo: "git+https://github.com/hferee/rocq-pil.git" +bug-reports: "https://github.com/hferee/rocq-pil/issues" +doc: "https://hferee.github.io/UIML" +maintainer: "feree@irif.fr" +authors: [ + "Hugo Férée" + "Sam van Gool" + "Yago Iglesias Vasquez" +] +license: "CECILL-2.1" + +depends: [ + "dune" {>= "3.8"} + "rocq-core" {= "dev"} + "rocq-stdpp" {>= "1.13.0"} + "rocq-equations" {} +] + +build: [ + [make "-j%{jobs}%"] +] +install: [ + [make "install"] +] + +tags: [ + "date:2025-02-14" + "keyword:intuitionistic logic" + "keyword:proof theory" + "keyword:propositional quantifiers" + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "category:Mathematics/Logic/Foundations" + "category:Mathematics/Logic/Modal logic" + "logpath:ISL" +] + +conflicts: [ "coq-pil" { != version } ] + +url { + src: "git+https://github.com/hferee/rocq-pil.git#main" +} diff --git a/extra-dev/packages/rocq-robot-rocq/rocq-robot-rocq.dev/opam b/extra-dev/packages/rocq-robot-rocq/rocq-robot-rocq.dev/opam new file mode 100644 index 0000000000..77d780865e --- /dev/null +++ b/extra-dev/packages/rocq-robot-rocq/rocq-robot-rocq.dev/opam @@ -0,0 +1,45 @@ +# 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: "Reynald Affeldt " + +homepage: "https://github.com/affeldt-aist/robot-rocq" +dev-repo: "git+https://github.com/affeldt-aist/robot-rocq.git" +bug-reports: "https://github.com/affeldt-aist/robot-rocq/issues" +license: "LGPL-2.1-or-later" + +synopsis: "Formal Foundations for Modeling Robot Manipulators" +description: """ +This repository contains an experimental library for the mathematics +of rigid body transformations using the Rocq proof-assistant and the +Mathematical Components library.""" + +build: [make "-j%{jobs}%" ] +install: [make "install"] +depends: [ + "coq" { = "dev" } + "rocq-hierarchy-builder" { = "dev" } + "rocq-mathcomp-ssreflect" { = "dev" } + "rocq-mathcomp-fingroup" { = "dev" } + "rocq-mathcomp-algebra" { = "dev" } + "rocq-mathcomp-solvable" { = "dev" } + "rocq-mathcomp-field" { = "dev" } + "rocq-mathcomp-analysis" { = "dev" } + "rocq-mathcomp-real-closed" { = "dev" } +] + +tags: [ + "keyword:robotics" + "keyword:3D geometry" + "logpath:robot" +] +authors: [ + "Reynald Affeldt, AIST" + "Cyril Cohen, Inria" + "Laurent Théry, Inria" +] + +url { + src: "git+https://github.com/affeldt-aist/robot-rocq.git#master" +} diff --git a/extra-dev/packages/rocq-rouche-capelli/rocq-rouche-capelli.dev/opam b/extra-dev/packages/rocq-rouche-capelli/rocq-rouche-capelli.dev/opam new file mode 100644 index 0000000000..be1df11192 --- /dev/null +++ b/extra-dev/packages/rocq-rouche-capelli/rocq-rouche-capelli.dev/opam @@ -0,0 +1,48 @@ +opam-version: "2.0" +name: "rocq-rouche-capelli" +synopsis: "A proof for the Rouché–Capelli theorem by rocq-math-comp" +description: """ +This package provides a formal proof of the Rouché–Capelli theorem (also known as +the Kronecker–Capelli theorem) using the Rocq Prover and the Mathematical Components +library. The theorem provides necessary and sufficient conditions for a system of +linear equations to have solutions, stating that a system is consistent if and only +if the rank of its coefficient matrix equals the rank of its augmented matrix. +""" +maintainer: "Chenghui Weng <144981080+weng-chenghui@users.noreply.github.com>" +authors: [ + "Cheng-Hui Weng" + "Reynald Affeldt" + "Jacques Garrigue" + "Takafumi Saikawa" +] +license: "MIT" +homepage: "https://github.com/weng-chenghui/rocq-rouche-capelli" +bug-reports: "https://github.com/weng-chenghui/rocq-rouche-capelli/issues" +dev-repo: "git+https://github.com/weng-chenghui/rocq-rouche-capelli.git" +tags: [ + "category:Mathematics/Algebra" + "keyword:linear algebra" + "keyword:matrix" + "keyword:rank" + "logpath:RoucheCapelli" +] +depends: [ + "ocaml" {>= "4.14.0"} + "rocq-core" {= "dev"} + "rocq-mathcomp-ssreflect" {= "dev"} + "rocq-mathcomp-algebra" {= "dev"} + "rocq-mathcomp-field" {= "dev"} + "rocq-mathcomp-fingroup" {= "dev"} + "rocq-mathcomp-solvable" {= "dev"} +] +build: [ + ["rocq" "makefile" "-f" "_CoqProject" "-o" "Makefile.coq"] + ["%{make}%" "-f" "Makefile.coq" "-j%{jobs}%"] +] +install: [ + ["%{make}%" "-f" "Makefile.coq" "install"] +] + +url { + src: "git+https://github.com/weng-chenghui/rocq-rouche-capelli.git#main" +} diff --git a/extra-dev/packages/rocq-rust-extraction/rocq-rust-extraction.dev/opam b/extra-dev/packages/rocq-rust-extraction/rocq-rust-extraction.dev/opam new file mode 100644 index 0000000000..a3b17ba220 --- /dev/null +++ b/extra-dev/packages/rocq-rust-extraction/rocq-rust-extraction.dev/opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +name: "rocq-rust-extraction" +synopsis: "Rocq extraction to Rust" +description: """ +A framework for extracting Rocq programs to Rust +""" +maintainer: "Danil Annenkov " +authors: "The COBRA team" +license: "MIT" +homepage: "https://github.com/peregrine-project/rocq-typed-extraction" +dev-repo: "git+https://github.com/peregrine-project/rocq-typed-extraction.git" +bug-reports: "https://github.com/peregrine-project/rocq-typed-extraction/issues" +doc: "https://peregrine-project.github.io/rocq-typed-extraction/toc.html" + +depends: [ + "rocq-typed-extraction-common" {= version} +] + +build: [ + ["bash" "./configure.sh"] + [make "-j" "%{jobs}%" "-C" "rust"] +] + +install: [ + [make "-C" "rust" "install"] +] + +tags: [ + "keyword:rust" + "keyword:extraction" + "logpath:TypedExtraction" +] + +url { + src: "git+https://github.com/peregrine-project/rocq-typed-extraction.git#master" +} diff --git a/extra-dev/packages/rocq-sims/rocq-sims.dev/opam b/extra-dev/packages/rocq-sims/rocq-sims.dev/opam new file mode 100644 index 0000000000..a794f4219a --- /dev/null +++ b/extra-dev/packages/rocq-sims/rocq-sims.dev/opam @@ -0,0 +1,41 @@ +opam-version: "2.0" +synopsis: "A library of various strong and weak simulation relations" +maintainer: ["Nicolas Chappe"] +authors: ["Nicolas Chappe"] +license: "LGPL-3.0-or-later" +tags: [ + "category:Computer Science/Semantics and Compilation/Semantics" + "category:Computer Science/Semantics and Compilation/Compilation" + "keyword:simulation" + "keyword:coinduction up-to" + "logpath:Sims" +] +homepage: "https://github.com/rocq-sims/rocq-sims" +bug-reports: "https://github.com/rocq-sims/rocq-sims/issues" +depends: [ + "dune" {>= "3.8"} + "coq" {= "dev"} + "coq-coinduction" {>= "1.9"} + "coq-relation-algebra" {>= "1.7"} + "coq-ctree" {>= "2.0"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/rocq-sims/rocq-sims.git" + +url { + src: "git+https://github.com/rocq-sims/rocq-sims.git#main" +} diff --git a/extra-dev/packages/rocq-ssprove/rocq-ssprove.dev/opam b/extra-dev/packages/rocq-ssprove/rocq-ssprove.dev/opam new file mode 100644 index 0000000000..fd2b90be25 --- /dev/null +++ b/extra-dev/packages/rocq-ssprove/rocq-ssprove.dev/opam @@ -0,0 +1,37 @@ +opam-version: "2.0" +name: "rocq-ssprove" +synopsis: "A Foundational Framework for Modular Cryptographic Proofs" +maintainer: "philipp@haselwarter.org" +authors: ["SSProve team"] +homepage: "https://github.com/SSProve/ssprove" +bug-reports: "https://github.com/SSProve/ssprove/issues" +dev-repo: "git+https://github.com/SSProve/ssprove.git" +doc: "https://SSProve.github.io/ssprove/index.html" +license: "MIT" +depends: [ + "rocq-core" {>= "9.0"} + "rocq-stdlib" {>= "9.0"} + "rocq-equations" {(>= "1.3.1+9.0")} + "coq-mathcomp-ssreflect" {(>= "2.3.0")} + "coq-mathcomp-analysis" {>= "1.8.0"} + "coq-mathcomp-experimental-reals" {>= "1.8.0"} + "coq-mathcomp-word" {>= "3.3" & < "3.5"} + "coq-extructures" {(>= "0.5.0" & < "dev")} + "coq-deriving" {(>= "0.2.1" & < "dev")} +] +build: [ + [make "-j%{jobs}%"] +] +install: [ + [make "install"] +] +tags: [ + "keyword:cryptography" + "logpath:SSProve" +] + +conflicts: [ "coq-ssprove" { != version } ] + +url { + src: "git+https://github.com/SSProve/ssprove.git#main" +} diff --git a/extra-dev/packages/rocq-stdpp/rocq-stdpp.dev/opam b/extra-dev/packages/rocq-stdpp/rocq-stdpp.dev/opam new file mode 100644 index 0000000000..613b8bc54e --- /dev/null +++ b/extra-dev/packages/rocq-stdpp/rocq-stdpp.dev/opam @@ -0,0 +1,59 @@ +opam-version: "2.0" +maintainer: "Ralf Jung " +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 Rocq" +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: [ + # Upstream's own rocq-stdpp.opam writes both of these as menus, + # `{(>= "9.0" & < "9.4~") | (= "dev")}`, which permits a dev prover without + # ever requiring one -- the same shape #59 fixed on rocq-infotheo.dev and + # rocq-laproof.dev. A `.dev` row tracking a moving branch has to require dev + # outright, so both are tightened here. + "rocq-core" {= "dev"} + "rocq-stdlib" {= "dev"} +] +conflicts: [ + # Kept unversioned, exactly as upstream writes it on rocq-stdpp.1.13.0 and on + # their own rocq-stdpp.dev.*. Older upstream revisions used a versioned + # `{< "dev.2025-08-02.1"}` here, which deliberately let a coq-stdpp + # compatibility shim co-install; upstream stopped publishing that shim in + # August 2025 and widened the conflict to retire the coq- name. Do not narrow + # this to admit a coq-stdpp.dev without deciding that question first -- see + # the notes on task #79. + "coq-stdpp" +] + +build: ["./make-package" "stdpp" "-j%{jobs}%"] +install: ["./make-package" "stdpp" "install"] + +url { + src: "git+https://github.com/rocq-iris/stdpp.git#master" +} diff --git a/extra-dev/packages/rocq-typed-extraction-plugin/rocq-typed-extraction-plugin.dev/opam b/extra-dev/packages/rocq-typed-extraction-plugin/rocq-typed-extraction-plugin.dev/opam new file mode 100644 index 0000000000..835cbfc1ef --- /dev/null +++ b/extra-dev/packages/rocq-typed-extraction-plugin/rocq-typed-extraction-plugin.dev/opam @@ -0,0 +1,36 @@ +opam-version: "2.0" +name: "rocq-typed-extraction-plugin" +synopsis: "Rocq extraction to Rust and Elm" +description: """ +A framework for extracting Rocq programs to Rust and Elm +""" +maintainer: "Danil Annenkov " +authors: "The COBRA team" +license: "MIT" +homepage: "https://github.com/peregrine-project/rocq-typed-extraction" +dev-repo: "git+https://github.com/peregrine-project/rocq-typed-extraction.git" +bug-reports: "https://github.com/peregrine-project/rocq-typed-extraction/issues" +doc: "https://peregrine-project.github.io/rocq-typed-extraction/toc.html" + +depends: [ + "rocq-elm-extraction" {= version} + "rocq-rust-extraction" {= version} +] + +build: [ + ["bash" "./configure.sh"] + [make "-j" "%{jobs}%" "-C" "plugin"] +] + +install: [ + [make "-C" "plugin" "install"] +] + +tags: [ + "keyword:extraction" + "logpath:TypedExtraction" +] + +url { + src: "git+https://github.com/peregrine-project/rocq-typed-extraction.git#master" +} diff --git a/extra-dev/packages/rocq-typed-extraction/rocq-typed-extraction.dev/opam b/extra-dev/packages/rocq-typed-extraction/rocq-typed-extraction.dev/opam new file mode 100644 index 0000000000..408ac211bd --- /dev/null +++ b/extra-dev/packages/rocq-typed-extraction/rocq-typed-extraction.dev/opam @@ -0,0 +1,28 @@ +opam-version: "2.0" +name: "rocq-typed-extraction" +synopsis: "Rocq extraction to Rust and Elm" +description: """ +A framework for extracting Rocq programs to Rust and Elm +""" +maintainer: "Danil Annenkov " +authors: "The COBRA team" +license: "MIT" +homepage: "https://github.com/peregrine-project/rocq-typed-extraction" +dev-repo: "git+https://github.com/peregrine-project/rocq-typed-extraction.git" +bug-reports: "https://github.com/peregrine-project/rocq-typed-extraction/issues" +doc: "https://peregrine-project.github.io/rocq-typed-extraction/toc.html" + +depends: [ + "rocq-elm-extraction" {= version} + "rocq-rust-extraction" {= version} + "rocq-typed-extraction-plugin" {= version} +] + +tags: [ + "keyword:extraction" + "logpath:TypedExtraction" +] + +url { + src: "git+https://github.com/peregrine-project/rocq-typed-extraction.git#master" +}