Rocq-community

All

75 repositories

run-coq-bug-minimizer
Public
Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
Shell
•
MIT License
•0•2•9•0•Updated Jul 23, 2025Jul 23, 2025
parseque
Public
Total Parser Combinators in Coq [maintainer=@womeier]
parser-combinators coq
Rocq Prover
•
MIT License
•6•45•2•0•Updated Jul 19, 2025Jul 19, 2025
bignums
Public
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
large-numbers coq-plugin docker-coq-action coq-ci coq-platform coq
Rocq Prover
•
GNU Lesser General Public License v2.1
•22•24•1•2•Updated Jul 18, 2025Jul 18, 2025
corn
Public
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
coq coq-library real-number coq-ci coq-platform
Rocq Prover
•
GNU General Public License v2.0
•47•115•8•1•Updated Jul 18, 2025Jul 18, 2025
math-classes
Public
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
coq mathematics typeclasses coq-library coq-ci coq-platform
Rocq Prover
•
MIT License
•43•166•10•1•Updated Jul 18, 2025Jul 18, 2025
coq-nix-toolbox
Public
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
coq nix
Nix
•
MIT License
•17•43•30•6•Updated Jul 17, 2025Jul 17, 2025
fourcolor
Public
Formal proof of the Four Color Theorem [maintainer=@ybertot]
ssreflect four-color-theorem mathcomp coq-ci coq
Rocq Prover
•
Other
•23•214•0•2•Updated Jul 5, 2025Jul 5, 2025
trocq
Public
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
coq parametricity
Rocq Prover
•
GNU Lesser General Public License v3.0
•9•23•15•4•Updated Jul 1, 2025Jul 1, 2025
graph-theory
Public
Graph Theory [maintainers=@chdoc,@damien-pous]
coq graph-theory mathcomp docker-coq-action mathcomp-ci
Rocq Prover
•4•37•2•1•Updated Jun 27, 2025Jun 27, 2025
apery
Public
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
ssreflect mathcomp coq
Rocq Prover
•
Other
•7•24•5•0•Updated Jun 27, 2025Jun 27, 2025
gaia
Public
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
coq set-theory ssreflect mathcomp docker-coq-action bourbaki mathcomp-ci
Rocq Prover
•
MIT License
•7•30•0•1•Updated Jun 27, 2025Jun 27, 2025
coqeal
Public
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
coq refinement mathcomp coq-ci coq-platform mathcomp-ci
Rocq Prover
•
Other
•17•71•6•3•Updated Jun 27, 2025Jun 27, 2025
coq-100-theorems
Public
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
coq theorems
HTML
•
Other
•14•60•2•1•Updated Jun 23, 2025Jun 23, 2025
docker-base
Public
Parent image for Docker images of the Coq proof assistant [maintainers=@erikmd,@himito]
coq docker-coq
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•4•4•1•1•Updated Jun 23, 2025Jun 23, 2025
templates
Public
Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@liyishuai,@palmskog,@Zimmi48]
continuous-integration coq mustache-templates
Mustache
•
The Unlicense
•9•15•22•3•Updated Jun 19, 2025Jun 19, 2025
tarjan
Public
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]
coq tarjan-algorithm ssreflect mathcomp mathcomp-ci
Rocq Prover
•
Other
•8•17•0•0•Updated Jun 17, 2025Jun 17, 2025
rocq-lean-import
Public
OCaml
•
GNU Lesser General Public License v2.1
•7•24•4•0•Updated Jun 16, 2025Jun 16, 2025
docker-rocq
Public
Docker images of the Rocq Prover (see also: https://github.com/rocq-community/docker-coq-action) [maintainers=@erikmd,@himito]
Dockerfile
•
MIT License
•0•1•4•0•Updated Jun 12, 2025Jun 12, 2025
aac-tactics
Public
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
coq coq-plugin coq-tactic docker-coq-action nix-action coq-ci coq-platform
OCaml
•
Other
•23•32•3•3•Updated Jun 4, 2025Jun 4, 2025
coq-dpdgraph
Public
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
dependency-analysis dependency-graph docker-coq-action coq-ci coq-platform coq
Coq
•
GNU Lesser General Public License v2.1
•30•90•9•10•Updated Jun 2, 2025Jun 2, 2025
coq-performance-tests-plots-history
Public
Maintaining plot history for coq-community/coq-performance-tests gh-pages branch [maintainer=@JasonGross]
0•0•1•0•Updated Jun 1, 2025Jun 1, 2025
coq-performance-tests
Public
A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]
testing performance coq
Coq
•
MIT License
•7•7•1•2•Updated Jun 1, 2025Jun 1, 2025
rocq-tricks
Public
Tricks you wish the Coq manual told you [maintainer=@tchajed]
coq
Coq
•
MIT License
•24•523•6•1•Updated May 28, 2025May 28, 2025
docker-coq
Public
Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]
ci coq opam docker-coq dockerfile docker-image
Shell
•
BSD 3-Clause "New" or "Revised" License
•3•39•7•0•Updated May 13, 2025May 13, 2025
bits
Public
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
bitset coq-library ssreflect paper-artifacts coq-extraction coq mathcomp
Coq
•
Apache License 2.0
•7•23•3•0•Updated May 1, 2025May 1, 2025
reglang
Public
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
regexp coq regular-languages ssreflect mathcomp docker-coq-action coq-nix-toolbox coq-platform mathcomp-ci
Coq
•
Other
•7•44•1•0•Updated Apr 23, 2025Apr 23, 2025
paramcoq
Public
Old Coq plugin for parametricity [maintainer=@ppedrot]
coq coq-plugin parametricity docker-coq-action coq-ci coq-platform
Coq
•
Other
•25•45•6•1•Updated Apr 18, 2025Apr 18, 2025
manifesto
Public
Documentation on goals of the Rocq-community organization, the shared contributing guide and code of conduct.
coq manifesto community-driven
Other
•6•68•37•0•Updated Mar 31, 2025Mar 31, 2025
lemma-overloading
Public
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
automation coq typeclasses ssreflect paper-artifacts canonical-structures mathcomp
Coq
•
Other
•6•27•3•1•Updated Mar 28, 2025Mar 28, 2025
rocq-community.github.io
Public
Rocq-community website
website coq rocq-prover
HTML
•
Creative Commons Zero v1.0 Universal
•1•1•1•0•Updated Mar 27, 2025Mar 27, 2025