Melpa fail to build #413
Labels
Comments
|
I upgraded to emacs 26.1 and this problem persists, so i guess it's a bug. I can see from the manual installation, So I suppose it's a genuine bug. |
|
Hi @HuStmpHrrr, thanks for the report! and I get 13 errors: I suspect this issue comes from the recent cleanup by @monnier but I did not investigate this further… This is a bit unfortunate as one of my courses in Toulouse should start using Emacs+PG from next Monday :/ Cc @ProofGeneral/core |
monnier
added a commit
that referenced
this issue
Jan 13, 2019
* generic/pg-user.el (proof-add-completions): `proof-assistant` can also be the empty string :-(
|
I think I found the culprit. I just pushed a patch that should fix it.
|
|
Excellent! thank you Stefan for the prompt fix 👍 |
erikmd
added a commit
that referenced
this issue
Jan 13, 2019
The previous code raised some bytecomp errors when loading a ~/.emacs
containing a bootstrapped use-package proof-general config., such as:
```
(require 'package)
(let* ((no-ssl (and (memq system-type '(windows-nt ms-dos))
(not (gnutls-available-p))))
(proto (if no-ssl "http" "https")))
(add-to-list 'package-archives
(cons "melpa" (concat proto "://melpa.org/packages/")) t))
(package-initialize)
;; Bootstrap use-package
(unless (package-installed-p 'use-package)
(package-refresh-contents)
(package-install 'use-package))
(eval-when-compile
(require 'use-package))
(use-package proof-general
:ensure t
:mode ("\\.v\\'" . coq-mode))
```
|
Hi @monnier @cpitclaudel, FYI Stefan's fix 58cea1b was not enough to make |
|
I installed PG from melpa again and it worked. |
|
This issue seems to have reappeared on my computer:
It looks like the above-described patch has been un-applied... |
|
Hi. Bad news :-(. |
|
@thirs can you describe the procedure to obtain this error? Is it when installing the elpa package? |
|
Yes, I think I just installed it via melpa, followed the "quick installation instructions" on the website, and tried to open some ".v" file. |
|
@Matafou It seems to work out of the box on the other computer. Previous computer had the same except for Debian 5.10.103-1 (2022-03-07). |
|
@Matafou I forgot to look up the version numbers of the elpa package: on the first machine it was 20220310.2253, while it is 20220328.1209 on the other. So I tried the newer version on the first machine, and it also doesn't work. So I guess it has to do with emacs configuration, right? What should I look for? On today's computer, melpa says On yesterday's computer (on which it doesn't work), it says: Weird: proof-general is there twice, once as installed, once as obsolete, with the same version. But installation failed so I guess this is more a consequence of the failure than a cause. |
You sure you don't have any other remaining part from an older installation of proofgeneral? |
|
Not entirely, but seems do say so. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
MELPA dist seems to fail on my machine. In particular, paths seem badly configured. For instance, all files in
coq/fail to compile if they have local dependencies, e.g.coq-syntax.el. If I compile this file, it generates the following messages.I suppose something wrong with path config? I don't see code which add
coq/toload-pathwhich explains this situation.The text was updated successfully, but these errors were encountered: