#582768 proofgeneral: file-error "cannot open load file" "hilit19"

Package:
coq
Source:
coq
Description:
proof assistant for higher-order logic (toplevel and compiler)
Submitter:
edwin
Date:
2022-06-14 05:57:04 UTC
Severity:
normal
#582768#5
Date:
2010-05-23 13:28:28 UTC
From:
To:
I installed proofgeneral on my desktop, and it works properly (including
highlighting).
Now I install it on my laptop, and highlighting doesn't work.
Both run Debian unstable, Emacs 23.2.

Testcase:
1. proofgeneral x.v
    On my desktop it opens and highlits file properly. On my laptop it opens,
    and gives the error that it can't find 'hilit19' and doesn't highlight
    anything.
2. emacs x.v
M-x coq-mode

On both the laptop and the desktop this gives the error that 'hilit19' can't be
found.

I did a rgrep hilit19 /usr/share/emacs* on my desktop and only found coq.elc
(and some files like NEWS, AUTHORS), do I don't think hilit19 is defined on my
desktop either.
But for some reason proofgeneral works just fine without it on
the desktop, but not on the laptop.

How do I make proofgeneral work the same way as it does on my desktop?
Do I need to install additional packages?

P.S.: this bugreport was filed from the laptop, where proofgeneral doesn't work.
#582768#10
Date:
2010-05-23 13:53:23 UTC
From:
To:
Investigating further I see that my desktop has proofgeneral-coq
installed, while my laptop has proofgeneral-misc installed.

So unless I explicitly install proofgeneral-coq in the first place I get
a proofgeneral installed that doesn't work ... even if I have
apt/aptitude set to install all Recommends packages.

I think either:
 - README.Debian should mention that you must install proofgeneral-coq
explicitly to actually get something that works.
 - The "proofgeneral-misc | proofgeneral-coq" dependency should be
changed to an AND instead of an OR. aptitude won't install both, and
will always install only the first one. Which still leaves you with a
non-working proofgeneral, even if you set aptitude to install all
recommends automatically. I think that you should recommend both -misc
and -coq, so aptitude installs something that works.

Best regards,
--Edwin
#582768#21
Date:
2010-11-26 14:16:15 UTC
From:
To:
Hi,

I believe the problem is that coq-mode from package coq requires
hilit19, see #605024. I would guess that on the desktop you have
(proofgeneral) in your .emacs, while on the laptop you have not.
Therefore on the desktop *.v files get coq-mode from proofgeneral
while on the laptop they get coq-mode from package coq, which
requires the nonexistent hilit19.

Bye,

Hendrik
#582768#26
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