1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
|
;;; coq-local-vars.el --- local variable list tools for coq -*- lexical-binding:t -*-
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
;; Authors: Pierre Courtieu
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
;;; Commentary:
;;
;;; Code:
(require 'local-vars-list) ; in lib directory
(defvar coq-prog-name)
(defvar coq-load-path)
(defconst coq-local-vars-doc nil
"Documentation-only variable.
PROJECT FILE
The recommended way of setting coqtop options (-I, -R and others)
is to use a project file. See the coq documentation (\"generating
makefile\") for details. The default name of the project file is
\"_CoqProject\" (can be configured via `coq-project-filename')
and its content should be a list of options to be given to
coq_makefile (one option per line). Here is an example:
-R foo bar
-I foo2
-arg -foo3
...(optionally followed by all .v files to be compiled)
If `coq-use-project-file' is t (default) ProofGeneral reads the
project file and sets coqtop options accordingly (via variable
`coq-load-path' and variable `coq-prog-args'). In this example the
coqtop invocation will be:
coqtop -foo3 -R foo bar -I foo2
FILE VARIABLES
If for some reason you want to avoid or override the project file
method, you can use the file variables. See Info node ‘(emacs)File
Variables’. This feature of Emacs allows to set Emacs variables on a
per-file basis. File Variables are (usually) written as a list at the
end of the file.
We provide the following feature to help you:
\\[coq-ask-insert-coq-prog-name] builds a standard file variable
list for a coq file by asking you some questions. It is
accessible in the menu
`Coq' -> `COQ PROG (ARGS)' -> `Set coq prog *persistently*'.
You should be able to use this feature without reading the rest
of this documentation, which explains how it is used for coq. For
more precision, refer to the Emacs info manual at ((Emacs)File
Variables).
In Coq projects involving multiple directories, it is usually
necessary to set the variable `coq-load-path' for each file. For
example, if the file .../dir/bar/foo.v builds on material in
.../dir/theories/, then one would put the following local
variable section at the end of foo.v:
\(*
*** Local Variables:
*** coq-load-path: ((\"../util\" \"util\") \"../theories\")
*** End:
*)
This way the necessary \"-I\" options are added to all
invocations of `coqtop', `coqdep' and `coqc'. Note that the
option \"-I\" \"../theories\" is specific to file foo.v. Setting
`coq-load-path' globally via Emacs Customization is therefore
usually inappropriate. With this local variables list, Emacs will
set `coq-load-path' only when inside a buffer that visits foo.v.
Other buffers can have their own value of
`coq-load-path' (probably coming from their own local variable
lists).
If you use `make' for the compilation of coq modules you can set
`coq-compile-command' as local variable. For instance, if the
makefile is located in \".../dir\", you could set
\(*
*** Local Variables:
*** coq-load-path: (\"../theories\")
*** coq-compile-command: \"make -C .. %p/%o\"
*** End:
*)
This way, if foo.v contains the command \"Require bar.\" then
\"make -C .. .../theories/bar.vo\" will run, just before the
require command is sent to coqtop (assuming that bar.v is found
in .../theories).
\(Note that `coq-compile-command' is quite flexible because of
its use of substitution keys. A file local setting of
`coq-compile-command' should therefore usually not be
necessary.)")
(defun coq-insert-coq-prog-name (progname coqloadpath)
"Insert or modify the local variables `coq-prog-name' and `coq-load-path'.
Set them to PROGNAME and COQLOADPATH respectively. These variables
describe the coqtop command to be launched on this file."
(add-file-local-variable 'coq-prog-name progname)
(add-file-local-variable 'coq-load-path coqloadpath)
;; coq-guess-command-line uses coq-prog-name, so set it
(make-local-variable 'coq-prog-name)
(setq coq-prog-name progname)
(make-local-variable 'coq-load-path)
(setq coq-load-path coqloadpath))
(defun coq-read-directory (prompt &optional default maynotmatch initialcontent)
"Ask for (using PROMPT) and return a directory name.
Do not insert the default directory."
(let*
;; read-file-name here because it is convenient to see .v files when
;; selecting directories to add to the path. Moreover read-directory-name
;; does not seem to exist in fsf emacs?? temporarily disable graphical
;; dialog, as read-file-name does not allow to select a directory
((current-use-dialog-box use-dialog-box)
(_dummy (setq use-dialog-box nil))
(fname (file-name-nondirectory default))
(dir (file-name-directory default))
(path
(read-file-name prompt dir fname (not maynotmatch) initialcontent)))
(setq use-dialog-box current-use-dialog-box)
path))
(defun coq-ask-load-path (&optional olddirs)
"Ask for and return the information to put into `coq-load-path'.
Optional argument OLDDIRS specifies the previous value of `coq-load-path', it
will be used to suggest values to the user."
(let (loadpath option)
;; first suggest previous directories
(dolist (olddir olddirs)
(if (y-or-n-p (format "Keep the directory %s? " olddir))
(setq loadpath (cons olddir loadpath))))
;; then ask for more
(setq option (coq-read-directory
"Add directory (TAB to complete, empty to stop): -I " ""))
(while (not (string-equal option ""))
(setq loadpath (cons option loadpath)) ;reversed
(setq option (coq-read-directory
"Add directory (TAB to complete, empty to stop): -I " "")))
(message "Note: Syntax for option \"-R physicalpath logicalpath\":\ncoq-load-path: ((\"physicalpath\" \"logicalpath\") <other paths>)")
(reverse loadpath)))
(defun coq-ask-prog-name (&optional oldvalue)
"Ask for and return the local variables `coq-prog-name'.
These variable describes the coqtop command to be launched on this file.
Optional argument OLDVALUE specifies the previous value of `coq-prog-name', it
will be used to suggest a value to the user."
(let* ((deflt (or oldvalue "coqtop"))
(cmd (coq-read-directory
(concat "coq program name (default \"" oldvalue "\"): ")
deflt t))
(cmd (if (string-equal cmd "") oldvalue cmd)))
(if (and
(string-match " " cmd)
(not (y-or-n-p "The prog name contains spaces, are you sure ? ")))
(coq-ask-prog-name oldvalue) ; retry
cmd)))
(defun coq-ask-insert-coq-prog-name ()
"Ask for and insert the local variables `coq-prog-name' and `coq-prog-args'.
These variables describe the coqtop command to be launched on this file."
(interactive)
(let* ((oldname (local-vars-list-get-safe 'coq-prog-name))
(oldpath (local-vars-list-get-safe 'coq-load-path))
(progname (coq-ask-prog-name oldname))
(loadpath (coq-ask-load-path oldpath)))
(coq-insert-coq-prog-name progname loadpath)))
(provide 'coq-local-vars)
;;; coq-local-vars.el ends here
;; Local Variables: ***
;; fill-column: 79 ***
;; indent-tabs-mode: nil ***
;; End: ***
|
