Closed manuel-uberti closed 5 years ago
Hi @manuel-uberti, thanks for your detailed report! I can't reproduce it with GNU Emacs 25.1.1 + MELPA + use-package... I did not test yet with the Emacs version you mention, BTW I see that you are using a bleeding edge version of Emacs ;) which was not tested by our Travis CI config.
Several questions:
.v
file? (because the error precisely seems to occur because proof-assistant-symbol
is nil
, while this variable should be set to coq
or so, at loading time when opening a .v
file...)proof-general
package directly using M-x package install
etc., rather than relying on use-package
?To answer you questions:
emacs -Q
using M-x package-install
, and it workedI guess it's something related to my configuration. I had PG already set up using the "old way" (cloning the repository, etc.). It must be something related to that, I suppose.
Hi, please let us know if this is due to an old install of pg, because probably a lot of people will also have that when they switch to melpa...
Meanwhile, removing it and reinstalling it from MELPA gives this:
Debugger entered--Lisp error: (error "Already loaded")
signal(error ("Already loaded"))
error("Already loaded")
(if (featurep 'proof-autoloads) (error "Already loaded"))
#<subr eval-buffer>(#<buffer *load*> nil "/home/manuel/.emacs.d/elpa/proof-general-20180825...." nil t)
apply(#<subr eval-buffer> (#<buffer *load*> nil "/home/manuel/.emacs.d/elpa/proof-general-20180825...." nil t))
eval-buffer(#<buffer *load*> nil "/home/manuel/.emacs.d/elpa/proof-general-20180825...." nil t) ; Reading at buffer position 562
load-with-code-conversion("/home/manuel/.emacs.d/elpa/proof-general-20180825...." "/home/manuel/.emacs.d/elpa/proof-general-20180825...." nil t)
#<subr load>("/home/manuel/.emacs.d/elpa/proof-general-20180825...." nil t nil nil)
apply(#<subr load> ("/home/manuel/.emacs.d/elpa/proof-general-20180825...." nil t))
load("/home/manuel/.emacs.d/elpa/proof-general-20180825...." nil t)
(closure ((loaded-files-list "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." "/home/manuel/.emacs.d/elpa/proof-general-20..." ...) (reload . :reload) (pkg-desc . #s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (i..." :reqs ((emacs ...)) :kind nil :archive nil :dir "/home/manuel/.emacs.d/elpa/proof-general-20..." :extras nil :signed nil)) Info-directory-list cl-struct-package--bi-desc-tags cl-struct-package-desc-tags t) (feature) (load feature nil t))("/home/manuel/.emacs.d/elpa/proof-general-20180825....")
mapc((closure ((loaded-files-list "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." ...) (reload . :reload) (pkg-desc . #s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (in..." :reqs ((emacs ...)) :kind nil :archive nil :dir "/home/manuel/.emacs.d/elpa/proof-general-201..." :extras nil :signed nil)) Info-directory-list cl-struct-package--bi-desc-tags cl-struct-package-desc-tags t) (feature) (load feature nil t)) ("/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." "/home/manuel/.emacs.d/elpa/proof-general-201..." ...))
(condition-case err (mapc #'(lambda (feature) (load feature nil t)) (remove (file-truename (package--autoloads-file-name pkg-desc)) loaded-files-list)) ((debug error) (message "Error in package--load-files-for-activation: %s" err) nil))
(let* ((loaded-files-list (if reload (progn (package--list-loaded-files (progn (or ... ...) (aref pkg-desc 7))))))) (package--activate-autoloads-and-load-path pkg-desc) (condition-case err (mapc #'(lambda (feature) (load feature nil t)) (remove (file-truename (package--autoloads-file-name pkg-desc)) loaded-files-list)) ((debug error) (message "Error in package--load-files-for-activation: %s" err) nil)))
package--load-files-for-activation(#s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind nil :archive nil :dir "/home/manuel/.emacs.d/elpa/proof-general-20180825...." :extras nil :signed nil) :reload)
(if (listp package--quickstart-pkgs) (setq package--quickstart-pkgs (cons pkg-desc package--quickstart-pkgs)) (package--load-files-for-activation pkg-desc reload))
(catch 'exit (if deps (progn (let ((--dolist-tail-- (progn (or ... ...) (aref pkg-desc 4)))) (while --dolist-tail-- (let ((req ...)) (if (package-activate ...) nil (message "Unable to activate package `%s'.\nRequired package ..." name ... ...) (throw ... nil)) (setq --dolist-tail-- (cdr --dolist-tail--))))))) (if (listp package--quickstart-pkgs) (setq package--quickstart-pkgs (cons pkg-desc package--quickstart-pkgs)) (package--load-files-for-activation pkg-desc reload)) (if (file-exists-p (expand-file-name "dir" pkg-dir)) (progn (require 'info) (info-initialize) (setq Info-directory-list (cons pkg-dir Info-directory-list)))) (setq package-activated-list (cons name package-activated-list)) t)
(let* ((name (progn (or (and (memq (type-of pkg-desc) cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list 'package-desc pkg-desc))) (aref pkg-desc 1))) (pkg-dir (progn (or (and (memq (type-of pkg-desc) cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list 'package-desc pkg-desc))) (aref pkg-desc 7)))) (if pkg-dir nil (error "Internal error: unable to find directory for `%s'" (package-desc-full-name pkg-desc))) (catch 'exit (if deps (progn (let ((--dolist-tail-- (progn ... ...))) (while --dolist-tail-- (let (...) (if ... nil ... ...) (setq --dolist-tail-- ...)))))) (if (listp package--quickstart-pkgs) (setq package--quickstart-pkgs (cons pkg-desc package--quickstart-pkgs)) (package--load-files-for-activation pkg-desc reload)) (if (file-exists-p (expand-file-name "dir" pkg-dir)) (progn (require 'info) (info-initialize) (setq Info-directory-list (cons pkg-dir Info-directory-list)))) (setq package-activated-list (cons name package-activated-list)) t))
package-activate-1(#s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind nil :archive nil :dir "/home/manuel/.emacs.d/elpa/proof-general-20180825...." :extras nil :signed nil) :reload :deps)
(if (package-activate-1 new-desc :reload :deps) (progn (package--compile new-desc) (package--load-files-for-activation new-desc :reload)))
(let ((new-desc (package-load-descriptor pkg-dir))) (if (equal (package-desc-full-name new-desc) (package-desc-full-name pkg-desc)) nil (error "The retrieved package (`%s') doesn't match what th..." (package-desc-full-name new-desc) (package-desc-full-name pkg-desc))) (if (package-activate-1 new-desc :reload :deps) (progn (package--compile new-desc) (package--load-files-for-activation new-desc :reload))))
(let* ((name (progn (or (and (memq (type-of pkg-desc) cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list 'package-desc pkg-desc))) (aref pkg-desc 1))) (dirname (package-desc-full-name pkg-desc)) (pkg-dir (expand-file-name dirname package-user-dir))) (let* ((val (progn (or (and (memq ... cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list ... pkg-desc))) (aref pkg-desc 5)))) (cond ((eq val 'dir) (make-directory pkg-dir t) (let ((file-list (directory-files default-directory ... "\\`[^.].*\\.el\\'" ...))) (let ((--dolist-tail-- file-list)) (while --dolist-tail-- (let ... ... ...))) (progn (or (and ... t) (signal ... ...)) (let* (...) (aset v 5 ...))))) ((eq val 'tar) (make-directory package-user-dir t) (let* ((default-directory (file-name-as-directory package-user-dir))) (package-untar-buffer dirname))) ((eq val 'single) (let ((el-file (expand-file-name ... pkg-dir))) (make-directory pkg-dir t) (package--write-file-no-coding el-file))) (t (let ((kind val)) (error "Unknown package kind: %S" kind))))) (package--make-autoloads-and-stuff pkg-desc pkg-dir) (let ((new-desc (package-load-descriptor pkg-dir))) (if (equal (package-desc-full-name new-desc) (package-desc-full-name pkg-desc)) nil (error "The retrieved package (`%s') doesn't match what th..." (package-desc-full-name new-desc) (package-desc-full-name pkg-desc))) (if (package-activate-1 new-desc :reload :deps) (progn (package--compile new-desc) (package--load-files-for-activation new-desc :reload)))) pkg-dir)
package-unpack(#s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "MELPA" :dir nil :extras ((:stars) (:commit . "69066bf2cb97d6df74a069c3e90155e43353a2a0")) :signed nil))
(let ((save-silently t)) (package-unpack pkg-desc))
(progn (insert content) (let ((save-silently t)) (package-unpack pkg-desc)))
(unwind-protect (progn (insert content) (let ((save-silently t)) (package-unpack pkg-desc))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))
(save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (insert content) (let ((save-silently t)) (package-unpack pkg-desc))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))
(let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (insert content) (let ((save-silently t)) (package-unpack pkg-desc))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))
(closure ((content . "proof-general-20180825.1627/\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0...") (temp-buffer . #<buffer *temp*>) (url . "https://melpa.org/packages/proof-general-20180825....") (url-1 . "https://melpa.org/packages/") (file . "proof-general-20180825.1627.tar") (location . "https://melpa.org/packages/") (pkg-desc . #s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "MELPA" :dir nil :extras ((:stars) (:commit . "69066bf2cb97d6df74a069c3e90155e43353a2a0")) :signed nil)) package-quickstart-file cl-struct-package--ac-desc-tags warning-minimum-level autoload-timestamps generated-autoload-file tar-parse-info Info-directory-list cl-struct-package--bi-desc-tags cl-struct-package-desc-tags t) (&optional good-sigs) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (insert content) (let (...) (package-unpack pkg-desc))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (if good-sigs (progn (write-region (mapconcat #'epg-signature-to-string good-sigs "\n") nil (expand-file-name (concat (package-desc-full-name pkg-desc) ".signed") package-user-dir) nil 'silent) (progn (or (and (memq ... cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list ... pkg-desc))) (let* ((v pkg-desc)) (aset v 9 t))) (let* ((pkg-descs (and t ...))) (if pkg-descs (progn (or ... ...) (let* ... ...)))))))(nil)
funcall((closure ((content . "proof-general-20180825.1627/\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0...") (temp-buffer . #<buffer *temp*>) (url . "https://melpa.org/packages/proof-general-20180825....") (url-1 . "https://melpa.org/packages/") (file . "proof-general-20180825.1627.tar") (location . "https://melpa.org/packages/") (pkg-desc . #s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "MELPA" :dir nil :extras ((:stars) (:commit . "69066bf2cb97d6df74a069c3e90155e43353a2a0")) :signed nil)) package-quickstart-file cl-struct-package--ac-desc-tags warning-minimum-level autoload-timestamps generated-autoload-file tar-parse-info Info-directory-list cl-struct-package--bi-desc-tags cl-struct-package-desc-tags t) (&optional good-sigs) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (insert content) (let (...) (package-unpack pkg-desc))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (if good-sigs (progn (write-region (mapconcat #'epg-signature-to-string good-sigs "\n") nil (expand-file-name (concat (package-desc-full-name pkg-desc) ".signed") package-user-dir) nil 'silent) (progn (or (and (memq ... cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list ... pkg-desc))) (let* ((v pkg-desc)) (aset v 9 t))) (let* ((pkg-descs (and t ...))) (if pkg-descs (progn (or ... ...) (let* ... ...))))))) nil)
(progn (funcall callback nil))
(if (and callback allow-unsigned) (progn (funcall callback nil)))
(let ((allow-unsigned (eq package-check-signature 'allow-unsigned))) (if (and callback allow-unsigned) (progn (funcall callback nil))) (if unwind (progn (funcall unwind))) (if allow-unsigned nil (error "Unsigned file `%s' at %s" file location)))
(condition-case err (progn (url-insert-file-contents url) t) (error (let ((allow-unsigned (eq package-check-signature 'allow-unsigned))) (if (and callback allow-unsigned) (progn (funcall callback nil))) (if unwind (progn (funcall unwind))) (if allow-unsigned nil (error "Unsigned file `%s' at %s" file location))) (if t nil (signal (car err) (cdr err)))))
(if (condition-case err (progn (url-insert-file-contents url) t) (error (let ((allow-unsigned (eq package-check-signature 'allow-unsigned))) (if (and callback allow-unsigned) (progn (funcall callback nil))) (if unwind (progn (funcall unwind))) (if allow-unsigned nil (error "Unsigned file `%s' at %s" file location))) (if t nil (signal (car err) (cdr err))))) (progn (unwind-protect (let ((sig (package--check-signature-content (buffer-substring ... ...) string sig-file))) (if callback (progn (funcall callback sig))) sig) (if unwind (progn (funcall unwind))))))
(progn (if (condition-case err (progn (url-insert-file-contents url) t) (error (let ((allow-unsigned (eq package-check-signature ...))) (if (and callback allow-unsigned) (progn (funcall callback nil))) (if unwind (progn (funcall unwind))) (if allow-unsigned nil (error "Unsigned file `%s' at %s" file location))) (if t nil (signal (car err) (cdr err))))) (progn (unwind-protect (let ((sig (package--check-signature-content ... string sig-file))) (if callback (progn (funcall callback sig))) sig) (if unwind (progn (funcall unwind)))))))
(unwind-protect (progn (if (condition-case err (progn (url-insert-file-contents url) t) (error (let ((allow-unsigned ...)) (if (and callback allow-unsigned) (progn ...)) (if unwind (progn ...)) (if allow-unsigned nil (error "Unsigned file `%s' at %s" file location))) (if t nil (signal (car err) (cdr err))))) (progn (unwind-protect (let ((sig ...)) (if callback (progn ...)) sig) (if unwind (progn (funcall unwind))))))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))
(save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn (url-insert-file-contents url) t) (error (let (...) (if ... ...) (if unwind ...) (if allow-unsigned nil ...)) (if t nil (signal ... ...)))) (progn (unwind-protect (let (...) (if callback ...) sig) (if unwind (progn ...)))))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))
(let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn (url-insert-file-contents url) t) (error (let ... ... ... ...) (if t nil ...))) (progn (unwind-protect (let ... ... sig) (if unwind ...))))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))
(if async (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn ... t) (error ... ...)) (progn))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn ... t) (error ... ...)) (progn (unwind-protect ... ...)))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))
(let ((url (concat url-1 sig-file))) (if async (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err ... ...) (progn))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err ... ...) (progn ...))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))))
(if (string-match-p "\\`https?:" url-1) (let ((url (concat url-1 sig-file))) (if async (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if ... ...)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if ... ...)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn ... t) (error ... ...)) (progn (unwind-protect ... ...)))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))
(let* ((url-1 location)) (if (string-match-p "\\`https?:" url-1) (let ((url (concat url-1 sig-file))) (if async (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn ...) (and ... ...)))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn ...) (and ... ...)))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err ... ...) (progn ...))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))))
(let ((sig-file (concat file ".sig")) (string (or string (buffer-string)))) (let* ((url-1 location)) (if (string-match-p "\\`https?:" url-1) (let ((url (concat url-1 sig-file))) (if async (let ((temp-buffer ...)) (save-current-buffer (set-buffer temp-buffer) (unwind-protect ... ...))) (let ((temp-buffer ...)) (save-current-buffer (set-buffer temp-buffer) (unwind-protect ... ...))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if ... ...)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))))
package--check-signature("https://melpa.org/packages/" "proof-general-20180825.1627.tar" "proof-general-20180825.1627/\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0..." nil (closure ((content . "proof-general-20180825.1627/\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0...") (temp-buffer . #<buffer *temp*>) (url . "https://melpa.org/packages/proof-general-20180825....") (url-1 . "https://melpa.org/packages/") (file . "proof-general-20180825.1627.tar") (location . "https://melpa.org/packages/") (pkg-desc . #s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "MELPA" :dir nil :extras ((:stars) (:commit . "69066bf2cb97d6df74a069c3e90155e43353a2a0")) :signed nil)) package-quickstart-file cl-struct-package--ac-desc-tags warning-minimum-level autoload-timestamps generated-autoload-file tar-parse-info Info-directory-list cl-struct-package--bi-desc-tags cl-struct-package-desc-tags t) (&optional good-sigs) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (insert content) (let (...) (package-unpack pkg-desc))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (if good-sigs (progn (write-region (mapconcat #'epg-signature-to-string good-sigs "\n") nil (expand-file-name (concat (package-desc-full-name pkg-desc) ".signed") package-user-dir) nil 'silent) (progn (or (and (memq ... cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list ... pkg-desc))) (let* ((v pkg-desc)) (aset v 9 t))) (let* ((pkg-descs (and t ...))) (if pkg-descs (progn (or ... ...) (let* ... ...))))))))
(let ((content (buffer-string))) (package--check-signature location file content nil #'(lambda (&optional good-sigs) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn ... ...) (and ... ...)))) (if good-sigs (progn (write-region (mapconcat ... good-sigs "\n") nil (expand-file-name ... package-user-dir) nil 'silent) (progn (or ... ...) (let* ... ...)) (let* (...) (if pkg-descs ...)))))))
(if (or (not package-check-signature) (member (progn (or (and (memq (type-of pkg-desc) cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list 'package-desc pkg-desc))) (aref pkg-desc 6)) package-unsigned-archives)) (let ((save-silently t)) (package-unpack pkg-desc)) (let ((content (buffer-string))) (package--check-signature location file content nil #'(lambda (&optional good-sigs) (let ((temp-buffer ...)) (save-current-buffer (set-buffer temp-buffer) (unwind-protect ... ...))) (if good-sigs (progn (write-region ... nil ... nil ...) (progn ... ...) (let* ... ...)))))))
(progn (if (or (not package-check-signature) (member (progn (or (and (memq ... cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list ... pkg-desc))) (aref pkg-desc 6)) package-unsigned-archives)) (let ((save-silently t)) (package-unpack pkg-desc)) (let ((content (buffer-string))) (package--check-signature location file content nil #'(lambda (&optional good-sigs) (let (...) (save-current-buffer ... ...)) (if good-sigs (progn ... ... ...)))))))
(if (condition-case err (progn (url-insert-file-contents url) t) (error nil (if nil nil (signal (car err) (cdr err))))) (progn (if (or (not package-check-signature) (member (progn (or (and ... t) (signal ... ...)) (aref pkg-desc 6)) package-unsigned-archives)) (let ((save-silently t)) (package-unpack pkg-desc)) (let ((content (buffer-string))) (package--check-signature location file content nil #'(lambda (&optional good-sigs) (let ... ...) (if good-sigs ...)))))))
(progn (if (condition-case err (progn (url-insert-file-contents url) t) (error nil (if nil nil (signal (car err) (cdr err))))) (progn (if (or (not package-check-signature) (member (progn (or ... ...) (aref pkg-desc 6)) package-unsigned-archives)) (let ((save-silently t)) (package-unpack pkg-desc)) (let ((content (buffer-string))) (package--check-signature location file content nil #'(lambda ... ... ...)))))))
(unwind-protect (progn (if (condition-case err (progn (url-insert-file-contents url) t) (error nil (if nil nil (signal (car err) (cdr err))))) (progn (if (or (not package-check-signature) (member (progn ... ...) package-unsigned-archives)) (let ((save-silently t)) (package-unpack pkg-desc)) (let ((content ...)) (package--check-signature location file content nil #'...)))))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))
(save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn (url-insert-file-contents url) t) (error nil (if nil nil (signal ... ...)))) (progn (if (or (not package-check-signature) (member ... package-unsigned-archives)) (let (...) (package-unpack pkg-desc)) (let (...) (package--check-signature location file content nil ...)))))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))
(let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn (url-insert-file-contents url) t) (error nil (if nil nil ...))) (progn (if (or ... ...) (let ... ...) (let ... ...))))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))
(if nil (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn ... t) (error nil ...)) (progn))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn ... t) (error nil ...)) (progn (if ... ... ...)))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))
(let ((url (concat url-1 file))) (if nil (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err ... ...) (progn))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err ... ...) (progn ...))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))))
(if (string-match-p "\\`https?:" url-1) (let ((url (concat url-1 file))) (if nil (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if ... ...)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if ... ...)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err (progn ... t) (error nil ...)) (progn (if ... ... ...)))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))
(let* ((url-1 location)) (if (string-match-p "\\`https?:" url-1) (let ((url (concat url-1 file))) (if nil (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn ...) (and ... ...)))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn ...) (and ... ...)))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if (condition-case err ... ...) (progn ...))) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))))
(let* ((location (package-archive-base pkg-desc)) (file (concat (package-desc-full-name pkg-desc) (package-desc-suffix pkg-desc)))) (let* ((url-1 location)) (if (string-match-p "\\`https?:" url-1) (let ((url (concat url-1 file))) (if nil (let ((temp-buffer ...)) (save-current-buffer (set-buffer temp-buffer) (unwind-protect ... ...))) (let ((temp-buffer ...)) (save-current-buffer (set-buffer temp-buffer) (unwind-protect ... ...))))) (let ((temp-buffer (generate-new-buffer " *temp*"))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if ... ...)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))))
package-install-from-archive(#s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "MELPA" :dir nil :extras ((:stars) (:commit . "69066bf2cb97d6df74a069c3e90155e43353a2a0")) :signed nil))
mapc(package-install-from-archive (#s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "MELPA" :dir nil :extras ((:stars) (:commit . "69066bf2cb97d6df74a069c3e90155e43353a2a0")) :signed nil)))
package-download-transaction((#s(package-desc :name proof-general :version (20180825 1627) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "MELPA" :dir nil :extras ((:stars) (:commit . "69066bf2cb97d6df74a069c3e90155e43353a2a0")) :signed nil)))
(progn (package-download-transaction transaction) (package--quickstart-maybe-refresh))
(if transaction (progn (package-download-transaction transaction) (package--quickstart-maybe-refresh)) (message "`%s' is already installed" name))
(let* ((transaction (and t (if (and (memq (type-of pkg) cl-struct-package-desc-tags) t) (if (package-installed-p pkg) nil (package-compute-transaction (list pkg) (progn ... ...))) (package-compute-transaction nil (list (list pkg))))))) (if transaction (progn (package-download-transaction transaction) (package--quickstart-maybe-refresh)) (message "`%s' is already installed" name)))
(let ((name (if (and (memq (type-of pkg) cl-struct-package-desc-tags) t) (progn (or (and (memq ... cl-struct-package-desc-tags) t) (signal 'wrong-type-argument (list ... pkg))) (aref pkg 1)) pkg))) (if (or dont-select (package--user-selected-p name)) nil (package--save-selected-packages (cons name package-selected-packages))) (let* ((transaction (and t (if (and (memq ... cl-struct-package-desc-tags) t) (if (package-installed-p pkg) nil (package-compute-transaction ... ...)) (package-compute-transaction nil (list ...)))))) (if transaction (progn (package-download-transaction transaction) (package--quickstart-maybe-refresh)) (message "`%s' is already installed" name))))
package-install(proof-general)
use-package-ensure-elpa(proof-general (t) nil)
#<subr eval-region>(207 311 t #f(compiled-function (ignore) #<bytecode 0x20d4b55>))
apply(#<subr eval-region> (207 311 t #f(compiled-function (ignore) #<bytecode 0x20d4b55>)))
eval-region(207 311 t #f(compiled-function (ignore) #<bytecode 0x20d4b55>)) ; Reading at buffer position 302
elisp--eval-defun()
eval-defun(nil)
eros-eval-defun(nil)
funcall-interactively(eros-eval-defun nil)
call-interactively(eros-eval-defun nil nil)
command-execute(eros-eval-defun)
If this is unrelated, I can open another issue.
@Matafou sorry for the late reply, but yes, it seems related to my configuration, because as I stated with emacs -Q
I can install it from MELPA with no issues.
Sorry guys, any hint wrt to the above "Already loaded" error? I'm not able to uninstall/reinstall proof-general
at the moment.
Are you sure there is no manually installed pg anywhere in your config? The only reason for this Is can think of is that you still have a (load "...proof-site.el") somewhere.
Can you try bisecting your config? It would be nice to see what causes it.
This is the results of running rg
in my .emacs.d
:
manuel@elle:~/.emacs.d$ rg proof
lisp/mu-coq.el
11:(use-package proof-general ; Generic interface for proof assistants
22: (setq-default proof-silence-compatibility-warning t
23: proof-splash-enable nil
24: proof-three-window-mode-policy 'hybrid
37: (bind-key "C-c RET" #'company-coq-proof-goto-point company-coq-map)))
Without looking into elpa
directory, of course.
Do you have anything in your ~/.emacs?
I don't have a ~/.emacs
. :)
I meant commenting things out of your config until the error goes away, or conversely commenting it all out and adding things back in progressively. If it works with emacs -Q, it must be possible to isolate one or two faulty lines in your config that cause this issue.
I think I found it. This is what I did:
proof-general
package with M-x package-delete
init.el
: (package-activate-all)
~/.emacs.d/early-init.el
(setq package-enable-at-startup nil)
at the top of my init.el
right after (require 'package)
proof-general
This seems to work fine.
This is a bit odd. You seem to be on Emacs master, but there package-activate-all is already called automatically, and you don't need to (require 'package)
any more, do you? Setting package-enable-at-startup
in your init.el probably doesn't do anything, either, does it?
Another thing: could you post a copy of the error message without the ...
abbreviations? I'd like to understand why package.el is loading all these files.
If I don't use (require 'package)
, where should I put this?
(setq package-archives
'(("GNU ELPA" . "http://elpa.gnu.org/packages/")
("MELPA" . "https://melpa.org/packages/")
("ORG" . "https://orgmode.org/elpa/")))
Furthermore, without package-activate-all
I get this:
Warning (initialization): An error occurred while loading ‘/home/manuel/.emacs.d/init.el’:
error: package.el is not yet initialized!
To ensure normal operation, you should investigate and remove the
cause of the error in your initialization file. Start Emacs with
the ‘--debug-init’ option to view a complete error backtrace.
Hmm emacs27 has a new startup sequence if I understood well.
I think early-init.el
is where you should configure package-archives
. It is loaded before packages initialization.
Yes, but I still have to add (require 'package)
before package-archives
configuration, otherwise it doesn't work.
Ok, with the following setup I am able to install proof-general
from MELPA.
In ~/.emacs.d/early-init.el
:
(require 'package)
(setq package-archives
'(("GNU ELPA" . "https://elpa.gnu.org/packages/")
("MELPA" . "https://melpa.org/packages/")
("ORG" . "https://orgmode.org/elpa/")))
(provide 'early-init)
In ~/.emacs.d/init.el
I have now nothing related to packages configuration.
Looks like we can close this issue now. Thanks for the support, guys.
Thanks @manuel-uberti for your feedback! As an aside, I've noticed in your previous comment that you have an extra key-binding config that might now be unnecessary, due to #228.
Fantastic, thanks!
Hi,
now that
proof-general
is available on MELPA, I am trying to install it like this:However, this is what I get:
Some extra details about my system, in case you need it:
If you need me to do more tests to further debug the problem, feel free to ask.