Skip to content
@rocq-community

Rocq-community

A project for a collaborative, community-driven effort for the long-term maintenance and advertisement of packages for the Rocq Prover

Pinned Loading

  1. manifesto Public

    Documentation on goals of the Rocq-community organization, the shared contributing guide and code of conduct.

    68 6

  2. hydra-battles Public

    Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

    Coq 74 12

  3. awesome-coq Public

    A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

    345 20

  4. docker-coq Public

    Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]

    Dockerfile 37 3

  5. templates Public

    Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@liyishuai,@palmskog,@Zimmi48]

    Mustache 13 9

Repositories

Showing 10 of 75 repositories
  • manifesto Public

    Documentation on goals of the Rocq-community organization, the shared contributing guide and code of conduct.

    68 6 37 1 Updated Mar 28, 2025
  • lemma-overloading Public

    Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]

    Coq 27 6 3 1 Updated Mar 28, 2025
  • coq-nix-toolbox Public

    Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]

    Nix 38 MIT 12 29 (1 issue needs help) 3 Updated Mar 27, 2025
  • coq-dpdgraph Public

    Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

    Coq 89 LGPL-2.1 29 9 9 Updated Mar 27, 2025
  • rocq-community.github.io Public

    Rocq-community website

    HTML 0 CC0-1.0 0 0 0 Updated Mar 27, 2025
  • run-coq-bug-minimizer Public

    Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]

    Shell 2 MIT 0 8 0 Updated Mar 27, 2025
  • apery Public

    A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]

    Coq 23 7 5 0 Updated Mar 25, 2025
  • gaia Public

    Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

    Coq 30 MIT 7 0 0 Updated Mar 25, 2025
  • fourcolor Public

    Formal proof of the Four Color Theorem [maintainer=@ybertot]

    Coq 201 22 0 3 Updated Mar 25, 2025
  • docker-coq-action Public

    GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]

    Shell 12 MIT 4 21 (2 issues need help) 2 Updated Mar 23, 2025

Top languages

Loading…

Most used topics

Loading…