Add Proof General recipe

[marsam]

Recently Proof General migrated to github https://github.com/ProofGeneral/PG
This recipe is a translation from the Makefile, and probably break some Proof General features, but I hope gets merged to help catch bugs in PG.

Thanks in advance

[purcell]

This recipe will copy all the .el into the root of the created package, right? Probably "*/*.el" would have the same effect and be more concise?

For me, it's already a problem that there's no top-level proof-general.el or proof-general-pkg.el from which we can obtain metadata for the package. That automatically makes this a malformed package, and I wouldn't be very happy to merge it in that state.

There has previously been discussion about adding Proof General to MELPA: #2907 and #2538. I'd be happy to hear any comments @npe9 and @cpitclaudel might have about this.

[cpitclaudel]

Hi @marsam and @purcell,

@marsam, thanks for working on this! It would be awesome to migrate PG to MELPA.

However, I'd be very surprised if copying all .el files to the root of the package worked well, if at all. And there are subtleties in the way PG is byte-compiled, too, so the recipe should probably take these into account.

Maybe a better first step would be to add a root proof-general.el (which is more or less what proof-site.el is), and a proper package definition? It would also be great to understand how PG's mmm-mode connects with the upstream mmm-mode.

[purcell]

Maybe a better first step would be to add a root proof-general.el (which is more or less what proof-site.el is), and a proper package definition?

Yes, even simply a proof-general-pkg.el with a (define-package ...) form.

It would also be great to understand how PG's mmm-mode connects with the upstream mmm-mode.

Indeed - I maintain the latter.

[marsam]

No problem, I'll try to make PG follow the melpa guidelines and update the recipe

[fourier]

Any move on this ?

[tarsius]

@marsam Here's a friendly ping for you.

[marsam]

Sorry for the late response. I'll start working on this this week

[cpitclaudel]

@marsam Note that we're in the process of rewriting significant parts of Proof General to support Coq's newer IDE protocol. This should be fairly independent of your efforts, but there'll probably be some rebasing work to do (creating a package will require new code in the repo)

[stardiviner]

Any news on this?

[marsam]

I think I managed to packaged :D. I'll make sure I haven't broken anything and make a pull request to upstream

@stardiviner You can try with:

(add-to-list 'package-archives
             '("emacs-pe" . "https://emacs-pe.github.io/packages/"))

(use-package coq
  :ensure t
  :defer t
  :pin emacs-pe)

[tarsius]

@marsam is there anything speaking against adding the recipe at https://github.com/emacs-pe/emacs-pe.github.io/blob/master/recipes/coq to Melpa also? If not, then please submit a pr.

[cpitclaudel]

@tarsius Yes: it doesn't work. The autoloads are wrong (PG needs pre-generated autoloads, since package.el doesn't recurse into subdirectories to find autoloads. See ProofGeneral/PG#128

[tarsius]

Is there any hope it can be made to work? This has been open for over a year now, and I kinda have lost hope in this being completed anytime soon. Should we close this?

[cpitclaudel]

I think it's pretty close :) Completing the patch plus testing it should be a matter of at most a few hours, but when one of us will have that time is unpredictable. @marsam, do you want to try to build on ProofGeneral/PG#128?

It's not for me to say whether we should close this, since I'm not the original author of this PR :)

[marsam]

Hi:

Sorry for the late response. Given that ProofGeneral/PG#128 is likely to be
merged, and is a different approach. I'm closing this PR.

FWWI, How is ProofGeneral and Coq are packaged in https://emacs-pe.github.io/packages/

/libs
Each file has its own recipe.

/generic
I've moved all the generic dependencies here and created a package proof
as base package so the autoload file are generated for /generic directory only.
So each prover i.e coq can have is own recipe and can installed
independently.

@cpitclaudel I'll open another PR after ProofGeneral/PG#128 is merged.

[cpitclaudel]

@marsam I've made progress on this at ProofGeneral/PG#157 ; maybe you could take a look? Thanks :)

[marsam]

@cpitclaudel Sure, I'll take a look during the week :)

[cpitclaudel]

Thanks a lot!