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 60 12

  3. awesome-coq awesome-coq Public

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

    296 18

  4. vscoq vscoq Public

    A Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]

    OCaml 317 66

  5. 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 36 3

  6. templates templates Public

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

    Mustache 12 8

Repositories

Showing 10 of 71 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 31 MIT 9 28 (1 issue needs help) 5 Updated Jun 30, 2024
  • atbr Public

    Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]

    coq-community/atbr’s past year of commit activity
    Coq 23 5 0 0 Updated Jun 30, 2024
  • stalmarck Public

    Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]

    coq-community/stalmarck’s past year of commit activity
    Coq 1 LGPL-2.1 3 0 0 Updated Jun 30, 2024
  • 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 7 0 Updated Jun 30, 2024
  • 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 29 21 2 1 Updated Jun 29, 2024
  • apery Public

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

    coq-community/apery’s past year of commit activity
    Coq 19 5 4 0 Updated Jun 29, 2024
  • graph-theory Public

    Graph Theory [maintainers=@chdoc,@damien-pous]

    coq-community/graph-theory’s past year of commit activity
    Coq 30 3 2 1 Updated Jun 29, 2024
  • 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 26 MIT 4 0 0 Updated Jun 29, 2024
  • fourcolor Public

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

    coq-community/fourcolor’s past year of commit activity
    Coq 154 19 0 3 Updated Jun 29, 2024
  • coqeal Public

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

    coq-community/coqeal’s past year of commit activity
    Coq 64 15 5 3 Updated Jun 29, 2024