Bug#605024: coq: coq.el requires nonexistent hilit19
Le 26/11/2010 15:17, Mehdi Dogguy a écrit : This seems to be fixed in Coq 8.3 (in experimental). We will try to backport a fix and ask the Release Team for an unblock. Unfortunately, the emacs mode in v8.3 has completely changed, and I cannot guarantee that it works with v8.2: tools/coq-db.el| 240 tools/coq-font-lock.el | 137 +++ tools/coq-syntax.el| 974 tools/coq.el | 58 +--- 4 files changed, 1360 insertions(+), 49 deletions(-) Cheers, -- Stéphane -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of unsubscribe. Trouble? Contact listmas...@lists.debian.org
Bug#605024: coq: coq.el requires nonexistent hilit19
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-common1.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 coqide8.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 -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of unsubscribe. Trouble? Contact listmas...@lists.debian.org
Bug#605024: coq: coq.el requires nonexistent hilit19
reassign 605014 coq reassign 582768 coq forcemerge 605024 605014 582768 thanks On 26/11/2010 14:40, Hendrik Tews wrote: 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 seems to be fixed in Coq 8.3 (in experimental). We will try to backport a fix and ask the Release Team for an unblock. This problem is wrongly attributed to proofgeneral, see #605014 and #582768. Right. I'm merging the bugreports. Regards, -- Mehdi Dogguy مهدي الدڤي http://dogguy.org/ -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of unsubscribe. Trouble? Contact listmas...@lists.debian.org
