On 19.01.2016 17:05, Clément Pit--Claudel wrote:
Hi pg-devel folks,

TL;DR: Please get in touch with me if you've made significant contributions to the 
PG source code (> 10 lines total); we need an FSF copyright assignment from you 
to include PG in Emacs.

Pierre and I, and Stefan, are looking for ways to make Proof General easier to 
install for our users, and to relieve David of some of the maintenance burden. 
Moving to Github was a good step, but it's not the whole story; in particular, 
we're still dependent on David to maintain the website, and release packages 
for various Linux distributions.

One significant change since PG was launched is how Emacs packages are 
typically distributed: it used to be the case that packages would be either 
installed from a source code repository, or shared as tarballs, or through the 
package managers of Linux distributions; but Emacs now has (and has had for a 
while) it's own package manager. Migrating to this would make a lot of things 
simpler for us:

* No need for per-distribution packages
* No need to manage a complex release process
* No need for complex installation instructions
* We could depend on other packages: for example we could depend on the latest 
mmm-mode instead of vendoring it, or we could use the seq library, etc. (this 
has been a pain point for me while working on PG patches: I can't use features 
of external libraries at all)
The move to Github went pretty smoothly, so I think now is a good time to go one step further and move to ELPA. ELPA is the Emacs Lisp Package Archive, the main FSF-maintained package repository for Emacs. Choosing this package archive will have the additional advantage that we will be part of the official Emacs ecosystem: it'll be easier for us to ask for help, for example.

Two things need to be done for this:

* A general cleanup to be a good citizen of the package eco-system; Stefan will 
do it :)
* Copyright assignments: hosting packages in the GNU Emacs package archive 
requires them; see https://www.gnu.org/licenses/why-assign.html for more info. 
The broad idea is that as we transfer PG into Emacs, it becomes covered by FSF; 
that doesn't make a big difference in the end, since it stays GPL.

Hi Clément,

IMO that makes a big difference, as FSF-Emacs refuses to distribute GPLed code - unless it's copyrighted under US-law.

Requiring US-copyright is a different thing than the idea of free software. AFAIK it puts its signers under considerable risk. The papers to sign are hard to find, resp. not available in public. The contributor doesn't get legal advice when signing, etc.

What about using Melpa - which would not require the US-legal procedure.

(require 'package)
(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/";) t)

Would be all needed than to make proof-general available.

Best regards,


ProofGeneral-devel mailing list

Reply via email to