The Coq mailing list

[David MENTRE <dmentre AT linux-france.org>]

Hello,

I have an issue to setup a working ProofGeneral environment with Coq.

Versions used:
  * The Coq Proof Assistant, version 8.3pl2 (August 2011)
  * ProofGeneral 3.7
  * GNU Emacs 23.3.1
  * System: Ubuntu Linux 11.10 (oneiric)

All are coming from Ubuntu's packages.

I added following lines in my .emacs:
-----
;; For ProofGeneral mode
(setq coq-version-is-V8-0 nil)
(setq coq-version-is-V8-1 t)
(setq coq-prog-name "coqtop")
(setq coq-load-path '("/usr/local/lib/why3/coq"
                      "/usr/local/lib/why3/coq/int"
                      "/usr/local/lib/why3/coq/real"))
------

[ Side note: I need to configure "coq-version-is-V8-1" and
"coq-prog-name" variables for ProofGeneral to work. ]

The /usr/local/lib/why3/coq/real/ directory contains needed Coq .vo files:
-----
$ ls /usr/local/lib/why3/coq/real/
Abs.vo  ExpLog.vo  FromInt.vo  MinMax.vo  Real.vo  Square.vo
-----

I am testing this configuration on following demo.v file:
------
Require Import ZArith.
Require Import Rbase.
Require real.Real.
------

To test it:
  1. I start Emacs
  2. I load ProofGeneral with M-x proofgeneral (apparently a Debian
specific configuration)
  3. I open the .v file (ProofGeneral correctly starts)
  4. I load in Coq each file line with C-c C-n

The "Require real.Real" line fails (after a C-c C-n) with "Error:
Cannot find library real.Real in loadpath" error message.

I googled the web, read the manual, read Debian
/usr/share/doc/proofgeneral/ but I now really don't understand why my
"coq-load-path" is not taken into account.

Any hint?

Sincerely yours,
david