The Coq mailing list

[Zhaohui Li <lizhaohui1991 AT gmail.com>]

Hello everyone.

I have implemented a new coq-project-file feature based on proof-general.
The differences compared to the old _PROJECT file are that:

  1. New project-file can specify both coq version and coq arguments,
     so we can have different coq implementations with different projects.

  2. New project-file uses elisp language. Actually, it is just .el file.
     For example, in a project, my project-file is this:

       (setq coq-prog-name (expand-file-name "coqtop" (getenv "coq85bin")))
       (setq coq-prog-args `("-R" ,(file-name-directory (buffer-file-name)) "Certi"))

     This means I need coq8.5 and using the project-file directory as the root coq
     LoadPath.

  3. Don't like old _PROJECT file and emacs .dir-locals.el file, which will be loaded
     each time opening a coq file, new project-file is read only before we want run a
     coq file.
     Because in my experience, I always run coq file in a project, but need to see files
     in another project, which project-file should not be read to overwrite the running one.

I write this feature without touching proof-general's code, and the original purpose is
only for my own use:)

Is anyone think this useful?

Thanks ~