Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] New Coq version not seen by Proof General?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] New Coq version not seen by Proof General?


Chronological Thread 
  • From: Chris Brinkley <Chris.Brinkley AT sslmda.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] New Coq version not seen by Proof General?
  • Date: Sat, 28 Oct 2017 19:45:06 +0000
  • Accept-language: en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Chris.Brinkley AT sslmda.com; spf=None smtp.mailfrom=Chris.Brinkley AT sslmda.com; spf=None smtp.helo=postmaster AT mx0a-00142601.pphosted.com
  • Ironport-phdr: 9a23:8g6v1RU+aNZgSJGfUqpo4Kww7X3V8LGtZVwlr6E/grcLSJyIuqrYZRyCt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl8/LePsX4XWks6f1uao+pSVbR8CzG62Zqo3JxGrpy3QsNMXiM1sMPBi5AHOpy5je/5X3itCP1OVnBLx94/k15558j8Wkegg8c1EXLTSZL88SLBRSj8hNjZmt4XQqRDfQF7XtTMnWWIMn08QDg==

Thanks to all who offered suggestions.  It’s working now.

 

(Running PG 4.4.1~pre with companycoq over emacs 24.5.1 on Ubuntu 16.04.)

 

Resolution:

 

init.el:

(setq coq-prog-name "~/opam-coq.8.6/4.01.0/bin/coqtop")
(setq coq-compiler "~/opam-coq.8.6/4.01.0/bin/coqc")
(setq coq-dependency-analyzer "~/opam-coq.8.6/4.01.0/bin/coqdep")

Terminal:

export OPAMROOT=~/opam-coq.8.6
eval `opam config env`
emacs

 

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.

Archive powered by MHonArc 2.6.18.

Top of Page