《Certified Programming with Dependent Types》编译冲突及库依赖问题求助

Let's break down your two main issues and fix them step by step—both stem from mismatches between how your Makefile compiles code and how Proof General sets up the Coq environment.

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.

This error is straightforward: the compiled .vo file was built with a different Coq version than the one Proof General is using. Coq uses "magic numbers" to validate that compiled files are compatible with the running Coq instance. Here's how to fix it:

• Verify Coq versions match
  • Run coqc --version in your terminal (this is the default Coq binary your Makefile uses)
  • In Proof General, go to Coq > About to check the version it's invoking
  • If they differ, either install matching Coq versions, or configure Proof General to use the same binary as your terminal. Add this to your Emacs config (.emacs or .emacs.d/init.el):

    (setq coq-prog-name "/path/to/your/correct/coqc")
    

• Recompile with the correct Coq version
  • First fully clean old compiled files to avoid leftovers: make clean
  • Recompile using the same Coq binary as Proof General:

    COQC=/path/to/proofgeneral/coqc make
    

• Align loadpath configurations
  • Ensure Proof General uses the same namespace mappings (-Q/-R flags) as your Makefile. Add this to your Emacs config:

    (setq coq-prog-args '("-Q" "/home/usuario/Desktop/Coq/cpdt/src/" "Cpdt"))
    

  • Alternatively, add this line at the very top of your Subset.v file (before any Require statements) to set the loadpath directly in Coq:

    Add LoadPath "/home/usuario/Desktop/Coq/cpdt/src" as Cpdt.
    

Error: Unable to locate library Extraction.

Extraction is part of Coq's standard library, so this error means Proof General's auto-compilation process isn't including Coq's default standard library paths when running coqdep or coqc. The command log you shared only includes project-specific -Q/-R flags, missing the default loadpath. Try these fixes:

• Test without auto-compilation first
  • Turn off the Coq -> Auto Compilation -> Compile before require option
  • Run Require Extraction. directly in Proof General. If this works, the problem is definitely with the auto-compilation argument setup.
• Fix Proof General's auto-compilation loadpath
  • Check your Emacs config for any coq-prog-args that include -noinit—this flag disables the standard library, so remove it if present.
  • If needed, explicitly add the standard library path to coq-prog-args. First get the standard library path with coqc -where, then add this to your Emacs config:

    (setq coq-prog-args (append coq-prog-args '("-R" "/path/to/coq/stdlib" "Coq")))
    

• Check your Makefile for problematic flags
  • If your Makefile uses -noinit or other flags that exclude the standard library, remove them—these will break any Require of standard library modules like Extraction.
• Use the full namespace (if needed)
  • In some cases, you might need to specify the full standard library namespace:

    Require Coq.Extraction.Extraction.
    

内容的提问来源于stack exchange，提问作者user1868607