Re: [coq] coq-mode doesn't work in emacs
Greetings! Thanks for getting in touch.
On Thursday, February 14, 2019, at 4:04 AM EST, i@ksqsf.moe wrote:
> I'm using Debian testing and I noticed that Coq-mode packaged with coq
> doesn't work [...] coq.el[c] was not found in
> /usr/share/emacs/site-lisp/coq.
>
> [...]
>
> Additional information that might be relevant:
>
> ~$ dpkg-query -W coq emacs
> coq 8.6-5
> emacs 1:26.1+1-3.2
This looks like a bug in the Coq packaging, but it’s unlikely to get fixed
per se: Upstream no longer maintains any Emacs support and has designated
Proof General (package: proofgeneral) as the preferred Emacs system for
working with Coq. This change, coming with Coq 8.9, has already been
applied to unstable and is likely to migrate to testing in the next week
or two.
I recommend investigating Proof General and seeing if it meets your needs.
If it doesn’t and you’re willing to maintain coq.el, I recommend getting
in touch with upstream (either via the coq-club mailing list or by
commenting on https://github.com/coq/coq/pull/7843). It seems like they’d
be receptive to somebody resurrecting it outside the main tree.
Hope this isn’t too disruptive,
Benjamin
PS: In the future, please consider reporting bugs to the bug tracker
instead of mailing debian-ocaml-maint directly. Just run `reportbug`, and
it’ll help you generate the report. If you have a functioning sendmail on
your machine, it’ll even submit the report for you; if not, it’ll generate
mail you can send to submit@bugs.debian.org.
Reply to: