emacscoqproof-general

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.

  1. 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.

  1. 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:

    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