Skip to content
@coq-community

coq-community

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

Pinned Loading

  1. manifesto manifesto Public

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

    68 6

  2. hydra-battles hydra-battles Public

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

    Coq 72 12

  3. awesome-coq awesome-coq Public

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

    338 20

  4. docker-coq 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 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
  • coq-nix-toolbox Public

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

    coq-community/coq-nix-toolbox’s past year of commit activity
    Nix 37 MIT 12 29 (1 issue needs help) 4 Updated Feb 20, 2025
  • fourcolor Public

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

    coq-community/fourcolor’s past year of commit activity
    Coq 191 22 0 3 Updated Feb 20, 2025
  • aac-tactics Public

    Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

    coq-community/aac-tactics’s past year of commit activity
    OCaml 31 21 3 1 Updated Feb 19, 2025
  • coq-dpdgraph Public

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

    coq-community/coq-dpdgraph’s past year of commit activity
    Coq 89 LGPL-2.1 29 9 9 Updated Feb 19, 2025
  • coq-community/rocq-lean-import’s past year of commit activity
    OCaml 17 LGPL-2.1 5 1 0 Updated Feb 19, 2025
  • coqeal Public

    The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

    coq-community/coqeal’s past year of commit activity
    Coq 69 17 6 3 Updated Feb 18, 2025
  • run-coq-bug-minimizer Public

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

    coq-community/run-coq-bug-minimizer’s past year of commit activity
    Shell 2 MIT 0 8 1 Updated Feb 17, 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-community/tarjan’s past year of commit activity
    Coq 14 8 0 1 Updated Feb 16, 2025
  • gaia Public

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

    coq-community/gaia’s past year of commit activity
    Coq 30 MIT 7 0 0 Updated Feb 16, 2025
  • reglang Public

    Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

    coq-community/reglang’s past year of commit activity
    Coq 41 7 1 0 Updated Feb 16, 2025