aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2013-07-09 17:40:44 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2013-07-09 17:40:44 +0000
commita169507920a0116839a32b691d095be7106932c7 (patch)
tree7db52ecb839fa604a191b6af06f16951b7ce8039
parenta818564b6e0ff66b0e52503b1359411b00c6f4a4 (diff)
Fixed interaction between file variables and coq project file + faq.
-rw-r--r--coq/coq.el24
-rw-r--r--coq/faq76
2 files changed, 96 insertions, 4 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 56f5ae55..05894183 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1039,7 +1039,8 @@ project file settings."
(defun coq-find-project-file ()
"Return '(buf alreadyopen) where buf is the buffer visiting coq project file.
alreadyopen is t if buffer already existed."
- (let* ((projectfiledir (locate-dominating-file buffer-file-name coq-project-filename)))
+ (let* (
+ (projectfiledir (locate-dominating-file buffer-file-name coq-project-filename)))
(when projectfiledir
(let* ((projectfile (expand-file-name coq-project-filename projectfiledir))
;; we store this intermediate result to know if we have to kill
@@ -1116,10 +1117,24 @@ and `use-project-file' to disable this feature."
(unless no-kill (kill-buffer projectbuffer)))))
-;; TODO: read COQBIN somewhere?
+
+;; Since coq-project-filename can be set via .dir-locals.el or file variable,
+;; we need to call coq-load-coq-project-file only *after* local variables are
+;; set. But coq-mode-hook is called BEFORE local variables are read. Therefore
+;; coq-load-coq-project-file is added to hack-local-variables-hook instead. To
+;; avoid adding for other modes , the setting is performed inside
+;; coq-mode-hook. This is described in www.emacswiki.org/emacs/LocalVariables
+
+(defun coq-local-variables-if-enabled ()
+ (when coq-use-project-file (coq-load-project-file)))
+
+;; TODO: also read COQBIN somewhere?
+;; Note: this does not need to be at a particular place in the hook, but we
+;; need to make this hook local.
(add-hook 'coq-mode-hook
- '(lambda ()
- (when coq-use-project-file (coq-load-project-file))))
+ '(lambda () (add-hook 'hack-local-variables-hook
+ 'coq-local-variables-if-enabled
+ nil t)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1647,6 +1662,7 @@ mouse activation."
(unless (zerop (length s)) (insert (format "%s %s.\n" reqkind s)))
while (not (string-equal s "")))))
+;; TODO add module closing
(defun coq-end-Section ()
"Ends a Coq section."
(interactive)
diff --git a/coq/faq b/coq/faq
index d2b1ce7b..c74b6779 100644
--- a/coq/faq
+++ b/coq/faq
@@ -3,6 +3,7 @@
This is a small FAQ for users of coq proof general.
* Configuration of coqtop
+
** How do I configure the options for coqtop?
*** Answer 1: Recommended way of setting coqtop options: use coq project file _CoqProject
@@ -48,9 +49,80 @@ Add the following line to the local variables explained above to set
the binary to use for coqtop (if not in the path):
*** coq-prog-name: ("xxx/bin/coqtop") ***
+
+** OK I want to use a coq project file but with another name, can I?
+
+Yes you can:
+
+(setq coq-project-filename "myprojectfile")
+
+or:
+
+(setq (make-local-variable 'coq-project-filename) "myprojectfile")
+
+If this is for a whole project, the best is probably to have a
+.dir-locals.el file as explained in the section of proofgeneral manual
+(section "Using file variables"). This file should contain something
+like:
+
+((coq-mode . ((coq-project-filename . "myprojectfile"))))
+
+or equivalently:
+
+((coq-mode
+ .
+ ((eval
+ .
+ (progn
+ (make-local-variable 'coq-project-filename)
+ (setq coq-project-filename "myprojectfile"))))))
+
* Ergonomy
+** What are the shortcuts I should know?
+
+The one for navigation:
+
+*** C-c C-n for one step
+*** C-c C-enter to go to cursor.
+You may want to bind these to more convenient non-standard shortcuts.
+ProofGeneral follows emacs policy: it avoids polluting the "short"
+shortcuts with its bindings and let the user configure them at will
+instead.
+
+Other useful shortcuts for queries to coq:
+
+*** C-c C-a C-i
+Inserts ``intros '' and also introduces the name of the hypothesis
+proposed by coq on the current goal.
+
+*** C-c C-a C-s
+Show the goal (enter for the current goal, i <enter> for the ith
+goal).
+
+IMPORTANT: Add the prefix C-u to see the answer with all pretty
+printing options temporarily disable (Set Printing All).
+
+*** C-c C-a C-c
+Prompts for ``Check '' query arguments, the default input name is built
+from the identifier under the cursor.
+
+IMPORTANT: Add the prefix C-u to see the answer with all pretty
+printing options temporarily disable (Set Printing All).
+
+*** C-c C-a C-p The same for a ``Print '' query.
+*** C-c C-a C-b The same for a ``About '' query.
+*** C-c C-a C-a The same for a ``SearchAbout '' query (no C-u prefix).
+*** C-c C-a C-o The same for a Search ``SearchIsos'' (no C-u prefix).
+
+** I hate menus, why do you have menus?
+
+Indeed, very few emacs users use menus, which is understandable.
+However you should have a look at Coq menu and PG menu from time to
+time to see the features they propose, then remember the shortcut and
+hide the menu again.
+
** How can I tell coq to recompile the files that need to be recompiled?
Use option Coq > Settings > Compile before Require
@@ -60,6 +132,10 @@ the file needs to be recompiled by computing the dependencies between
files and comparing modification dates of files. A special Thanks to
Hendrik Tews for this cool feature.
+Notice that this feature will only work if the the coq load path is
+the same for all files. To configure the load path, see the question
+"How do I configure the options for coqtop?" in this faq.
+
* Three windows mode
It has been cleaned up. Here is how it works now.