[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#605024: marked as done (coq: coq.el requires nonexistent hilit19)

Your message dated Tue, 14 Jun 2022 07:55:27 +0200
with message-id <c14b06d99b3fc4eb5d20e77c6ca02125146e8e0f.camel@gmail.com>
and subject line Obsolete bug
has caused the Debian Bug report #582768,
regarding coq: coq.el requires nonexistent hilit19
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
582768: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=582768
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Package: coq
Version: 8.2.pl2+dfsg-1
Severity: normal

The file /etc/emacs/site-start.d/50coq.el sets coq-mode for *.v
files and declares coq-mode to autoload coq.el. The file
/usr/share/emacs/site-lisp/coq/coq.el however requires hilit19 in
line 140, which seems not to be available in squeeze. Therefore
loading any *.v file or starting coq-mode manually stops with the
error 

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

This problem is wrongly attributed to proofgeneral, see #605014
and #582768.


Bye,

Hendrik

-- System Information:
Debian Release: squeeze/sid
  APT prefers testing
  APT policy: (500, 'testing')
Architecture: i386 (x86_64)

Kernel: Linux 2.6.32-5-amd64 (SMP w/2 CPU cores)
Locale: LANG=en_US.UTF-8, LC_CTYPE=en_US.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/dash

Versions of packages coq depends on:
ii  coq-theories              8.2.pl2+dfsg-1 proof assistant for higher-order l
ii  emacsen-common            1.4.19         Common facilities for all emacsen
ii  libc6                     2.11.2-7       Embedded GNU C Library: Shared lib
ii  ocaml-base-nox [ocaml-bas 3.11.2-2       Runtime system for OCaml bytecode 

Versions of packages coq recommends:
ii  coqide                    8.2.pl2+dfsg-1 proof assistant for higher-order l
ii  proofgeneral-coq          3.7-4          generic interface for proof assist

Versions of packages coq suggests:
ii  coq-doc                       8.2pl1-1   documentation for Coq
ii  ledit [readline-editor]       2.01-6     line editor for interactive progra
pn  libcoq-ocaml-dev              <none>     (no description available)
ii  ocaml-nox                     3.11.2-2   ML implementation with a class-bas
ii  proofgeneral-coq              3.7-4      generic interface for proof assist
pn  why                           <none>     (no description available)

-- no debconf information

--- End Message ---
--- Begin Message --- 
Hi,

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

Cheers,

J.Puydt

--- End Message ---
Reply to: