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.

Please do let me know if you already have the forms on file, too.

Cheers and thanks for your help in making PG easier to install for our users, 
and to hack on for everyone,

Attachment: signature.asc
Description: OpenPGP digital signature

ProofGeneral-devel mailing list

Reply via email to