proof-autoloads not found by Emacs

[andreas-roehler]

According to INSTALL: git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG make -C ~/.emacs.d/lisp/PG However path on my computer is not what var proof-home-directory from proof-site.el expects. This var was customized to a different value. Users might run into trouble at this point. Suggested fix: set a relative path here instead of an absolute one.

[cpitclaudel]

Can you clarify what the problem is?

[andreas-roehler]

Install from Melpa failed with the backtrace shown below.

When looking for the cause, it turned out ‘proof-home-directory’ was set to a wrong value from my custom-file.

The question is: given PG has a constant structure notwithstanding where installed from, is dealing with customized ‘proof-home-directory’ necessary? IMO it's better to hard-encode relative paths to the required packages, just setting load-path at only one occasion.

Thanks developing the great tool, Andreas

Debugger entered--Lisp error: (file-missing "Cannot open load file" "Datei oder Verzeichnis nicht gefunden" "proof-autoloads")
  require(proof-autoloads)
  eval-buffer(#<buffer  *load*-989357> nil "/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." nil t)  ; Reading at buffer position 5536
  load-with-code-conversion("/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." "/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." nil t)
  require(proof-site "/home/my-name/.emacs.d/elpa/proof-general-20200206.1...")
  (if (and (boundp 'byte-compile-current-file) byte-compile-current-file) nil (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root)))
  eval-buffer(#<buffer  *load*> nil "/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." nil t)  ; Reading at buffer position 688
  load-with-code-conversion("/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." "/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." nil t)
  load("/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." nil t)
  package--activate-autoloads-and-load-path(#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind nil :archive nil :dir "/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." :extras nil :signed nil))
  package--load-files-for-activation(#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind nil :archive nil :dir "/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." :extras nil :signed nil) :reload)
  package-activate-1(#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind nil :archive nil :dir "/home/my-name/.emacs.d/elpa/proof-general-20200206.1..." :extras nil :signed nil) :reload :deps)
  package-unpack(#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "melpa" :dir nil :extras ((:commit . "2a17093f6a7b168fedabc623602edec35aef8d8a")) :signed nil))
  #f(compiled-function (&optional good-sigs) #<bytecode 0x7475c2831a0b53f>)(nil)
  #f(compiled-function () #<bytecode -0xce7e1ce2b5047ae>)()
  package--with-response-buffer-1("https://melpa.org/packages/" #f(compiled-function () #<bytecode 0x1bfc975918533af8>) :file "proof-general-20200206.1448.tar.sig" :async nil :error-function #f(compiled-function () #<bytecode -0xce7e1ce2b5047ae>) :noerror t)
  package--check-signature("https://melpa.org/packages/" "proof-general-20200206.1448.tar" "proof-general-20200206.1448/\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0\0..." nil #f(compiled-function (&optional good-sigs) #<bytecode 0x7475c2831a0b53f>))
  #f(compiled-function () #<bytecode 0x120f606e46cb16ce>)()
  package--with-response-buffer-1("https://melpa.org/packages/" #f(compiled-function () #<bytecode 0x120f606e46cb16ce>) :file "proof-general-20200206.1448.tar" :async nil :error-function #f(compiled-function () #<bytecode 0x1e0000171e91>) :noerror nil)
  package-install-from-archive(#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "melpa" :dir nil :extras ((:commit . "2a17093f6a7b168fedabc623602edec35aef8d8a")) :signed nil))
  mapc(package-install-from-archive (#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "melpa" :dir nil :extras ((:commit . "2a17093f6a7b168fedabc623602edec35aef8d8a")) :signed nil)))
  package-download-transaction((#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "melpa" :dir nil :extras ((:commit . "2a17093f6a7b168fedabc623602edec35aef8d8a")) :signed nil)))
  package-install(#s(package-desc :name proof-general :version (20200206 1448) :summary "A generic front-end for proof assistants (interact..." :reqs ((emacs (24 3))) :kind tar :archive "melpa" :dir nil :extras ((:commit . "2a17093f6a7b168fedabc623602edec35aef8d8a")) :signed nil) nil)
  package-install-button-action(#<marker (moves after insertion) at 75 in *Help*>)
  button-activate(#<marker (moves after insertion) at 75 in *Help*> nil)
  push-button(75)
  funcall-interactively(push-button 75)
  call-interactively(push-button nil nil)
  (prog1 (call-interactively cmd record-flag keys) (if (and (symbolp cmd) (get cmd 'byte-obsolete-info) (not (get cmd 'command-execute-obsolete-warned))) (progn (put cmd 'command-execute-obsolete-warned t) (message "%s" (macroexp--obsolete-warning cmd (get cmd 'byte-obsolete-info) "command")))))
  (cond ((arrayp final) (if record-flag (progn (add-to-history 'command-history (list 'execute-kbd-macro final prefixarg) nil t))) (execute-kbd-macro final prefixarg)) (t (prog1 (call-interactively cmd record-flag keys) (if (and (symbolp cmd) (get cmd 'byte-obsolete-info) (not (get cmd 'command-execute-obsolete-warned))) (progn (put cmd 'command-execute-obsolete-warned t) (message "%s" (macroexp--obsolete-warning cmd (get cmd ...) "command")))))))
  (let ((final cmd)) (while (progn (setq final (indirect-function final)) (if (autoloadp final) (setq final (autoload-do-load final cmd))))) (cond ((arrayp final) (if record-flag (progn (add-to-history 'command-history (list 'execute-kbd-macro final prefixarg) nil t))) (execute-kbd-macro final prefixarg)) (t (prog1 (call-interactively cmd record-flag keys) (if (and (symbolp cmd) (get cmd 'byte-obsolete-info) (not (get cmd ...))) (progn (put cmd 'command-execute-obsolete-warned t) (message "%s" (macroexp--obsolete-warning cmd ... "command"))))))))
  (if (and (symbolp cmd) (get cmd 'disabled) disabled-command-function) (run-hooks 'disabled-command-function) (let ((final cmd)) (while (progn (setq final (indirect-function final)) (if (autoloadp final) (setq final (autoload-do-load final cmd))))) (cond ((arrayp final) (if record-flag (progn (add-to-history 'command-history (list ... final prefixarg) nil t))) (execute-kbd-macro final prefixarg)) (t (prog1 (call-interactively cmd record-flag keys) (if (and (symbolp cmd) (get cmd ...) (not ...)) (progn (put cmd ... t) (message "%s" ...))))))))
  (let ((prefixarg (if special nil (prog1 prefix-arg (setq current-prefix-arg prefix-arg) (setq prefix-arg nil) (if current-prefix-arg (progn (prefix-command-update))))))) (if (and (symbolp cmd) (get cmd 'disabled) disabled-command-function) (run-hooks 'disabled-command-function) (let ((final cmd)) (while (progn (setq final (indirect-function final)) (if (autoloadp final) (setq final (autoload-do-load final cmd))))) (cond ((arrayp final) (if record-flag (progn (add-to-history ... ... nil t))) (execute-kbd-macro final prefixarg)) (t (prog1 (call-interactively cmd record-flag keys) (if (and ... ... ...) (progn ... ...))))))))
  command-execute(push-button)

[andreas-roehler]

Seems to work nicely having that in my emacs-init:

(defun ar-proofgeneral-laden ()
  (interactive)
  (add-to-list 'load-path "~/.emacs.d/lisp/PG/")
  (add-to-list 'load-path "~/.emacs.d/lisp/PG/generic")
  (add-to-list 'load-path "~/.emacs.d/lisp/PG/lib")
  (require 'proof-site)
  (delete '("\\.[ds]?vh?\\'" . verilog-mode) auto-mode-alist)
  (add-to-list 'auto-mode-alist (cons (purecopy "\\.v\\'")  'coq-mode)))

(ar-proofgeneral-laden)

[andreas-roehler]

Still get the error: Error loading autoloads: (file-missing Cannot open load file Datei oder Verzeichnis nicht gefunden proof-autoloads)

IMHO proof-add-to-load-path needs to be loaded at the very beginning, i.e. from head of proof-general.el.

[Matafou]

IMO it's better to hard-encode relative paths to the required packages, just setting load-path at only one occasion.

Not sure to understand what you mean: load-path is set at only one occasion at line proof-site.el:162, making use of the proof-home-directory.

Do you know why your proof-home-directory is incorrect? It is suppose to set itself when loading the proof-site.el file (by detecting where this very file is).

[monnier]

However path here is not what var proof-home-directory from proof-site.el expects. This var was customized to a different value.

Indeed, it doesn't make sense to defer to the user's customization when we have hard evidence of where the files are. In your sample stacktrace we see that proof-site knows full well where it is (via load-file-name) but it decides to rely on the user's mistaken customization instead.

How 'bout the following patch which makes this var into a non-customizable one?

    Stefan

[Matafou]

Makes sense to me. @andreas-roehler can you explain your use case of customizing?

[andreas-roehler]

@Matafou Don't have a use-case for that - rather think at best it's redundant but a possible source of error as shown. Specifying the load-path in Emacs-init should be sufficient. Assume the customizing was left by a earlier install years ago - don't remember the precise circumstance.

[Matafou]

OK. So @monnier I don't know where your proposed patch is but I am all for it.

[monnier]

OK. So @monnier I don't know where your proposed patch is but I am all for it.

Hmm... so Github dropped my attachment? Let's see if this works better.

    Stefan

diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 7a22c9f7..54fa8abb 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -45,7 +45,7 @@

 (defun pg-autotest-find-file (file)
   "Find FILE (relative to `proof-home-directory')."
-  (let* ((name   (concat proof-home-directory file)))
+  (let* ((name   (expand-file-name file proof-home-directory)))
     (if (file-exists-p name)
    (find-file name)
       (error (format "autotest: requested file %s does not exist" name)))))
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 755d41f5..2b2454d8 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -43,7 +43,7 @@
   "<?xml-stylesheet type=\"text/xsl\" href=\"proviola-spp.xsl\"?>")

 (defun pg-movie-stylesheet-location ()
-  (concat proof-home-directory "etc/proviola/proviola-spp.xsl"))
+  (expand-file-name "etc/proviola/proviola-spp.xsl" proof-home-directory))

 (defvar pg-movie-frame 0 "Frame counter for movie.")
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 5fb9cdb8..0efd9506 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -114,34 +114,29 @@
 ;; Load path must be extended manually during compilation.
 ;;

-(defun proof-home-directory-fn ()
-  "Used to set `proof-home-directory'."
-  (let ((s (getenv  "PROOFGENERAL_HOME")))
-    (if s
-   (if (string-match "/$" s) s (concat s "/"))
-      (let ((curdir
-        (or
-         (and load-in-progress (file-name-directory load-file-name))
-         (file-name-directory (buffer-file-name)))))
-   (file-name-directory (substring curdir 0 -1))))))
-
-(defcustom proof-home-directory
-  (proof-home-directory-fn)
-  "Directory where Proof General is installed.  Ends with slash.
-Default value taken from environment variable `PROOFGENERAL_HOME' if set,
-otherwise based on where the file `proof-site.el' was loaded from.
-You can use customize to set this variable."
-  :type 'directory
-  :group 'proof-general-internals)
+(defconst proof-home-directory
+  (let ((curfile
+    (or
+     (and load-in-progress load-file-name)
+     buffer-file-name)))
+    (if curfile
+        (file-name-directory (directory-file-name
+                              (file-name-directory curfile)))
+      (let ((s (getenv "PROOFGENERAL_HOME")))
+   (if s (file-name-as-directory s)))))
+  "Directory where Proof General is installed.
+based on where the file `proof-site.el' was loaded from.
+Falls back to consulting the environment variable `PROOFGENERAL_HOME' if
+proof-site.el couldn't know where it was executed from.")

 (defcustom proof-images-directory
-  (concat proof-home-directory "images/")
+  (expand-file-name "images/" proof-home-directory)
     "Where Proof General image files are installed.  Ends with slash."
   :type 'directory
   :group 'proof-general-internals)

 (defcustom proof-info-directory
-  (concat proof-home-directory "doc/")
+  (expand-file-name "doc/" proof-home-directory)
   "Where Proof General Info files are installed.  Ends with slash."
   :type 'directory
   :group 'proof-general-internals)
@@ -159,8 +154,8 @@ You can use customize to set this variable."
   "Add DIR to `load-path' if not contained already."
   (add-to-list 'load-path dir))

-(proof-add-to-load-path (concat proof-home-directory "generic/"))
-(proof-add-to-load-path (concat proof-home-directory "lib/"))
+(proof-add-to-load-path (expand-file-name "generic/" proof-home-directory))
+(proof-add-to-load-path (expand-file-name "lib/" proof-home-directory))

 ;; Declare some global variables and autoloads
@@ -184,12 +179,12 @@ You can use customize to set this variable."

 (defcustom proof-assistant-table
   (apply
-   'append
+   #'append
    (mapcar
     ;; Discard entries whose directories have been removed.
     (lambda (dne)
-      (let ((atts (file-attributes (concat proof-home-directory
-                      (symbol-name (car dne))))))
+      (let ((atts (file-attributes (expand-file-name (symbol-name (car dne))
+                                proof-home-directory))))
    (if (and atts (eq 't (car atts)))
        (list dne)
      nil)))
@@ -342,12 +337,11 @@ the Lisp variable `proof-assistants', or the contents of `proof-assistant-table'
   "Visit a standardly named example file for prover PROVER."
   (interactive
    (list (proof-chose-prover "Visit example file for prover: ")))
-  (find-file (concat proof-home-directory
-            prover "/example."
-            (nth 2 (assoc (intern prover) proof-assistant-table-default)))))
-
-
-
+  (find-file (expand-file-name
+         (concat prover "/example."
+             (nth 2 (assoc (intern prover)
+                           proof-assistant-table-default)))
+         proof-home-directory)))

 (provide 'proof-site)

[Matafou]

Thanks! Should we make also proof-info-directory and proof-images-directory or do you see use cases where these need to be customizable?

[monnier]

Should we make also proof-info-directory and proof-images-directory or do you see use cases where these need to be customizable?

I have no opinion on that. I would keep them as defvars but I don't see why we should encourage end-users to mess with them via Customize.

[andreas-roehler]

@monnier +1