PG
PG copied to clipboard
ProofGeneral
Melpa fail to build
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.
Compiling file /home/hu/.emacs.d/elpa/proof-general-20181226.2300/coq/coq-syntax.el at Fri Jan 4 13:36:41 2019
Entering directory ‘/home/hu/.emacs.d/elpa/proof-general-20181226.2300/coq/’
coq-syntax.el:23:1:Error: Cannot open load file: No such file or directory, coq-db
I suppose something wrong with path config? I don't see code which add coq/ to load-path which explains this situation.
I upgraded to emacs 26.1 and this problem persists, so i guess it's a bug. I can see from the manual installation, load-path is twisted to make it work:
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml pgshell phox twelf
generic lib))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove
(quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile acl2/acl2.el
So I suppose it's a genuine bug.
Hi @HuStmpHrrr, thanks for the report! I can reproduce this with a fresh Emacs 25.1 as follows:
$ git clone https://github.com/melpa/melpa
$ cd melpa
$ make clean-packages clean-sandbox recipes/proof-general sandbox
M-x package-install RET proof-general RET
and I get 13 errors:
coq-abbrev.el:23:1:Error: Cannot open load file: No such file or directory, coq-syntax
coq-compile-common.el:27:1:Error: Cannot open load file: No such file or directory, coq-system
coq-mode.el:28:1:Error: Cannot open load file: No such file or directory, coq-smie
coq-par-compile.el:39:1:Error: Cannot open load file: No such file or directory, coq-compile-common
coq-par-test.el:33:1:Error: Cannot open load file: No such file or directory, coq-par-compile
coq-seq-compile.el:30:1:Error: Cannot open load file: No such file or directory, coq-compile-common
coq-smie.el:43:1:Error: Cannot open load file: No such file or directory, coq-indent
coq-syntax.el:23:1:Error: Cannot open load file: No such file or directory, coq-db
coq-system.el:27:1:Error: Cannot open load file: No such file or directory, coq-mode
coq.el:54:1:Error: Cannot open load file: No such file or directory, coq-system
easycrypt-abbrev.el:14:1:Error: Cannot open load file: No such file or directory, easycrypt-syntax
easycrypt-syntax.el:14:1:Error: Cannot open load file: No such file or directory, easycrypt-keywords
easycrypt.el:15:1:Error: Cannot open load file: No such file or directory, easycrypt-syntax
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
Excellent! thank you Stefan for the prompt fix :+1: I have redone the steps mentioned in my comment and it seems very OK. I guess we can close that issue. @HuStmpHrrr please reopen if ever the fix were not working with your version of emacs.
Hi @monnier @cpitclaudel, FYI Stefan's fix 58cea1b8ffb02bc546ddb56a669d4094390d4809 was not enough to make proof-general.el work in all situations (in particular with this proposed procedure, where use-package + proof-general are installed at ~/.emacs first load, I was still getting 13 bytecomp errors).
I made many intermediate tweaks between the "broken" version in master and 05df29f7ff065d8da45b81691c602b6cf075e4a0, which was working. Finally, I restored Clément's original code of pg-init.el :smiley: (renamed to proof-general.el) and it now seems to work smoothly with use-package.
(But feel free to comment if you have an explanation of what was going on there…)
Kind regards, Erik
This issue seems to have reappeared on my computer:
Compiling file /home/thirs/.emacs.d/elpa/proof-general-20220310.2253/coq/coq-syntax.el at Mon Mar 28 18:04:38 2022 coq-syntax.el:23:1:Error: Cannot open load file: No such file or directory, coq-db
Does anyone have any hints?
It looks like the above-described patch has been un-applied...
Hi. Bad news :-(. @erikmd, do you think we can add the special build of the melpa package as a test in our CI?
@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. I then tried with a fresh .emacs. I'll try again on a different computer today.
@Matafou It seems to work out of the box on the other computer.
thirs ~ $ emacs --version
GNU Emacs 27.1
Copyright (C) 2020 Free Software Foundation, Inc.
GNU Emacs comes with ABSOLUTELY NO WARRANTY.
You may redistribute copies of GNU Emacs
under the terms of the GNU General Public License.
For more information about these matters, see the file named COPYING.
thirs ~ $ uname -a
Linux lama-e29 5.10.0-10-amd64 #1 SMP Debian 5.10.84-1 (2021-12-08) x86_64 GNU/Linux
thirs ~ $ coqtop --version
The Coq Proof Assistant, version 8.12.0 (November 2020)
compiled on Nov 25 2020 6:34:32 with OCaml 4.11.1
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
async 20191009.1018 installed Asynchronous processing in Emacs
auctex 12.1.1 installed Integrated environment for *TeX*
bind-key 20210210.1609 installed A simple way to manage personal keybindings
company-coq 20220314.526 installed A collection of extensions for Proof General's Coq mode
exec-path-from-shell 20210914.1247 installed Get environment variables such as $PATH from the shell
list-utils 20160414.702 installed List-manipulation utility functions
math-symbol-lists 1.1 installed Lists of Unicode math symbols and latex commands
proof-general 20220328.1209 installed A generic Emacs interface for proof assistants
ucs-utils 20150826.714 installed Utilities for Unicode characters
use-package 20210207.1926 installed A configuration macro for simplifying your .emacs
company 20180501.11 dependency Modular text completion framework
company-math 1.1 dependency Completion backends for unicode math symbols and latex tags
dash 20180413.30 dependency A modern list library for Emacs
pcache 20170105.1414 dependency persistent caching for Emacs.
persistent-soft 20150223.1053 dependency Persistent storage, returning nil on failure
yasnippet 20180412.1548 dependency Yet another snippet extension for Emacs.
notmuch 0.35 external Emacs based front-end (MUA) for notmuch
allout 2.3 built-in extensive outline mode for use alone and with other modes
allout-widgets 1.0 built-in Visually highlight allout outline structure.
ansi-color 3.4.2 built-in translate ANSI escape sequences into faces
antlr-mode 2.2.3 built-in major mode for ANTLR grammar files
artist 1.2.6 built-in draw ascii graphics with your mouse
auth-source-pass 5.0.0 built-in Integrate auth-source with password-store
backtrace 1.0 built-in generic major mode for Elisp backtraces
bs 1.17 built-in menu for selecting and displaying buffers
cc-mode 5.33.1 built-in user customization variables for CC Mode
cedet 2.0 built-in Data structure debugger
cfengine 1.4 built-in mode for editing Cfengine files
chart 0.2 built-in Draw charts (bar charts, etc)
checkdoc 0.6.2 built-in check documentation strings for style requirements
cl-generic 1.0 built-in CLOS-style generic functions for Elisp
cl-lib 1.0 built-in Common Lisp extensions for Emacs
cl-print 1.0 built-in CL-style generic printing
cwarn 1.3.1 built-in highlight suspicious C and C++ constructions
delim-col 2.1 built-in prettify all columns in a region or rectangle
dunnet 2.2 built-in text adventure for Emacs
ebnf2ps 4.4 built-in translate an EBNF to a syntactic chart on PostScript
ede 1.2 built-in EDE utilities
ediff 2.81.6 built-in a comprehensive visual interface to diff & patch
edmacro 2.1 built-in keyboard macro editor
eieio 1.4 built-in Enhanced Implementation of Emacs Interpreted Objects
eieio-core 1.4 built-in Core implementation for eieio
epg 1.0.0 built-in the EasyPG Library
erc 5.3 built-in An Emacs Internet Relay Chat client
eshell 2.4.2 built-in the Emacs command shell
faceup 0.0.6 built-in Markup language for faces and font-lock regression testing
feedmail 11 built-in assist other email packages to massage outgoing messages
find-cmd 0.6 built-in Build a valid find(1) command with sexps
finder 1.0 built-in topic & keyword-based code finder
flymake 1.0.8 built-in A universal on-the-fly syntax checker
flymake-proc 1.0 built-in Flymake backend for external tools
foldout 1.10 built-in folding extensions for outline-mode and outline-minor-mode
footnote 0.19 built-in footnote support for message mode
gamegrid 1.2 built-in library for implementing grid-based games on Emacs
gnus 5.13 built-in Identifying spam
hippie-exp 1.6 built-in expand text trying various ways to find its expansion
htmlfontify 0.21 built-in htmlize a buffer/source tree with optional hyperlinks
icalendar 0.19 built-in iCalendar implementation
idlwave 6.1.22 built-in IDL editing mode for GNU Emacs
image-dired 0.4.11 built-in use dired to browse and manipulate your images
info-xref 3 built-in check external references in an Info document
inversion 1.3 built-in When you need something in version XX.XX
isearchb 1.5 built-in a marriage between iswitchb and isearch
js 9 built-in Major mode for editing JavaScript
json 1.4 built-in JavaScript Object Notation parser / generator
jsonrpc 1.0.9 built-in JSON-RPC library
let-alist 1.0.6 built-in Easily let-bind values of an assoc-list by their names
linum 0.9.24 built-in display line numbers in the left margin
map 2.0 built-in Map manipulation functions
master 1.0.2 built-in make a buffer the master over another buffer
md4 1.0 built-in MD4 Message Digest Algorithm.
meta-mode 1.0 built-in major mode for editing Metafont or MetaPost sources
mh-e 8.6snapshot built-in MH-E X-Face and Face header field display
mixal-mode 0.1 built-in Major mode for the mix asm language.
nadvice 1.0 built-in Light-weight advice primitives for Elisp functions
ntlm 2.1.0 built-in NTLM (NT LanManager) authentication support
org 9.3 built-in Export Framework for Org Mode
package 1.1.0 built-in Simple package system for Emacs
printing 6.9.3 built-in printing utilities
ps-mode 1.1.9 built-in PostScript mode for GNU Emacs
ps-print 7.3.5 built-in ps-print sample setup code
pulse 1.0 built-in Pulsing Overlays
python 0.26.1 built-in Python's flying circus support for Emacs
regi 1.8 built-in REGular expression Interpreting engine
remember 2.0 built-in a mode for quickly jotting down things to remember
repeat 0.51 built-in convenient way to repeat the previous command
ruby-mode 1.2 built-in Major mode for editing Ruby files
ruler-mode 1.6 built-in display a ruler in the header line
sasl 1.0 built-in SASL client framework
savehist 24 built-in Save minibuffer history
semantic 2.2 built-in GNU Bison for Emacs - Runtime
seq 2.21 built-in Sequence manipulation functions
sh-script 2.0.6 built-in shell-script editing commands for Emacs
so-long 1.0 built-in Say farewell to performance problems with minified code.
soap-client 3.1.5 built-in Interactive WSDL inspector
sql 3.6 built-in specialized comint.el for SQL interpreters
srecode 1.2 built-in Srecode texinfo support.
svg 1.0 built-in SVG image creation functions
tabulated-list 1.0 built-in generic major mode for tabulated lists
tetris 2.1 built-in implementation of Tetris for Emacs
thunk 1.0 built-in Lazy form evaluation
tildify 4.6.1 built-in adding hard spaces into texts
timeclock 2.6.1 built-in mode for keeping track of how much you work
tramp 2.4.3 built-in Transparent Remote Access, Multiple Protocol
vera-mode 2.28 built-in major mode for editing Vera files
verilog-mode 2019.12.17.268053413 built-in major mode for editing verilog source in Emacs
viper 3.14.1 built-in A full-featured Vi emulator for Emacs
wdired 2.0 built-in Rename files editing their names in dired buffers
whitespace 13.2.2 built-in minor mode to visualize TAB, (HARD) SPACE, NEWLINE
woman 0.551 built-in browse UN*X manual pages `wo (without) man'
On yesterday's computer (on which it doesn't work), it says:
auctex 13.1.1 installed Integrated environment for *TeX*
bind-key 20210210.1609 installed A simple way to manage personal keybindings
company-coq 20220314.526 installed A collection of extensions for Proof General's Coq mode
company-try-hard 20200417.1603 installed get all completions from company backends
elm-mode 20220227.931 installed Major mode for Elm
exec-path-from-shell 20210914.1247 installed Get environment variables such as $PATH from the shell
ghub 20220325.1028 installed Minuscule client libraries for Git forge APIs.
latex-unicode-math-mode 20170123.1816 installed Input method for Unicode math symbols
let-alist 1.0.6 installed Easily let-bind values of an assoc-list by their names
list-utils 20210111.1522 installed List-manipulation utility functions
math-symbol-lists 20200131.2338 installed Lists of Unicode math symbols and latex commands
modus-themes 20220329.442 installed Elegant, highly legible and customizable themes
peg 20150708.641 installed Parsing Expression Grammars in Emacs Lisp
proof-general 20220328.1209 installed A generic Emacs interface for proof assistants
ucs-utils 20150826.1414 installed Utilities for Unicode characters
use-package 20210207.1926 installed A configuration macro for simplifying your .emacs
w3m 20211122.335 installed an Emacs interface to w3m
zotelo 20160602.949 installed Manage Zotero collections from emacs
ztree 20210415.1947 installed Text mode directory tree
company 20220328.155 dependency Modular text completion framework
company-math 20210731.2019 dependency Completion backends for unicode math symbols and latex tags
dash 20210826.1149 dependency A modern list library for Emacs
f 20210624.1103 dependency Modern API for working with files and directories
pcache 20201226.634 dependency persistent caching for Emacs.
persistent-soft 20150223.1853 dependency Persistent storage, returning nil on failure
reformatter 20210831.1405 dependency Define commands which run reformatters on the current buffer
s 20210616.619 dependency The long lost Emacs string manipulation library.
seq 2.23 dependency Sequence manipulation functions
treepy 20191108.2217 dependency Generic tree traversal tools
yasnippet 20200604.246 dependency Yet another snippet extension for Emacs
caml 4.6 external OCaml code editing commands for Emacs
dash 2.17.0 external A modern list library for Emacs
dash-functional 1.2.0 external Collection of useful combinators for Emacs Lisp
epl 0.9 external Emacs Package Library
git-commit 2.99.0 external Edit Git commit messages
haskell-mode 17.2snapshot external A Haskell editing mode
htmlize 1.55 external Convert buffer text and decorations to HTML.
magit-popup 2.13.2 external Define prefix-infix-suffix command combos
org 9.4 external Outline-based notes management and organizer
transient 0.2.0.30 external Emacs key and popup interface for complex keybindings
tuareg 2.2.0 external OCaml mode for Emacs.
with-editor 3.0.2 external Use the Emacsclient as $EDITOR
allout 2.3 built-in extensive outline mode for use alone and with other modes
allout-widgets 1.0 built-in Visually highlight allout outline structure.
ansi-color 3.4.2 built-in translate ANSI escape sequences into faces
antlr-mode 2.2.3 built-in major mode for ANTLR grammar files
artist 1.2.6 built-in draw ascii graphics with your mouse
auth-source-pass 5.0.0 built-in Integrate auth-source with password-store
backtrace 1.0 built-in generic major mode for Elisp backtraces
bs 1.17 built-in menu for selecting and displaying buffers
cc-mode 5.33.1 built-in user customization variables for CC Mode
cedet 2.0 built-in Data structure debugger
cfengine 1.4 built-in mode for editing Cfengine files
chart 0.2 built-in Draw charts (bar charts, etc)
checkdoc 0.6.2 built-in check documentation strings for style requirements
cl-generic 1.0 built-in CLOS-style generic functions for Elisp
cl-lib 1.0 built-in Common Lisp extensions for Emacs
cl-print 1.0 built-in CL-style generic printing
cwarn 1.3.1 built-in highlight suspicious C and C++ constructions
delim-col 2.1 built-in prettify all columns in a region or rectangle
dunnet 2.2 built-in text adventure for Emacs
ebnf2ps 4.4 built-in translate an EBNF to a syntactic chart on PostScript
ede 1.2 built-in EDE utilities
ediff 2.81.6 built-in a comprehensive visual interface to diff & patch
edmacro 2.1 built-in keyboard macro editor
eieio 1.4 built-in Enhanced Implementation of Emacs Interpreted Objects
eieio-core 1.4 built-in Core implementation for eieio
epg 1.0.0 built-in the EasyPG Library
erc 5.3 built-in An Emacs Internet Relay Chat client
eshell 2.4.2 built-in the Emacs command shell
faceup 0.0.6 built-in Markup language for faces and font-lock regression testing
feedmail 11 built-in assist other email packages to massage outgoing messages
find-cmd 0.6 built-in Build a valid find(1) command with sexps
finder 1.0 built-in topic & keyword-based code finder
flymake 1.0.8 built-in A universal on-the-fly syntax checker
flymake-proc 1.0 built-in Flymake backend for external tools
foldout 1.10 built-in folding extensions for outline-mode and outline-minor-mode
footnote 0.19 built-in footnote support for message mode
gamegrid 1.2 built-in library for implementing grid-based games on Emacs
gnus 5.13 built-in Identifying spam
hippie-exp 1.6 built-in expand text trying various ways to find its expansion
htmlfontify 0.21 built-in htmlize a buffer/source tree with optional hyperlinks
icalendar 0.19 built-in iCalendar implementation
idlwave 6.1.22 built-in IDL editing mode for GNU Emacs
image-dired 0.4.11 built-in use dired to browse and manipulate your images
info-xref 3 built-in check external references in an Info document
inversion 1.3 built-in When you need something in version XX.XX
isearchb 1.5 built-in a marriage between iswitchb and isearch
js 9 built-in Major mode for editing JavaScript
json 1.4 built-in JavaScript Object Notation parser / generator
jsonrpc 1.0.9 built-in JSON-RPC library
let-alist 1.0.6 built-in Easily let-bind values of an assoc-list by their names
linum 0.9.24 built-in display line numbers in the left margin
map 2.0 built-in Map manipulation functions
master 1.0.2 built-in make a buffer the master over another buffer
md4 1.0 built-in MD4 Message Digest Algorithm.
meta-mode 1.0 built-in major mode for editing Metafont or MetaPost sources
mh-e 8.6snapshot built-in MH-E X-Face and Face header field display
mixal-mode 0.1 built-in Major mode for the mix asm language.
nadvice 1.0 built-in Light-weight advice primitives for Elisp functions
ntlm 2.1.0 built-in NTLM (NT LanManager) authentication support
org 9.3 built-in Export Framework for Org Mode
package 1.1.0 built-in Simple package system for Emacs
printing 6.9.3 built-in printing utilities
ps-mode 1.1.9 built-in PostScript mode for GNU Emacs
ps-print 7.3.5 built-in ps-print sample setup code
pulse 1.0 built-in Pulsing Overlays
python 0.26.1 built-in Python's flying circus support for Emacs
regi 1.8 built-in REGular expression Interpreting engine
remember 2.0 built-in a mode for quickly jotting down things to remember
repeat 0.51 built-in convenient way to repeat the previous command
ruby-mode 1.2 built-in Major mode for editing Ruby files
ruler-mode 1.6 built-in display a ruler in the header line
sasl 1.0 built-in SASL client framework
savehist 24 built-in Save minibuffer history
semantic 2.2 built-in GNU Bison for Emacs - Runtime
seq 2.21 built-in Sequence manipulation functions
sh-script 2.0.6 built-in shell-script editing commands for Emacs
so-long 1.0 built-in Say farewell to performance problems with minified code.
soap-client 3.1.5 built-in Interactive WSDL inspector
sql 3.6 built-in specialized comint.el for SQL interpreters
srecode 1.2 built-in Srecode texinfo support.
svg 1.0 built-in SVG image creation functions
tabulated-list 1.0 built-in generic major mode for tabulated lists
tetris 2.1 built-in implementation of Tetris for Emacs
thunk 1.0 built-in Lazy form evaluation
tildify 4.6.1 built-in adding hard spaces into texts
timeclock 2.6.1 built-in mode for keeping track of how much you work
tramp 2.4.3 built-in Transparent Remote Access, Multiple Protocol
vera-mode 2.28 built-in major mode for editing Vera files
verilog-mode 2019.12.17.268053413 built-in major mode for editing verilog source in Emacs
viper 3.14.1 built-in A full-featured Vi emulator for Emacs
wdired 2.0 built-in Rename files editing their names in dired buffers
whitespace 13.2.2 built-in minor mode to visualize TAB, (HARD) SPACE, NEWLINE
woman 0.551 built-in browse UN*X manual pages `wo (without) man'
proof-general 20220328.1209 obsolete A generic Emacs interface for proof assistants
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.
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? I can't reproduce here (emacs 27.1).
Not entirely, but
thirs ~ $ locate proof | grep general
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/AUTHORS
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/CHANGES
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/COPYING
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/PG-adapting.info
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/ProofGeneral.info
/home/thirs/.emacs.d/elpa/proof-general-20220328.1209/coq
seems do say so.
I tried this and I do not see any problem.
$ git clone https://github.com/melpa/melpa
$ cd melpa
$ make clean-packages clean-sandbox recipes/proof-general sandbox
M-x package-install RET proof-general RET
@erikmd @monnier do you have any clue?