diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 125 |
1 files changed, 52 insertions, 73 deletions
@@ -1,86 +1,65 @@ -How to write plugins in Coq -=========================== - # Working environment : merlin, tuareg (open question) - - ## OCaml & related tools +# Coq - These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) +[](https://gitlab.com/coq/coq/commits/master) +[](https://travis-ci.org/coq/coq/builds) +[](https://ci.appveyor.com/project/coq/coq/branch/master) +[](https://gitter.im/coq/coq) +[](https://doi.org/10.5281/zenodo.1003420) -```shell -opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2 -eval `opam config env --root=$PWD/CIW2018` -opam install camlp5 ocamlfind num # Coq's dependencies -opam install lablgtk # Coqide's dependencies (optional) -opam install merlin # prints instructions for vim and emacs -``` +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. - ## Coq +## Installation +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. -```shell -git clone git@github.com:coq/coq.git -cd coq -./configure -profile devel -make -j2 -cd .. -export PATH=$PWD/coq/bin:$PATH -``` +## Documentation - ## This tutorial +The sources of the documentation can be found in directory [`doc`](doc). +See [`doc/README.md`](/doc/README.md) to learn more about the documentation, +in particular how to build it. The +documentation of the last released version is available on the Coq +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. -```shell -git clone git@github.com:ybertot/plugin_tutorials.git -cd plugin_tutorials/tuto0 -make .merlin # run before opening .ml files in your editor -make # build -``` - - - - # tuto0 : basics of project organization - package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` - - Example of syntax to add a new toplevel command - - Example of function call to print a simple message - - Example of syntax to add a simple tactic - (that does nothing and prints a message) - - To use it: +## Changes +There is a file named [`CHANGES.md`](CHANGES.md) that explains the differences and the +incompatibilities since last versions. If you upgrade Coq, please read +it carefully. -```bash - cd tuto0; make - coqtop -I src -R theories Tuto0 -``` +## 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 +subscription link can be found at [coq.inria.fr/community](http://coq.inria.fr/community). - In the Coq session type: -```coq - Require Import Tuto0.Loader. HelloWorld. -``` +The topics to be discussed in the club should include: - # tuto1 : Ocaml to Coq communication - Explore the memory of Coq, modify it - - Commands that take arguments: strings, symbols, expressions of the calculus of constructions - - Commands that interact with type-checking in Coq - - A command that adds a new definition or theorem - - A command that uses a name and exploits the existing definitions - or theorems - - A command that exploits an existing ongoing proof - - A command that defines a new tactic +* technical problems; +* questions about proof developments; +* suggestions and questions about the implementation; +* announcements of proofs; +* theoretical questions about typed lambda-calculi which are + closely related to Coq. - Compilation and loading must be performed as for `tuto0`. - - # tuto2 : Ocaml to Coq communication - A more step by step introduction to writing commands - - Explanation of the syntax of entries - - Adding a new type to and parsing to the available choices - - Handling commands that store information in user-chosen registers and tables +## Bugs report +Please report any bug / feature request in [our issue tracker](https://github.com/coq/coq/issues). - Compilation and loading must be performed as for `tuto1`. +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. - # tuto3 : manipulating terms of the calculus of constructions - Manipulating terms, inside commands and tactics. - - Obtaining existing values from memory - - Composing values - - Verifying types - - Using these terms in commands - - Using these terms in tactics - - Automatic proofs without tactics using type classes and canonical structures +## Contributing - compilation and loading must be performed as for `tuto0`. +Guidelines for contributing to Coq in various ways are listed in the [contributor's guide](CONTRIBUTING.md). + +## Supporting Coq + +Help the Coq community grow and prosper by becoming a sponsor! The [Coq +Consortium](https://coq.inria.fr/consortium) can establish sponsorship contracts +or receive donations. If you want to take an active role in shaping Coq's +future, you can also become a Consortium member. If you are interested, please +get in touch! |