The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 07/09/2015 03:45 PM, Vadim Zaliva wrote:
> 
>> On Jul 9, 2015, at 13:34 , Kenneth Adam Miller 
>> <kennethadammiller AT gmail.com
>>  
>> <mailto:kennethadammiller AT gmail.com>>
>>  wrote:
>>
>> I could write an opam file for it. I think it would be suitable, but I 
>> think that there are aptitude, and emacs package descriptions for it as 
>> well, and together it's confusing which route to take and all...
> 
> I am not sure OPAM is the best way to manage EMACS packages.
> I recently started using this repo: http://melpa.org/ which contains 
> ‘company-coq’ package which should be dependent on PG, but
> PG itself is not included there. Ideally PG should be added there.

That's true; company-coq should register a dependency, but since PG isn't 
there it can't. It would be great if it was!

There have been discussion going on about this for a while, in particular on 
the Proof General mailing list. At some point Proof General will migrate to 
Github, and although that's taking a long time I don't think it would be good 
to migrate it aggressively.

Creating an Emacs package for PG is a trickier task than it could seem at 
first, in particular because most package archives have pretty strong 
requirements on package hygiene, and PG doesn't meet them. In particular, PG 
vendors mmm-mode, which is generally frowned upon (PG should register a 
dependency on mmm, not bundle it; but of course when PG was created the 
package manager didn't even exist). PG also ships with a number of obsolete 
options that make it look like an application in it's own right (so you can 
run Proof General and ignore that you're in Emacs). Finally, PG ships with 
it's own autoloads, instead of using magic comments (;;;###autoload).

If anyone is interesting in looking into these issues, the relevant email 
thread is on 
http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2015/000344.html, and 
detailed instructions to migrate the repo are 
http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2015/000348.html; feel 
free to share ideas there, too!
 
Cheers,
Clément.

> 
> 
> Sincerely,
> Vadim Zaliva
> 
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060
> Skype: vzaliva
>

Attachment: signature.asc
Description: OpenPGP digital signature