coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A new coq-project-file feature based on PG

From: Zhaohui Li <lizhaohui1991 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] A new coq-project-file feature based on PG
Date: Mon, 26 Sep 2016 15:47:40 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lizhaohui1991 AT gmail.com; spf=Pass smtp.mailfrom=lizhaohui1991 AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f46.google.com
Ironport-phdr: 9a23:0k/ENRW7rzihK/jiSuDjoIV0sgbV8LGtZVwlr6E/grcLSJyIuqrYZheEt8tkgFKBZ4jH8fUM07OQ6PG6HzVaqs/a6TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLHovcSJKFwT3XKUWvBbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4uUmwRkgdJSyzEpEX+X4Xxuyz6q+skiXjDFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==

Thanks for your kindness ~

2016-09-25 18:16 GMT+08:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

Hi,

Note that what you propose exists already for emacs (see dir_locals.el files). And I doubt Elisp syntax is what we want for config files that should work for other idea and makefiles (which is the goal of Coq project files).

However currently Coq project file only deals with options that are the same for all users. There is indeed a need for a config file that can handle local information like paths to executable and other libraries.

Probably these informations should go in a different file because we don't want them to be stored in repositories. Or we could rely on configure scripts.

P

Le samedi 24 septembre 2016, Zhaohui Li <lizhaohui1991 AT gmail.com> a écrit :
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 ~

[Coq-Club] A new coq-project-file feature based on PG, Zhaohui Li, 09/24/2016
- [Coq-Club] A new coq-project-file feature based on PG, Pierre Courtieu, 09/25/2016
  - Re: [Coq-Club] A new coq-project-file feature based on PG, Zhaohui Li, 09/26/2016