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: 22
Popularity: 1.524411
First Submitted: 2007-10-01 23:36
Last Updated: 2017-02-14 17:29

Latest Comments

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)

All comments