Package Details: proofgeneral 4.5-4

Git Clone URL: (read-only, click to copy)
Package Base: proofgeneral
Description: Generic interface for proof assistants.
Upstream URL:
Licenses: GPL
Replaces: proofgeneral-nox
Submitter: None
Maintainer: gilcu3
Last Packager: gilcu3
Votes: 23
Popularity: 0.000000
First Submitted: 2007-10-01 23:36 (UTC)
Last Updated: 2022-09-26 07:42 (UTC)

Latest Comments

1 2 3 4 Next › Last »

wilbowma commented on 2017-04-15 23:05 (UTC)

Ah, this is indeed a bug in the proofgeneral, but the `make install` installation is also depricated.

wilbowma commented on 2017-04-15 21:29 (UTC)

@suzumiya, sorry for the delay. The install scripts for the project don't make /usr/bin/proofgeneral executable. I can't tell if this is by design, e.g., because proofgeneral is not meant to be executed directly?

suzumiya commented on 2017-02-20 16:28 (UTC)

I successfully built it yesterday, but find that the file `/usr/bin/proofgeneral` is not an executable one. After I set it executable for all users, all things work well. I reckon it might due to some minor config problems in this rp. p.s. Thanks for your devotion to this rp. I love it.

zorun commented on 2017-02-09 20:54 (UTC)

Strange, it builds fine now (in a clean chroot, exactly in the same way I did it before when it failed). By the way, you may want to set the arch to "any", because the package does not contain any ELF binary.

wilbowma commented on 2017-02-08 22:39 (UTC)

Upgraded to Coq 8.6-4, and still can't reproduce.

wilbowma commented on 2017-02-08 21:57 (UTC)

@zorun, I cannot reproduce using emacs 25.1-4. What version of Coq are you using?

zorun commented on 2017-02-04 20:07 (UTC)

Build fails, here is the log: Maybe this is related to emacs 25.1?

wilbowma commented on 2016-10-14 21:26 (UTC)

@tchajed, thanks! Will update shortly

tchajed commented on 2016-10-14 21:14 (UTC)

Proof General has released v4.4 on GitHub ( It seems the proofgeneral-git PKGBUILD nearly works for this release, the only difference being that the .tar.gz extracts to the file PG-${pkgver} (and of course the .tar.gz has a fixed checksum that should be in the PKGBUILD). In addition, the new upstream URL to list is, and the recommended line to add to ~/.emacs is now: (load "/usr/share/emacs/site-lisp/ProofGeneral/generic/proof-site")

wilbowma commented on 2016-08-02 22:36 (UTC)

As far as I can tell, 4.2 is the last "release" version. I find references to 4.3pre and 4.4pre, but no release packages or tags. Unflagging this as out-of-date for now. If you want the most recent from GitHub, it looks like 4.4pre can be easily installed locally in .emacs.d.