bug#46016: broken Proof-General (emacs front-end to Coq)

[zimoun]

Hi,

On Wed, 10 Nov 2021 at 20:38, zimoun  wrote:

> 1: 

Done with cb296dfa2e2938d18ae0ee347bed0cc94bc79cf8.

Cheers,
simon

bug#46016: broken Proof-General (emacs front-end to Coq)

[zimoun]

Hi,

I think this bug is fixed by patch#51755 [1].

1: 

Cheers,
simon

bug#46016: broken Proof-General (emacs front-end to Coq)

[John Soo]

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

bug#46016: broken Proof-General (emacs front-end to Coq)

[zimoun]

Hi John,

On Sun, 24 Jan 2021 at 10:37, John Soo  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@gmail.com


Thanks,
simon

bug#46016: broken Proof-General (emacs front-end to Coq)

[John Soo]

Hi zimoun,

I use Proof General pretty regularly. I think this is the same as
https://issues.guix.gnu.org/45781.

Kindly,

John

bug#46016: broken Proof-General (emacs front-end to Coq)

[zimoun]

Hi Mark,

On Thu, 21 Jan 2021 at 16:26, Mark H Weaver  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

bug#46016: broken Proof-General (emacs front-end to Coq)

[Mark H Weaver]

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

>From a33bc91ac1327e3bcad335bb2eb84abaf7b785cb Mon Sep 17 00:00:00 2001
From: Mark H Weaver 
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

bug#46016: broken Proof-General (emacs front-end to Coq)

[zimoun]

Hi,

On Thu, 21 Jan 2021 at 12:10, zimoun  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

bug#46016: broken Proof-General (emacs front-end to Coq)

[zimoun]

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