search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
484 stars 85 forks source link

coq-load-project file should extract META files #736

Open hendriktews opened 5 months ago

hendriktews commented 5 months ago

Since 8.16 coq_makefile extracts META files from _CoqProject and passes them to coqdep via -m, see https://github.com/coq/coq/pull/15220. PG should also extract META files, such that a -m switch can be added to coqdep invocations. Otherwise auto-compilation on files using ML modules will fail, see #724. Note that the -m switch is only a necessary (but no sufficient) condition to support ML modules in auto-compilation.

hendriktews commented 5 months ago

Until this feature is implemented, affected users may workaround by setting coq-compile-extra-coqdep-arguments from PR #735. Note that one needs to use absolute path' there, because coqdep is also invoked on temporary files in /tmp that contain single require lines from the current file. The option needs to be set for all files of a project, so it's probably best to set it via directory variables, eg.,

((coq-mode .
      ((coq-compile-extra-coqdep-arguments
        . ("-m" "/absolute/path/to/META.file")))))