Package Details: proofgeneral 4.4-3

Git Clone URL: https://aur.archlinux.org/proofgeneral.git (read-only)
Package Base: proofgeneral
Description: Generic interface for proof assistants.
Upstream URL: https://proofgeneral.github.io/
Licenses: GPL
Submitter: None
Maintainer: wilbowma
Last Packager: wilbowma
Votes: 23
Popularity: 0.936979
First Submitted: 2007-10-01 23:36
Last Updated: 2017-02-14 17:29

Latest Comments

wilbowma commented on 2017-04-15 23:05

Ah, this is indeed a bug in the proofgeneral, but the `make install` installation is also depricated. https://github.com/ProofGeneral/PG/issues/177

wilbowma commented on 2017-04-15 21:29

@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

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

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

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

wilbowma commented on 2017-02-08 21:57

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

zorun commented on 2017-02-04 20:07

Build fails, here is the log: http://paste.aliens-lyon.fr/3tq

Maybe this is related to emacs 25.1?

wilbowma commented on 2016-10-14 21:26

@tchajed, thanks! Will update shortly

tchajed commented on 2016-10-14 21:14

Proof General has released v4.4 on GitHub (https://github.com/ProofGeneral/PG/releases). 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 https://proofgeneral.github.io, 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

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.

wilbowma commented on 2013-03-31 18:46

Integrated that bug fix and updated to 4.2

aws commented on 2013-03-26 13:13

The build fails for emacs 24.3, which is the current version in Extra. Bug is listed upstream as at http://proofgeneral.inf.ed.ac.uk/trac/ticket/458. The fix recommended there is to disable error-on-warn, as contained in the following patch:

diff -c src/ProofGeneral-4.1/Makefile src_fixed/ProofGeneral-4.1/Makefile
*** src/ProofGeneral-4.1/Makefile 2010-10-10 23:56:56.000000000 +0100
--- src_fixed/ProofGeneral-4.1/Makefile 2013-03-26 12:54:24.807369437 +0000
***************
*** 60,66 ****
# only during compilation. Another idea: put a function in proof-site
# to output the compile-time load path and ELISP_DIRS so these are set
# just in that one place.
! BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "${PWD}/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)

--- 60,66 ----
# only during compilation. Another idea: put a function in proof-site
# to output the compile-time load path and ELISP_DIRS so these are set
# just in that one place.
! BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "${PWD}/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) )' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)

aws commented on 2013-03-26 13:12

The build fails for emacs 24.3, which is the current version in Extra. Bug is listed upstream as [#458](http://proofgeneral.inf.ed.ac.uk/trac/ticket/458). The fix recommended there is to disable error-on-warn, as contained in the following patch:


diff -c src/ProofGeneral-4.1/Makefile src_fixed/ProofGeneral-4.1/Makefile
*** src/ProofGeneral-4.1/Makefile 2010-10-10 23:56:56.000000000 +0100
--- src_fixed/ProofGeneral-4.1/Makefile 2013-03-26 12:54:24.807369437 +0000
***************
*** 60,66 ****
# only during compilation. Another idea: put a function in proof-site
# to output the compile-time load path and ELISP_DIRS so these are set
# just in that one place.
! BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "${PWD}/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)

--- 60,66 ----
# only during compilation. Another idea: put a function in proof-site
# to output the compile-time load path and ELISP_DIRS so these are set
# just in that one place.
! BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "${PWD}/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) )' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)

wilbowma commented on 2013-01-14 00:23

Updated per eatsaq's patch.

wilbowma commented on 2013-01-11 23:32

@eatsaq: Can you provide error logs/steps to reproduce?

eatsaq commented on 2013-01-11 08:27

Compiling fails for the PhoX proof assistant bit. I removed the support (as I don't need it) like this:


--- proofgeneral/PKGBUILD 2012-10-14 02:51:57.000000000 +0300
+++ proofgeneral_fixed/PKGBUILD 2013-01-11 10:14:43.001542895 +0200
@@ -22,6 +22,9 @@

patch -p1 < "${srcdir}/interactive-p.patch"

+ sed -i 's,phox/\*,,' Makefile
+ sed -i 's,phox,,' Makefile
+
make
}

djhaskin987 commented on 2013-01-09 16:34

Awesome! Thanks so much.

Also, this page was helpful to me:
http://permalink.gmane.org/gmane.emacs.proofgeneral.devel/224
I used the patch at the bottom of the comment in build() since my installation of emacs is no-X.

Hope that helps!
Thanks again!

wilbowma commented on 2012-10-13 23:53

Thanks for the improvements!

chneukirchen commented on 2012-10-10 23:02

Improved PKGBUILD: http://sprunge.us/UQbO
* make isartags executable
* make install -j1 because with parallelization the bin/ scripts could be clobbered (ugh).

pherms commented on 2012-06-15 14:33

Note however that proofgeneral is currently not fully compatible with emacs 24.
One problem has been found and reported:
http://proofgeneral.inf.ed.ac.uk/trac/ticket/442
If you find other bugs, please report them as there will be a new release soon.

wilbowma commented on 2012-06-14 19:09

Thanks for the patch, it's been updated.

eatsaq commented on 2012-06-14 11:55

It didn't compile against latest Emacs, 24.1. I fixed the code and PKGBUILD and created a patch:

https://gist.github.com/2929859

eatsaq commented on 2012-06-14 08:56

It didn't compile against latest Emacs, 24.1. I fixed the code and PKGBUILD and created a patch:

https://gist.github.com/2929161

eatsaq commented on 2012-06-14 08:26

Won't compile with Emacs 24.1.

pherms commented on 2011-10-03 15:17

4.1 is out.

td123 commented on 2011-07-05 20:28

disowning, 4.1RC2 isn't really a version bump, but I'll leave that up to the next maintainer to decide on

td123 commented on 2011-04-13 05:23

@victor.vde
Thanks, everything should compile fine now.

victor.vde commented on 2011-04-12 19:10

It doesn't build with emacs 23.3 without patching mmm.
Patch at http://paste.lisp.org/display/121434 , tested by proof-mmm-toggle -ing a few times.

td123 commented on 2010-11-08 15:32

done

npouillard commented on 2010-11-08 09:38

Since the upstream distribution ships compiled file (for emacs 23.1), I would suggest to run make clean before make.