Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proof General has moved to GitHub!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof General has moved to GitHub!


Chronological Thread 
  • From: Clément Pit--Claudel <clement.pit AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proof General has moved to GitHub!
  • Date: Tue, 19 Jan 2016 08:25:23 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
  • Ironport-phdr: 9a23:UANoxhZtBDIvW2GEJYagNQ3/LSx+4OfEezUN459isYplN5qZpci/bnLW6fgltlLVR4KTs6sC0LqI9fGxEjdcqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh770qsyYOFkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JeWGXlxdOHz/97Q2/G7z1uzb2u+41jCKeMMj7S6xyQTW+x6huQR7sziwAMmhqoynslsVsgfcD81qarBtlztuMbQ==
On 01/19/2016 01:26 AM, John Wiegley wrote:
>>>>>> Jason Gross
>>>>>> <jasongross9 AT gmail.com>
>>>>>> writes:
>
>> I think there should instead be a MELPA package, but, as I understand it,
>> PG
>> currently needs arcane emacs flags to compile correctly, and melpa doesn't
>> support that (and it's not clear that it should).
>
> Any chance we could go full ELPA?

I would love that. I had been discussing it with Stefan. The major roadblocks
are:

1. PG needs a bit of cleaning up before it can be packaged (it has its own
autoload generation strategy, it vendors mmm-mode, `require`-ing certain of
its files crashes it unless some other commands are run, etc.)
2. We need to collect paperwork from contributors.

IMHO (1) is much trickier than (2).

Clément.

Archive powered by MHonArc 2.6.18.

Top of Page