Message ID | 87iminpj9x.fsf@asu.edu |
---|---|
State | Accepted |
Headers | show |
Series | [bug#40311] Update proof-general | expand |
Context | Check | Description |
---|---|---|
cbaines/comparison | success | View comparision |
cbaines/git branch | success | View Git branch |
cbaines/applying patch | success | View Laminar job |
John Soo <jsoo1@asu.edu> writes: > Hi Guix, > > In my effort to use strictly guix for my emacs package management, I > found that proof-general was not working out of the box with guix.el. > > In the end I could not figure out how to make it work, but I did update > proof-general to 4.4 and updated the home-page. > > proof-general puts its initialization file in > %outputs/share/emacs/site-lisp/site-start.d/pg-init.el. I also see > Tuareg puts the file there. Niether that path, nor any subdirectory of > site-lisp is included by $EMACSLOADPATH or is autoloaded by guix.el. > > For the record, I added > (load-file "~/.guix-profile/share/emacs/site-lisp/site-start.d/pg-init.el") > to init.el as a workaround. > > Anyways, this should fix proof-general to work with the current version > of coq at least and add some more newer niceties in recent versions. Thanks! I applied both patches, and also added a proper commit message for the first one (mention the changes to the various fields). I also added a git-file-name for the first patch as suggested by 'guix lint'.
>From bc79d139873c9a831f373dc7e92dacd96a80fecb Mon Sep 17 00:00:00 2001 From: John Soo <jsoo1@asu.edu> Date: Sun, 29 Mar 2020 02:26:46 -0700 Subject: [PATCH 2/2] gnu: proof-general: Update home-page. * gnu/packages/coq.scm (proof-general):[home-page] update to proofgeneral.github.io --- gnu/packages/coq.scm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 937e2cc20a..2a7fae2a74 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -196,7 +196,7 @@ It is developed using Objective Caml and Camlp5.") (substitute* "Makefile" ((" [^ ]*\\.pdf") "")) (apply invoke "make" "install-doc" make-flags)))))) - (home-page "http://proofgeneral.inf.ed.ac.uk/") + (home-page "https://proofgeneral.github.io/ ") (synopsis "Generic front-end for proof assistants based on Emacs") (description "Proof General is a major mode to turn Emacs into an interactive proof -- 2.26.0