Unable to set up Certified Programming with Dependent Types

I am working with the book Certified Programming with Dependent Types but each time I'm finding a different error. It seems to me that the error comes from a mismatch between the compilation process from Proof General and through the makefile of the sources of the book.

If I compile the sources with make and try to run for instance Subset.v in Proof-General I get:

Error: File /home/usuario/Desktop/Coq/cpdt/src/CpdtTactics.vo has bad magic number 81100 (expected 8600). It is corrupted or was compiled with another version of Coq.

If I clean the makefile compiled files with make clean and try to proceed with the option Coq -> Auto Compilation -> Compile before require then it is the line:

Require Extraction.

that fails. Originally it failed with the error:

Error: Unable to locate library Extraction.

but with the above option enables it gives something like:

echo "Require Extraction." > /tmp/ProofGeneral-coqQPJTf0.v coqdep -Q /home/usuario/Desktop/Coq/cpdt/src/ -R /home/usuario/Desktop/Coq/cpdt/src Cpdt /tmp/ProofGeneral-coqQPJTf0.v * Warning: in file /tmp/ProofGeneral-coqQPJTf0.v, library Extraction is required and has not been found in the loadpath! * Warning: in file /tmp/ProofGeneral-coqQPJTf0.v, library Extraction is required and has not been found in the loadpath! /tmp/ProofGeneral-coqQPJTf0.vo /tmp/ProofGeneral-coqQPJTf0.glob /tmp/ProofGeneral-coqQPJTf0.v.beautified: /tmp/ProofGeneral-coqQPJTf0.v /tmp/ProofGeneral-coqQPJTf0.vio: /tmp/ProofGeneral-coqQPJTf0.v

How can I solve this?

Solution

Side-questions: which OS are you using? do you rely on opam?

Regarding the first error you get, it certainly comes from the following fact:

outside proofgeneral, the coqc binary corresponds to Coq 8.11, while in ProofGeneral, the coqtop binary correspond to Coq 8.6. Maybe because the PATH variable is not the same in the two contexts.
To figure out which binary is found, you can do in the terminal which coqtop, and within Emacs, M-! which coqtop RET and you should thus get different paths.
Sometimes, opening emacs directly from the terminal (emacs &) can help for this kind of issue.
But if you want to change the coqtop binary that is used in ProofGeneral, you can set the coq-prog-name option, by using one of the following steps:
- Interactively, type C-u C-c C-x (to kill Coq), M-: (setq coq-prog-name "…/coqtop"), and C-c C-n
- Or create a .dir-locals.el file (Emacs' standard conf-file) in the project root containing:
```
((coq-mode . ((coq-prog-name . "…/coqtop"))))
```
  and close/reopen the ….v file at stake (or just do M-x normal-mode RET or C-x C-v RET in the already-opened ….v buffer)

Regarding the second error you get, I'm a bit puzzled that Require Extraction triggers this error, as this library does exist in Coq 8.6 and 8.11.

At first sight, I'd suggest to re-test the auto-compilation with Coq 8.11, asserting From Coq Require Extraction. (instead of just Require Extraction.)

But maybe there is a bug in PG's Auto Compilation -> Compile before require feature; anyway feel free to open a related issue in the PG tracker if need be, bug reports and feature requests are very welcome: https://github.com/ProofGeneral/PG/issues