From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- README.md | 32 +++++++++++++++++++++----------- 1 file changed, 21 insertions(+), 11 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index a41ee7cc..51dd3f27 100644 --- a/README.md +++ b/README.md @@ -1,24 +1,33 @@ # Coq + +[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds) +[![Appveyor](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master) +[![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq) +[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg)](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 -See the file `INSTALL` for installation procedure. +Download the pre-built packages of the [latest release](https://github.com/coq/coq/releases/latest) for Windows and MacOS; +read the [help page](https://coq.inria.fr/opam/www/using.html) on how to install Coq with OPAM; +or refer to the [`INSTALL` file](/INSTALL) for the procedure to install from source. ## Documentation -The documentation is part of the archive in directory doc. The + +The sources of the documentation can be found in directory [`doc`](/doc). The documentation of the last released version is available on the Coq -web site at [coq.inria.fr/doc](http://coq.inria.fr/doc). +web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). +See also [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), +and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ), +for additional user-contributed documentation. ## Changes -There is a file named `CHANGES` that explains the differences and the +There is a file named [`CHANGES`](/CHANGES) that explains the differences and the incompatibilities since last versions. If you upgrade Coq, please read it carefully. -## Availability -Coq is available from [coq.inria.fr](http://coq.inria.fr). - ## The Coq Club The Coq Club moderated mailing list is meant to be a standard way to discuss questions about the Coq system and related topics. The @@ -33,12 +42,13 @@ The topics to be discussed in the club should include: * theoretical questions about typed lambda-calculi which are closely related to Coq. -For any questions/suggestions about the Coq Club, please write to -`coq-club-request@inria.fr`. - ## Bugs report -Send your bug reports by filling a form at [coq.inria.fr/bugs](http://coq.inria.fr/bugs). +Please report any bug / feature request in [our issue tracker](https://github.com/coq/coq/issues). To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (`coqtop -v`), the configuration used, and include a complete source example leading to the bug. + +## Contributing + +Guidelines for contributing to Coq in various ways are listed in the [contributor's guide](CONTRIBUTING.md). -- cgit v1.2.3