coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Company-coq possible issue?

From: Merlin Göttlinger <megoettlinger AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Company-coq possible issue?
Date: Tue, 31 Oct 2017 22:01:53 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f178.google.com
Ironport-phdr: 9a23:PKU37RUrNdwAj+mDSpR25LhmeybV8LGtZVwlr6E/grcLSJyIuqrYZRKDt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl9+If2wEYrPhey20fqz8tvdeVZmnj24NJZ/NhG3qzL+KNUKhYpkJasrgk/Mr3RPdvhKwWJuKl+Jtxn578a0upVk9nID6Loa68dcXPCiLOwDRrtCAWF+Pg==

This seems to be similar to this issue:

https://github.com/cpitclaudel/company-coq/issues/126

I used this line in my init.el as a workaround:

https://gitlab.com/mgttlinger/dotfiles/blob/master/.emacs.d/init.el#L224

Cheers,

Merlin

On Tue, 31 Oct 2017, 02:34 Chris Brinkley, <Chris.Brinkley AT sslmda.com> wrote:

Now that I have ProofGeneral working with opam update of coq, I noticed on executing the trivial

Definition plus_fact : P := 2 + 2 = 4.

I get a company-coq error that disappears when I execute the next line:

company-coq: Parsing of tactic grammar failed with error (error Tactic parsing failure [(tactic: auto_using (quote AND) ))]”).

This is with ProofGeneral 4.4.1~pre, coq 8.6.0 installed per official coq opam intructions, and Logic.v from SF 5.3.

I don’t yet know if anything else is impacted. Should I be concerned?

This message (including any attachments) may contain confidential information intended for a specific individual and purpose. If you are not the intended recipient, you should delete this message and any attachments.

[Coq-Club] Company-coq possible issue?, Chris Brinkley, 10/31/2017
- Re: [Coq-Club] Company-coq possible issue?, Merlin Göttlinger, 10/31/2017