#605014 proofgeneral-coq: PG for coq unusable because hilit19 is missing

Package:
coq
Source:
coq
Description:
proof assistant for higher-order logic (toplevel and compiler)
Submitter:
Hendrik Tews
Date:
2022-06-14 05:57:03 UTC
Severity:
normal
#605014#5
Date:
2010-11-26 11:01:53 UTC
From:
To:
Opening any .v file or starting coq-mode manually only gives the
error

  File mode specification error: (file-error "Cannot open load file" "hilit19")

and no proof-general functionality is available. The package is
therefore completely unusable.

Bye,

Hendrik
#605014#16
Date:
2010-11-26 13:58:13 UTC
From:
To:
Hi,

sorry for the false alarm, the problem is in file
/usr/share/emacs/site-lisp/coq/coq.el from package coq, which
requires hilit19, See #605024.

The problem with proofgeneral is, that it does not install its on
bindings for *.v files on startup. Therefore one hits coq-mode
from package coq, even when proofgeneral is installed. It would
help if proofgeneral would override the broken coq bindings on
emacs startup.

Workaround: put (proofgeneral) in your .emacs or do M-x
proofgeneral before loading a .v file.

Bye,

Hendrik
#605014#17
Date:
2022-06-14 05:55:27 UTC
From:
To:
Hi,

the recent coq versions don't ship any coq for emacs file, so this bug
is now obsolete.

Cheers,

J.Puydt