<commit_before># Coq

[![GitLab][gitlab-badge]][gitlab-link]
[![Azure Pipelines][azure-badge]][azure-link]
[![Gitter][gitter-badge]][gitter-link]
[![DOI][doi-badge]][doi-link]

[gitlab-badge]: https://gitlab.com/coq/coq/badges/master/pipeline.svg
[gitlab-link]: https://gitlab.com/coq/coq/commits/master

[azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master
[azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master

[gitter-badge]: https://badges.gitter.im/coq/coq.svg
[gitter-link]: https://gitter.im/coq/coq

[doi-badge]: https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg
[doi-link]: https://doi.org/10.5281/zenodo.1003420

Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs.

## Installation

[![latest packaged version(s)][repology-badge]][repology-link]

[![Arch package][arch-badge]][arch-link]
[![Chocolatey package][chocolatey-badge]][chocolatey-link]
[![Conda package][conda-badge]][conda-link]
[![Homebrew package][homebrew-badge]][homebrew-link]
[![nixpkgs unstable package][nixpkgs-badge]][nixpkgs-link]

[repology-badge]: https://repology.org/badge/latest-versions/coq.svg
[repology-link]: https://repology.org/metapackage/coq/versions

[arch-badge]: https://repology.org/badge/version-for-repo/arch/coq.svg
[arch-link]: https://www.archlinux.org/packages/community/x86_64/coq/

[chocolatey-badge]: https://repology.org/badge/version-for-repo/chocolatey/coq.svg
[chocolatey-link]: https://chocolatey.org/packages/Coq

[conda-badge]: https://img.shields.io/conda/vn/conda-forge/coq.svg?label="Conda%20package"
[conda-link]: https://github.com/conda-forge/coq-feedstock

[homebrew-badge]: https://repology.org/badge/version-for-repo/homebrew/coq.svg
[homebrew-link]: https://formulae.brew.sh/formula/coq

[macports-badge]: https://repology.org/badge/version-for-repo/macports/coq.svg
[macports-link]: https://www.macports.org/ports.php?by=name&substr=coq

[nixpkgs-badge]: https://repology.org/badge/version-for-repo/nix_unstable/coq.svg
[nixpkgs-link]: https://nixos.org/nixos/packages.html#coq

Download the pre-built packages of the [latest release][] for Windows and macOS;
read the [help page][opam-using] on how to install Coq with OPAM;
or refer to the [`INSTALL.md`](INSTALL.md) file for the procedure to install from source.

[latest release]: https://github.com/coq/coq/releases/latest<commit_msg>Add badges for Docker Hub and coqorg/coq:latest version<commit_after># Coq

[![GitLab][gitlab-badge]][gitlab-link]
[![Azure Pipelines][azure-badge]][azure-link]
[![Gitter][gitter-badge]][gitter-link]
[![DOI][doi-badge]][doi-link]

[gitlab-badge]: https://gitlab.com/coq/coq/badges/master/pipeline.svg
[gitlab-link]: https://gitlab.com/coq/coq/commits/master

[azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master
[azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master

[gitter-badge]: https://badges.gitter.im/coq/coq.svg
[gitter-link]: https://gitter.im/coq/coq

[doi-badge]: https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg
[doi-link]: https://doi.org/10.5281/zenodo.1003420

Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs.

## Installation

[![latest packaged version(s)][repology-badge]][repology-link]

[![Arch package][arch-badge]][arch-link]
[![Chocolatey package][chocolatey-badge]][chocolatey-link]
[![Conda package][conda-badge]][conda-link]
[![Homebrew package][homebrew-badge]][homebrew-link]
[![nixpkgs unstable package][nixpkgs-badge]][nixpkgs-link]

[![Docker Hub package][dockerhub-badge]][dockerhub-link]
[![latest dockerized version][coqorg-badge]][coqorg-link]

[repology-badge]: https://repology.org/badge/latest-versions/coq.svg
[repology-link]: https://repology.org/metapackage/coq/versions

[arch-badge]: https://repology.org/badge/version-for-repo/arch/coq.svg
[arch-link]: https://www.archlinux.org/packages/community/x86_64/coq/

[chocolatey-badge]: https://repology.org/badge/version-for-repo/chocolatey/coq.svg
[chocolatey-link]: https://chocolatey.org/packages/Coq

[conda-badge]: https://img.shields.io/conda/vn/conda-forge/coq.svg?label="Conda%20package"
[conda-link]: https://github.com/conda-forge/coq-feedstock

[homebrew-badge]: https://repology.org/badge/version-for-repo/homebrew/coq.svg
[homebrew-link]: https://formulae.brew.sh/formula/coq

[macports-badge]: https://repology.org/badge/version-for-repo/macports/coq.svg
[macports-link]: https://www.macports.org/ports.php?by=name&substr=coq

[nixpkgs-badge]: https://repology.org/badge/version-for-repo/nix_unstable/coq.svg
[nixpkgs-link]: https://nixos.org/nixos/packages.html#coq

[dockerhub-badge]: https://img.shields.io/docker/automated/coqorg/coq.svg
[dockerhub-link]: https://hub.docker.com/r/coqorg/coq "Automated build on Docker Hub"

[coqorg-badge]: https://images.microbadger.com/badges/version/coqorg/coq.svg
[coqorg-link]: https://github.com/coq-community/docker-coq/wiki#docker-coq-images "Docker images of Coq"

Download the pre-built packages of the [latest release][] for Windows and macOS;
read the [help page][opam-using] on how to install Coq with OPAM;
or refer to the [`INSTALL.md`](INSTALL.md) file for the procedure to install from source.

[latest release]: https://github.com/coq/coq/releases/latest
{'fraction_non_alphanumeric': 0.17705382436260622, 'fraction_numerical': 0.011685552407932011, 'mean_word_length': 5.614754098360656, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 50, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5743304', 'n_tokens_mistral': 2238, 'n_tokens_neox': 2125, 'n_words': 299}