* bug#46016: broken Proof-General (emacs front-end to Coq)
@ 2021-01-21 11:10 zimoun
2021-01-21 12:04 ` zimoun
` (2 more replies)
0 siblings, 3 replies; 9+ messages in thread
From: zimoun @ 2021-01-21 11:10 UTC (permalink / raw)
To: 46016
Hi,
Let instantiate an environment:
guix environment -C -E TERM \
--ad-hoc coq proof-general emacs \
busybox \
-- emacs -q
and then “C-h i m“ list ‘Proof General’ and I can read the manual.
However, there is no ELisp about coq-mode or pg stuff. Let ’M-x shell’
and then:
--8<---------------cut here---------------start------------->8---
$ ls -aR1 $GUIX_ENVIRONMENT | grep '\.el'
guix-emacs.el
guix-emacs.elc
site-start.el
site-start.elc
--8<---------------cut here---------------end--------------->8---
(The package busybox is for debugging: necessary to be able to run Info
in container, list all files and grep them.)
Maybe it is related to bug#45781 [1].
1: < https://issues.guix.gnu.org/45781>
All the best,
simon
^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-01-21 11:10 bug#46016: broken Proof-General (emacs front-end to Coq) zimoun
@ 2021-01-21 12:04 ` zimoun
2021-01-21 21:26 ` Mark H Weaver
2021-11-10 19:38 ` zimoun
2 siblings, 0 replies; 9+ messages in thread
From: zimoun @ 2021-01-21 12:04 UTC (permalink / raw)
To: 46016
Hi,
On Thu, 21 Jan 2021 at 12:10, zimoun <zimon.toutoune@gmail.com> wrote:
> Let instantiate an environment:
>
> guix environment -C -E TERM \
> --ad-hoc coq proof-general emacs \
> busybox \
> -- emacs -q
>
[...]
> $ ls -aR1 $GUIX_ENVIRONMENT | grep '\.el'
> guix-emacs.el
> guix-emacs.elc
> site-start.el
> site-start.elc
This command is wrong and shows nothing! :-)
However, note that once Emacs is launched,
M-: (load “$GUIX_ENVIRONMENT/share/emacs/site-lisp/site-start.d/pg-init.el”)
allows to see the ’ProofGeneral’ front-end; for instance opening a Coq
file and small experiments seem to work.
> Maybe it is related to bug#45781 [1].
>
> 1: < https://issues.guix.gnu.org/45781>
Well, I do not know if it is related. But what is loaded does not seem
to work as expected. I mean, I am expecting that all under
’site-lisp/site-start.d/’ are run at start time.
All the best,
simon
^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-01-21 11:10 bug#46016: broken Proof-General (emacs front-end to Coq) zimoun
2021-01-21 12:04 ` zimoun
@ 2021-01-21 21:26 ` Mark H Weaver
2021-01-22 10:15 ` zimoun
2021-11-10 19:38 ` zimoun
2 siblings, 1 reply; 9+ messages in thread
From: Mark H Weaver @ 2021-01-21 21:26 UTC (permalink / raw)
To: zimoun, 46016
[-- Attachment #1: Type: text/plain, Size: 348 bytes --]
I've been carrying the attached commit on my private branch for a while
now. It may be an improvement, but I've forgotten the details. I used
proof-general for a while when I was learning Coq, but have since
removed it because I found it annoying that GNOME Shell misidentified my
normal Emacs as being an instance of Proof General.
Mark
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: Patch to possibly improve Proof General packaging in Guix --]
[-- Type: text/x-patch, Size: 4232 bytes --]
From a33bc91ac1327e3bcad335bb2eb84abaf7b785cb Mon Sep 17 00:00:00 2001
From: Mark H Weaver <mhw@netris.org>
Date: Tue, 7 Apr 2020 05:39:41 -0400
Subject: [PATCH] LOCAL: gnu: proof-general: Improve packaging.
* gnu/packages/coq.scm (proof-general)[arguments]: Remove the
'disable-byte-compile-error-on-warn' and 'clean' custom phases. Add
'make-installed-binaries-executable' phase. Adapt 'patch-hardcoded-paths'
phase to new version. Reindent.
---
gnu/packages/coq.scm | 52 ++++++++++++++++++++++----------------------
1 file changed, 26 insertions(+), 26 deletions(-)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fb6a899b48..656a07f31b 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -148,8 +148,7 @@ It is developed using Objective Caml and Camlp5.")
(source (origin
(method git-fetch)
(uri (git-reference
- (url (string-append
- "https://github.com/ProofGeneral/PG"))
+ (url "https://github.com/ProofGeneral/PG.git")
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
@@ -176,31 +175,32 @@ It is developed using Objective Caml and Camlp5.")
#:phases
(modify-phases %standard-phases
(delete 'configure)
- (add-after 'unpack 'disable-byte-compile-error-on-warn
- (lambda _
- (substitute* "Makefile"
- (("\\(setq byte-compile-error-on-warn t\\)")
- "(setq byte-compile-error-on-warn nil)"))
- #t))
(add-after 'unpack 'patch-hardcoded-paths
- (lambda* (#:key inputs outputs #:allow-other-keys)
- (let ((out (assoc-ref outputs "out"))
- (coq (assoc-ref inputs "coq"))
- (emacs (assoc-ref inputs "host-emacs")))
- (define (coq-prog name)
- (string-append coq "/bin/" name))
- (substitute* "Makefile"
- (("/sbin/install-info") "install-info"))
- (substitute* "bin/proofgeneral"
- (("^PGHOMEDEFAULT=.*" all)
- (string-append all
- "PGHOME=$PGHOMEDEFAULT\n"
- "EMACS=" emacs "/bin/emacs")))
- #t)))
- (add-after 'unpack 'clean
- (lambda _
- ;; Delete the pre-compiled elc files for Emacs 23.
- (invoke "make" "clean")))
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (let ((out (assoc-ref outputs "out"))
+ (coq (assoc-ref inputs "coq"))
+ (emacs (assoc-ref inputs "host-emacs")))
+ (define (coq-prog name)
+ (string-append coq "/bin/" name))
+ (make-file-writable "coq/coq-system.el")
+ (emacs-substitute-variables "coq/coq-system.el"
+ ("coq-prog-name" (coq-prog "coqtop"))
+ ("coq-compiler" (coq-prog "coqc"))
+ ("coq-dependency-analyzer" (coq-prog "coqdep")))
+ (substitute* "Makefile"
+ (("/sbin/install-info") "install-info"))
+ (substitute* "bin/proofgeneral"
+ (("^PGHOMEDEFAULT=.*" all)
+ (string-append
+ "PGHOMEDEFAULT=" out "/share/emacs/site-lisp/ProofGeneral\n"
+ "EMACS=" emacs "/bin/emacs")))
+ #t)))
+ (add-after 'install 'make-installed-binaries-executable
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((out (assoc-ref outputs "out")))
+ (for-each (lambda (file) (chmod file #o555))
+ (find-files (string-append out "/bin")))
+ #t)))
(add-after 'install 'install-doc
(lambda* (#:key make-flags #:allow-other-keys)
;; XXX FIXME avoid building/installing pdf files,
--
2.30.0
^ permalink raw reply related [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-01-21 21:26 ` Mark H Weaver
@ 2021-01-22 10:15 ` zimoun
2021-01-24 18:37 ` John Soo
0 siblings, 1 reply; 9+ messages in thread
From: zimoun @ 2021-01-22 10:15 UTC (permalink / raw)
To: Mark H Weaver, 46016
Hi Mark,
On Thu, 21 Jan 2021 at 16:26, Mark H Weaver <mhw@netris.org> wrote:
> I've been carrying the attached commit on my private branch for a while
> now. It may be an improvement, but I've forgotten the details. I
> used
Thanks! It helps.
Based on your patch, I have tweaked a bit and now “bin/proofgeneral“
seems to work. However, I have not yet tweaked enough to have the Emacs
load-path works.
> + (substitute* "bin/proofgeneral"
> + (("^PGHOMEDEFAULT=.*" all)
What does this line do?
All the best,
simon
^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-01-22 10:15 ` zimoun
@ 2021-01-24 18:37 ` John Soo
2021-01-25 10:54 ` zimoun
0 siblings, 1 reply; 9+ messages in thread
From: John Soo @ 2021-01-24 18:37 UTC (permalink / raw)
To: zimoun; +Cc: 46016
Hi zimoun,
I use Proof General pretty regularly. I think this is the same as
https://issues.guix.gnu.org/45781.
Kindly,
John
^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-01-24 18:37 ` John Soo
@ 2021-01-25 10:54 ` zimoun
2021-01-25 15:14 ` John Soo
0 siblings, 1 reply; 9+ messages in thread
From: zimoun @ 2021-01-25 10:54 UTC (permalink / raw)
To: John Soo; +Cc: 46016
Hi John,
On Sun, 24 Jan 2021 at 10:37, John Soo <jsoo1@asu.edu> wrote:
> I use Proof General pretty regularly. I think this is the same as
> https://issues.guix.gnu.org/45781.
No, I do not think it is the same issue.
As the Mark’s patch and my previous message [1] in this thread both
shown, I think the package is misconfigured. Therefore, how do you use
it? Maybe, I misunderstand something.
1: https://yhetil.org/guix/86eeielcms.fsf@gmail.com
Thanks,
simon
^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-01-25 10:54 ` zimoun
@ 2021-01-25 15:14 ` John Soo
0 siblings, 0 replies; 9+ messages in thread
From: John Soo @ 2021-01-25 15:14 UTC (permalink / raw)
To: zimoun; +Cc: 46016
Hi zimoun!
I'm sorry I forgot I had this line in init.el:
(load-file "~/.guix-profile/share/emacs/site-lisp/site-start.d/pg-init.el")
It does seem like proof general is misconfigured. Apologies.
- John
^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-01-21 11:10 bug#46016: broken Proof-General (emacs front-end to Coq) zimoun
2021-01-21 12:04 ` zimoun
2021-01-21 21:26 ` Mark H Weaver
@ 2021-11-10 19:38 ` zimoun
2021-11-22 18:36 ` zimoun
2 siblings, 1 reply; 9+ messages in thread
From: zimoun @ 2021-11-10 19:38 UTC (permalink / raw)
To: 46016; +Cc: public, jsoo1
Hi,
I think this bug is fixed by patch#51755 [1].
1: <http://issues.guix.gnu.org/issue/51755>
Cheers,
simon
^ permalink raw reply [flat|nested] 9+ messages in thread
* bug#46016: broken Proof-General (emacs front-end to Coq)
2021-11-10 19:38 ` zimoun
@ 2021-11-22 18:36 ` zimoun
0 siblings, 0 replies; 9+ messages in thread
From: zimoun @ 2021-11-22 18:36 UTC (permalink / raw)
To: 46016-done; +Cc: public, jsoo1
Hi,
On Wed, 10 Nov 2021 at 20:38, zimoun <zimon.toutoune@gmail.com> wrote:
> 1: <http://issues.guix.gnu.org/issue/51755>
Done with cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8.
Cheers,
simon
^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2021-11-22 18:40 UTC | newest]
Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-01-21 11:10 bug#46016: broken Proof-General (emacs front-end to Coq) zimoun
2021-01-21 12:04 ` zimoun
2021-01-21 21:26 ` Mark H Weaver
2021-01-22 10:15 ` zimoun
2021-01-24 18:37 ` John Soo
2021-01-25 10:54 ` zimoun
2021-01-25 15:14 ` John Soo
2021-11-10 19:38 ` zimoun
2021-11-22 18:36 ` zimoun
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.