diff options
author | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-05-29 00:09:59 +0200 |
---|---|---|
committer | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-05-29 09:30:15 +0200 |
commit | 75283fdbb3c9179730091ec7076b37a9bcb86dad (patch) | |
tree | adb2a992c0fdf34ee03377aa7ae1f5de4e85172b | |
parent | 73792323172e289b531afc086d3f97323b28ecb6 (diff) |
Add note about PG branches and license
-rw-r--r-- | README.md | 25 |
1 files changed, 25 insertions, 0 deletions
@@ -2,12 +2,28 @@ [![Build Status](https://travis-ci.org/ProofGeneral/PG.svg?branch=master)](https://travis-ci.org/ProofGeneral/PG) +## Overview + Proof General is a generic Emacs interface for proof assistants. The aim of the Proof General project is to provide a powerful, generic environment for using interactive proof assistants. This is version 4.4.1~pre of Proof General. +## About Proof General branches + +Two editions of Proof General are currently available: + +* the (legacy) REPL-based, stable version of Proof General, + gathered in the + [master](https://github.com/ProofGeneral/PG/tree/master) branch, and + licensed under GPLv2; +* the (newest) Coq-specific, experimental version of Proof General, + supporting asynchronous proof processing, + gathered in the + [async](https://github.com/ProofGeneral/PG/tree/async) branch, and + licensed under GPLv3+. + ## Setup Remove old versions of Proof General, then download and install the new release from GitHub: @@ -57,3 +73,12 @@ Supported proof assistants: * Obsolete instances: Demoisa, Lambda-Clam, Plastic A few example proofs are included in each prover subdirectory. + +## Contributing + +Contributions to this repository are placed under the BSD-3 license. +As BSD-3 is compatible with both GPLv2 and GPLv3+, this means that +we can merge them in both `master` and `async` branches if need be, +using the same license as the rest of the codebase, while you keep +all the rights on your code. +For more info, see <https://opensource.org/licenses/BSD-3-Clause>. |