Package Details: proofgeneral 4.2-2

Git Clone URL: https://aur.archlinux.org/proofgeneral.git (read-only)
Package Base: proofgeneral
Description: Generic interface for proof assistants.
Upstream URL: http://proofgeneral.inf.ed.ac.uk/
Licenses: GPL
Submitter: None
Maintainer: bluephoenix47
Last Packager: bluephoenix47
Votes: 19
Popularity: 0.007920
First Submitted: 2007-10-01 23:36
Last Updated: 2015-07-07 21:07

Latest Comments

bluephoenix47 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.

bluephoenix47 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)

bluephoenix47 commented on 2013-01-14 00:23

Updated per eatsaq's patch.

bluephoenix47 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!

bluephoenix47 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.

bluephoenix47 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.